Overview

YASER is a SAT solver written in C++23. The main features are:

• DIMACS CNF input
• CDCL-style DPLL algorithm
• Constraint propagation with watched literals
• VSIDS-driven variable decisions

Requirements

• C++23-capable compiler (supported are GCC and Clang)

• CMake (≥ 3.13)

• The repository uses some external libraries as submodules (fmt, googletest, google/benchmark).

License

Licensed under the BSD 2-Clause License - see the LICENSE file for details.