Today I played with SmallCheck. Interested in what happened when I tried to find a small unsatisfiable boolean formula that is not easily detected as such? Watch my attempts! (strip .html suffix for executable Haskell file)


After realising that the crucial step to enable SmallCheck to find the formula was not the limitation to conjunctive normal form but the limitation to only two variables, I tried what happens when incorporating this limitation in the original Serial instance for Booleans:

  instance Serial Boolean
    series = const [Var 0, Var 1]
          \/ cons0 Yes
          \/ cons0 No
          \/ cons1 Not
          \/ cons2 (:&&:)
          \/ cons2 (:||:)

Using this instance, SmallCheck finds a counter example at depth three in about 30 seconds:

  Depth 3:
    Failed test no. 10682586. Test values follow.
    (Var 0 :&&: Not (Var 0)) :||: (Var 1 :&&: Not (Var 1))

This is a condensed version of the formula found before (which is the CNF of this one). Seems like by generating only CNFs I was barking up the wrong tree!