| title | tags | authors | affiliations | date | bibliography | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
LearnSAT: A SAT Solver for Education |
|
|
|
25 February 2018 |
learnsat.bib |
Many problems can be solved by encoding them as formulas in propositional logic which are checked for satisfiability by a program called a SAT solver. If found, a satisfying assignment provides the answer to the problem. Donald Knuth [@knuth-sat] calls SAT solvers a killer app because diverse practical problems can be solved by a single, highly-optimized, program. Despite their importance, SAT solvers are described only in research papers. LearnSAT is designed for teaching and learning SAT solving by providing a concise, well-documented, implementation, fine-grained tracing (both textual and graphical) of the algorithms and a detailed tutorial.
LearnSAT implements the core algorithms of modern SAT solvers [@SAT]: the Davis-Putnam-Logemann-Loveland (DPLL) algorithm with conflict-driven clause learning (CDCL) and non-chronological backtracking (NCB). CDCL is implemented by backwards resolution from a conflict clause to a unique implication point (UIP) [@mlm]. It is also possible to compute dominators in the implication graph. In addition, two heuristics for lookahead are implemented.
The user of LearnSAT can choose any subset of 24 display options in order to tailor the output to a specific learning context. The display options include elementary steps like decision assignments, unit propagations and identifying conflict clauses, as well as the advanced steps of CDCL: the resolution steps used to obtain a learned clause and the search for UIPs.
LearnSAT can generate two types of graphs that are rendered using the dot tool: trees showing the search through the assignments and implication graphs that display the process for learning clauses from conflicts.
LearnSAT is implemented in Prolog and was developed using SWI-Prolog which available for Windows, MacOSX and Linux, although almost all the source code is compatible with the standard.
Three documents are included in the project:
learnsat-overviewAn overview of LearnSAT.learnsat-ugUser's guide and software documentation.learnsat-tutorialTutorial on SAT solving using LearnSAT.
About 20 examples are included of encodings of problems that can be solved by LearnSAT.