SAT Solver
SAT solver written as part of the course "SAT Solving" at LMU Munich in the winter semester 2020/2021
with Lukas Bartl, Christian Dietze & Luca Maio
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.
Notes
Written in C++17 and built with CMake, targeting POSIX systems (Linux and macOS). Licensed under the GPLv3+.