Computer Engineering students won the champion in the ICCAD 2014 International Contest, the 3rd time in a row (since 2012), setting an accumulated winning gap record (> 100%) over the 2nd place teams.
Congratulations to Xing Wei, Yi Diao, and Tak-Kei Lam supervised by Prof. Yu-Laing (David) Wu won the championship of international ICCAD contest 2014 in the contest problem “Simultaneous CNF Encoder Optimization with SAT solver Setting Selection”. It is considered one of the most difficult SAT solver problems (for electronic circuitry formal verification) containing some likely NP-hard sub-problems with no satisfactory solutions proposed by academia or industry. One of its sub-problems, Multiplier Verification, has been given in previous open SAT solver contest. To our knowledge, we are the world’s first team managed to solve this problem for all practical design styles in a runtime linear to the circuit size, a runtime complexity already achieving the theoretically lowest possible, thus can win the rest contest teams by a gap of ~40%.
This is a research-oriented contest problem posted by one leading EDA company Cadence to challenge global academia institutes, with cash prize sponsored by the Ministry of Education (MOE) of Taiwan. The contest problem was posted 6 months ahead of the deadline (for universities can form tailored project course for the contest), with contest scores of leading teams announced periodically. A team is encouraged to be formed by multiple supervising professors with unlimited number of students from multiple universities to maximize the chance of forming stronger teams to stimulate better results. Our team solved 81 out of the 120 tested circuits, a significant leading of the 2nd (3rd) teams who solved 59(57) cases.
Perhaps noteworthy to mention, this same member team has won the same contest champion 3 times since 2012, the first Hong Kong team achieving this, particularly with a record highest accumulated winning gaps atop the 2nd place teams by over 100% (47%/2012, 19%/2013, 37%/2014). (For reference, the winning gap of another contest problem of the same contest is < 1%)
