SAT Solver
SAT solver written as part of the course "SAT Solving" at LMU Munich in the winter semester 2020/2021 (group project).
About
A command-line SAT solver implementing both the CDCL (conflict-driven clause learning) and DPLL algorithms, developed as a group project for the lecture SAT Solving in the winter term 2020/2021 at LMU Munich. It reads instances in the DIMACS CNF format and outputs either a satisfying assignment or a verdict of unsatisfiability; in CDCL mode it can additionally emit a DRAT proof that can be checked by external verifiers such as drat-trim.
Features
Nearly every aspect of the solver can be configured on the command line:
- Branching heuristics: VMTF and VSIDS for CDCL; DLIS, DLCS, SLIS, SLCS, Böhm’s, and Jeroslow–Wang’s heuristics for DPLL (the solver type is inferred from the chosen heuristic)
- Learning schemes (CDCL): 1UIP, RelSAT, decision
- Clause deletion strategies (CDCL): simple and bounded, with tunable thresholds
- Restart policies (CDCL): inner/outer, geometric, Luby, fixed, or none
- Preprocessing: subsumed clause elimination, blocked clause elimination, pure literal elimination, and variable hole elimination, each of which can be toggled individually
Notes
Written in C++17 and built with CMake, targeting POSIX systems (Linux and macOS). Licensed under the GPLv3+.