Sitting solver aspires to be a good SAT solver in the future.
Resources about SAT solvers:
- The Wikipedia page for DPLL has a concise recursive formulation of the basic DPLL algorithm
- This series of blog posts has good explanations of the ideas behind DPLL, clause learning, and the two watched literals scheme, but be aware that their implementation of clause learning without conflict analysis isn't great
- This SAT tutorial paper is pretty good too; it has simple code examples with thorough explanations. I found its explanation of conflict analysis and backjumping particularly useful.
- The original MiniSAT paper is also helpful
- SATLIB and the annual SAT competitions have huge catalogs of SAT benchmarks, in a convenient format
To do:
- Main DPLL loop
- Watched literals
- Pre-processing
- Post-processing
- Conflict analysis and conflict-driven clause learning
- Conflict-clause minimization
- Update the heuristic: VSIDS
- Backjumping
- Limits for clause learning, + heuristic for which learned clauses to keep
- Restarts?
- Profiling + optimization
- Automated testing infrastructure
- Better docs
In the (far) future, I hope to extend it to a simple DPLL(T) SMT solver. This would involve:
- The Tseitin transformation
- A special preprocessing mode for DPLL(T)
- Likely a special postprocessing mode, too
- Extensions to the main DPLL solver to allow feedback from the theory solver
- Theory solvers: LRA, congruence closure for UF
- Theory-specific preprocessing?
- Something about quantifiers and E-graphs, idk
- Would also be cool to have: NRA by ICP + LRA or CAD, LIA somehow