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 -CNF will have a much greater
clauses/variables ratio, not to say about the length of its clauses).

LE BERRE Daniel 2002-09-16