DPLL SAT Solver

A simple DPLL-based boolean satisfiability solver written in C.

Building from source

After downloading a copy of the source code, the project can be built using GNU Make and Clang:

cd src
make

If you are using Nix, a development shell containing the required build tools can be created with the following command:

nix shell nixpkgs#gnumake nixpkgs#clang

This produces a binary in the src/ directory named DPLLMain.

Running

To run the solver, provide one argument containing a path to a DIMACS CNF file.

For example (from the /src/ working directory):

./DPLLMain example1.cnf

The program will output either true or false, meaning the formula is satisfiable or unsatisfiable respectively.

If the program outputs Input Error, then there was an issue with the provided input. Check that the file exists and the syntax is valid.