nksat is a lightweight SAT solver written in C++. nksat checks systems of
boolean equations for satisfiability. nksat expects a single input file in
the standard DIMACS .cnf input format.
Under the hood, nksat uses the DPLL
algorithm and makes use of the "two watched literals" and "pure literal
elimation" optimizations.
nksat has the following dependencies:
- A working C++ compiler and build system (e.g.
Make) CMake
To build nksat, create a new directory (e.g. build) inside the project root
directory, and then inside that directory run the following command
(assuming Make is the default build system):
cmake .. && make
This command will generate and run the build files. An nksat executable will
be created in the build directory.
nksat can be run using the following command:
nksat <path/to/.cnf/file>
nksat expects input files to be in the DIMACS .cnf format as described
here.
nksat will output either a satisfying assignemnt or inform if no such
assignment exists.
nksat was written jointly by:
- Nicholas Lindsay ([email protected])
- Ketaki Joshi ([email protected])
Both authors contributed equally.