next up previous
Next: Other views of the Up: The results Previous: Second stage


We awarded the two smallest (one satisfiable and one unsatisfiable) instances that remained unsolved during the competition. Of course, both instances participated in the second stage, i.e., the top 5 solvers were run on them for 6 hours! Note that we did not take into account here the instances that were submitted as ``unknown''.

The smallest hard unsatisfiable instance xor-chain/x1_36 (106 variables, 844 literal occurrences) was submitted by Lintao Zhang and Sharad Malik.

The smallest hard satisfiable instance hgen2-v500-s1216665065 (500 variables, 5250 literal occurrences) was generated by Edward A. Hirsch's random instance generator hgen2.

Note that instances with fewer variables also remained unsolved, but the winner was determined by the total number of literal occurrences in the formula (note that a hard randomly generated formula in $ 4$-CNF will have a much greater clauses/variables ratio, not to say about the length of its clauses).

LE BERRE Daniel 2002-09-16