TinySAT

A basic SAT solver using DPLL algorithm, available in both Python and Java.

Introduction

What is a SAT Solver?

A SAT solver is a mathematical solver created to find solutions for Boolean Satisfiability Problems, which is NP-complete. More info can be found on the wikipedia's page. Many difficult problems can be reduced to a SAT problem and thus can be solved with a SAT solver.

What are SAT Solvers used for?

Any NP-hard problems can be formulated as SAT formular and be solved by SAT Solvers. Some areas where they have been performing well are:

• Package management system. Conda, a package manager for Python, explains in this article that they have been using picosat in their implementation and is experimenting with other SAT solvers. Fedora's DNF is also solving the dependency resolution problem using SAT Solvers.

Usage

Input format

The input format is DIMACS CNF, which is standard for SAT solvers. A brief description can be found here.

Example:

c A sample input file.
p cnf 3 2
1 -3 0
2 3 -1 0 

Example usage

python tinysat.py ../examples/simple.dimacs