This git contains the SAT solver of a modular SMT Solver called modulariT. ModulariT is a project lead by Pr. Pascal Fontaine and whose goal is to create a modular SMT Solver in C++ for academic and research purposes.
NapSAT is inspired by the MiniSAT but (will) support incremental solving, hints and other useful features for SMT solving.
The solver was written by Robin Coutelier as a follow-up to his master thesis on "Chronological vs. Non-Chronological Backtracking in SMT Solving" and is currently work in progress. It was partially written while working at the University of Liège, Belgium, and the project is still ongoing at the TU Wien, Austria (as of 2024) under the supervision of Pr. Laura Kovács.
The goal of this project is to create a flexible SAT solver that implements both chronological and non-chronological backtracking while still supporting standard SMT features such as incremental solving, hints, etc.
The solver also implements an observer pattern that allow easy debugging, and automatic tikz graph generation for the trail, the clause set and the implication graph. This is useful for understanding the history of the bug, and generating slides for presentations.
This solver brings the contribution of Lazy Strong Chronological Backtracking. A method used to enforce stronger invariants to chronological backtracking, and to reduce the number of propagations while never missing unit implications. A paper on this topic is currently being written and will be submitted to SAT 2024.
This project uses the lzma library for decompression of xz files. You can install the necessary dependencies by running the following command:
make installThe project uses Make to generate the build files. To build the project as a library, simply run the following commands:
makeThis will generate the build files and compile the project. The executable will be located in the build folder.
You can also build a library by running make lib or make all.
A debug version can be generated by running the following commands:
make debugThis will generate the build files and compile the project with debug flags (including the library). The executable will be located in the build folder. In debug mode, the executable will be named NapSAT. This executable aggressively checks for invariant violations and will be much slower than the release version.
Building the project will generate two executables in the build folder: NapSAT-*version* and test-SAT. The first one is the SAT solver itself and the second one is the unit tests executable. The unit tests are not very elaborate at the moment, and will be improved in the future.
The SAT solver can be run with the following command:
./NapSAT <input-file> [options]The input file must be a valid DIMACS CNF file. The solver will then try to solve the given formula and print the result on the standard output.
NapSAT can be used as a library. The API is defined in include/SAT-API.hpp. This allows a more abstract use of the solver. However, advanturous users can also use the internal API defined in src/solver/NapSAT.hpp. However, since this project is not yet stable, the internal API is subject to change.
The main contribution of NapSAT is the implementation of different chronological backtracking strategies that can be selected at runtime. The different versions are described in a paper that is currently under submission.
An observer can be attached to the solver to check and debug the solver. The observer can be used to generate tikz figures of the trail, the clause set and the implication graph. This is useful for creating slides for presentations.
It also allows the user to check the behavior of the solver with a configurable level of detail. This can be useful for debugging large formulas.
Furthermore, the interactive mode if the solver allows the user to interact with the solver during runtime. Chosing specific decisions or learning clauses can be done interactively. For bug reproduction, this functionality can be accompanied by a command file that will be executed by the solver.
For example, the follwing command shows the behavior of the solver in lazy strong chronological backtracking mode on a specific test case:
One can set the navigation level to show more details. use the command set level 10 to show all details.
build/NapSAT tests/cnf/test-trigger-mli.cnf -i -commands test/cnf/test-trigger-commands.txt -lscbThe solver generates proofs for UNSAT formulas. The proof can be printed in a human-readable format or simply checked using the options -pp and -cp respectively.
build/NapSAT tests/cnf/unsat-01.cnf -ppThis project is not under any license yet, but the author allows anyone to use, modify and redistribute the code as long as the author is credited and the code is not used for commercial purposes.
If you have any questions or suggestions, feel free to contact me at robin.coutelier@gmail.com.