LearnSAT is a SAT solver: a program for searching for a satisfying interpretation of a CNF (conjunctive normal form) formula in propositional logic. Although the SAT problem is NP-complete, in real-world examples modern SAT solvers have proven to be extremely efficient and are widely used in many fields such as artificial intelligence and hardware verification. For an overview of SAT solving, see Chapter 6 of the third edition of Mathematical Logic for Computer Science. The definitive reference for SAT solving is: Biere, A., Heule, M., Van Maaren, H., Walsh, T. Handbook of Satisfiability , 2009.
LearnSAT is a program designed to facilitate learning the central algorithms used by modern SAT solvers: the DPLL algorithm together with conflict-directed clause-learning, non-chronological backtracking and lookahead.
LearnSAT is written in Prolog and the core algorithms consist of about 250 lines of code. A very detailed trace of the algorithm's execution is displayed and the specific content of the trace can be set by the user. LearnSAT generates DOT files for the implication graphs and the tree of assignments.
The archive contains CNF encoding for many example programs:
- Graphical combinatorics: graph coloring, Tseitin graphs.
- Games: Sudoku, 4-queens, colored queens.
- Number theory: Ramsey theory, Schur triples, Langford's and van der Waerden's problems.
- Constrained arrangements: pebbling formulas, seating guests at a table.
- Bounded model checking.
Three documents are included in the archive:
- User's Guide and Software Documentation.
- Tutorial which explains the algorithms and describes the examples.
Download from GitHub: https://github.com/motib/LearnSAT.