pysat — a CDCL SAT solver in pure Python

This is a CDCL Python (3.9+) native implementation. It is very slow (like 10x-50x times) but the data structure is a native python one, made with as many tricks as possible. It is a nice toy to play with. No dependency, only the Python standard library.

Not to be confused with PySAT (pip install python-sat), the Python toolkit that wraps C/C++ SAT solvers.

Learn Clause Learning Algorithms

The idea is to be able to quickly play with CDCL concepts. If you understand it, you can dig into Minisat/Glucose source code now!

The CDCL solver (src/pysat.py) implements:

• 2-watched literals propagation,
• conflict analysis with the first UIP scheme,
• VSIDS heuristics (with a heap of variables, as in Minisat) and phase saving,
• geometric restarts.

A plain DPLL solver (src/pysatdpll.py) is also given, written with the same data structures and function names, to compare both algorithms: occurrence lists, static heuristics and chronological backtracking, no learning.

The chain of solvers

The same algorithms are also written as a chain of classes, each one inheriting from the previous one and adding a single idea (usually by redefining two or three methods):

Class	File	What it adds
Solver	src/satsolver.py	the formula, the API (incremental addClause, solve), the statistics
DPLL	src/dpll.py	propagation with counters, decisions, chronological backtracking
CDCL	src/cdcl.py	first UIP conflict analysis, clause learning, backjumping
Watches	src/watches.py	2-watched literals: nothing to restore when backtracking
SATO	src/sato.py	(from CDCL, to compare with Watches) head/tail pointers for the propagation
VSIDS	src/vsids.py	the VSIDS heuristic, with the heap of Minisat
Restarts	src/restarts.py	geometric or Luby restarts, phase saving
Reduce	src/reduce.py	reduction of the learnt clauses, by activity or LBD
Minimize	src/minimize.py	local or recursive minimization of the learnt clauses
VMTF	src/vmtf.py	(from Watches, to compare with VSIDS) the VMTF heuristic: a queue, the variables of the conflicts move to the front
MinimizeVMTF	src/vmtf.py	the whole chain with VMTF instead of VSIDS, by multiple inheritance (class MinimizeVMTF(VMTF, Minimize))
Glucose, GlucoseVMTF	src/glucose.py	dynamic restarts of Glucose (moving average of the LBD, blocking restarts), with VSIDS or VMTF
Lookahead, DoubleLookahead	src/lookahead.py	(from DPLL) lookahead heuristics and failed literals

Each file can be run as a solver (python src/watches.py examples/sample.cnf). The source browser shows the inheritance tree and, for each class, its methods as a diff with the parent version, its hooks, the whole solver at this step and the measures (in French or English, button at the top): https://lorensipro.github.io/pysat/ (generated by python tools/navigateur.py in docs/).

The experiments of the course are replayed by python experiments/experiments.py (see --list, --jobs, --timeout); recent benchmarks of the SAT competitions are fetched from GBD by python examples/fetch_gbd.py.

How to use it?

Just go into the src directory and type:

python pysat.py ../examples/sample.cnf
python pysatdpll.py ../examples/sample.cnf

Input files are in the DIMACS CNF format, possibly compressed (.cnf.gz). As in the SAT competitions, the solver prints s SATISFIABLE (with the model on the v line) or s UNSATISFIABLE, and exits with code 10 or 20.

Random formulas can be generated with:

python genRandom.py 100 3 4.26 > random.cnf    # 100 variables, 3-CNF, ratio 4.26 (optional 4th argument: seed)

Some benchmarks are available in examples/BMC-Unsat (try barrel5.cnf.gz, it takes a few seconds).

The solver can also be used from Python:

from pysat import Solver

s = Solver()
s.addClause([1, -2])
s.addClause([2, 3])
s.buildDataStructure()
if s.solve() == s._cst.lit_True:
    print(s.finalModel)

Tests

From the root of the repository:

python -m unittest discover tests

All the solvers are checked against a brute-force enumeration on random formulas, the models are verified, and the learnt clauses are checked to be consequences of the formula.

See also

pysat is meant to be read next to other works that explain SAT solvers piece by piece. It does not replace them; it tries to be complementary.

SATCH, by Armin Biere, is the reference we would recommend first. It is a SAT solver written from scratch in C, whose main purpose is to provide a simple and clean code base for explaining and experimenting with SAT solvers, while still featuring most of the implementation techniques of a state-of-the-art solver, and serving as a gentle introduction to CaDiCaL and Kissat. Every feature can be switched off at compile time (./configure --no-learn, --no-watches, --no-cdcl...), with explicit dependencies and incompatibilities between features: a remarkably clean way to see what each ingredient brings, in a solver that is really efficient.

pysat takes the same question from the other side, and with other means:

	SATCH	pysat
Language	C, efficient	Python, slow but short and readable
Features	removed at compile time from a complete solver	added one by one, each class inheriting from the previous one
What a student reads	one solver, with its feature switches	a sequence of small diffs (see the source browser)
Measures	the solver itself, on real benchmarks	machine independent counters (clauses visited, clauses restored...) and the course experiments
Scope	state of the art: rephasing, stable/focused modes, tiers, inprocessing...	the path from DPLL to a Minisat/Glucose-like CDCL, plus lookahead (and soon local search)

The ingredients, side by side:

Ingredient	SATCH option	pysat
pure DPLL, no learning	--no-cdcl, --no-learn	DPLL
counters instead of watches	--no-watches	DPLL, CDCL (and SATO, head/tail pointers)
watched literals, blocking literals	default, --no-block	Watches (blocking literals: measured, not in the chain yet)
VSIDS, VMTF	--no-vsids, --no-vmtf	VSIDS, VMTF (and MinimizeVMTF)
restarts	moving averages, focused/stable modes	Restarts: geometric, Luby; Glucose: moving averages of the LBD, blocking
phase saving, target and best phases, rephasing	--no-save, --no-target, --no-best, --no-rephase	Restarts (phase saving only)
reduction of the learnt clauses	glue tiers, --no-reduce, --no-glue, --no-tier1, --no-tier2	Reduce: activity or LBD (glue clauses kept)
minimization, shrinking	--no-minimize, --no-shrink	Minimize: local or recursive
chronological backtracking, trail reuse	--no-chrono, --no-reuse	not yet
preprocessing and inprocessing	elimination, subsumption, strengthening, vivification	not yet
lookahead, failed literals		Lookahead, DoubleLookahead

Also worth reading:

• Donald Knuth, The Art of Computer Programming, vol. 4B, section 7.2.2.2, and his programs SAT0 to SAT13: a basic backtracking solver, WalkSAT (SAT8), survey propagation (SAT9), Davis-Putnam (SAT10), lookahead (SAT11), a preprocessor (SAT12) and CDCL (SAT13), each one measured in "mems".
• A. Biere, M. Fleury, N. Froleyks, M. Heule, The SAT Museum (Pragmatics of SAT 2023): the historical solvers run on the same benchmarks, to measure the progress of each generation.
• A. Biere, Tutorial on Modern SAT Solving (EPFL, 2019) and Modern CDCL SAT Solvers (SAT/SMT summer school, 2012).

Good luck!