LearnSat

Mordechai (Moti) Ben-Ari

http://www.weizmann.ac.il/sci-tea/benari/

---

LearnSAT is a Prolog program for learning about SAT solving. It implements the classic Davis-Putnam-Logemann-Loveland (DPLL) algorithm, together will modern extensions of the algorithm: conflict-driven clause learning (CDCL), non-chronological backtracking (NCB) and lookahead.

Licences

• The software is made available under the GNU General Public License.
• The documentation is made available under the Creative Commons Attribution-ShareAlike 3.0 License.

Installation and running

LearnSAT is written in Prolog.

• Install SWI-Prolog.
• Unzip the archive learnsat-N.zip.
• To run the LearnSAT, consult the file dpll.pro as explained in the User's Guide.

Directories

• src: The LearnSAT source code.
• examples: Source code for the examples.
• docs: Documentation (in LaTeX and PDF).

Documentation

• learnsat-overview An overview of LearnSAT.
• learnsat-ug User's guide and software documentation.
• learnsat-tutorial Tutorial on SAT solving using LearnSAT.

Community guidelines

Thank you for your interest in LearnSAT.

This is my first Open Source / GitHub project, so there may be some glitches until I have more experience!

For now, the guidelines are:

• If you wish to modify the Prolog source code, please fork the project and leave the master branch with my source code.
• If you have additional SAT examples or tutorial material that you want to add, I can include them in the master branch. Open an issue and / or contact me directly at moti.ben.ari@gmail.com.