SAT solver

Compiling

Simply run :

ocamlopt sat.ml && ./a.out

This yields the best performance as heavy computations are done for SAT solving (and not all optimizations are implemented).

Testing on .cnf formatted files

Specification of .cnf

You can test whether your formatted CNF is satisfiable or not by adding a test case (around line 264) :

assert (dpll_pure_unit (parse "<file>"));

Testing whether a sudoku has a solution (not necessarily unique)

Add a new test case (at the end of the file) in the form of a 2D-array [| [| … |] , … , [| … |] |] with clues ranging 0-8 and blanks marked as 9.