Simple implementation of the Davis–Putnam–Logemann–Loveland (DPLL) algorithm for solving the satisfiability problem of propositional logic written in C99 without external dependencies.
No dependencies except a C compiler (clang and gcc are tested)
Create build directory for out-of-tree build:
mkdir build
cd build
CMake generates files for another build system that will then be used for the actual build.
Generate default CMake build files:
cmake ..
Generate Makefile:
cmake -G 'Unix Makefiles' ..
Generate Ninja files:
cmake -G 'Ninja' ..
Specify C compiler:
cmake -DCMAKE_C_COMPILER=clang ..
Create release binary:
cmake -DCMAKE_BUILD_TYPE=Release ..
Create binary with debug information:
cmake -DCMAKE_BUILD_TYPE=Debug ..
Use link-time optimization (LTO) (needs compiler support):
cmake -DUSE_LTO=on ..
Enable building of tests (see below):
cmake -DBUILD_TESTING=on ..
Build using Makefile:
make
Build using Ninja:
ninja
Run solver on DIMACS file:
build/dpll --dimacs < input.txt
Run solver on plain text formula:
echo "{A, B}, {-A, -B}, {-C}, {E, D}" | build/dpll --cnf
Run solver on plain text formula with custom format:
echo "(A v B) ^ (-A v -B) ^ (-C) ^ (E v D)" | build/dpll --cnf --cstart '(' --cend ')' --cdel 'v' --cneg '-'
Before running test a successful build with -DBUILD_TESTING=on has to be done!
Test are tagged with labels functional and memory according to what they check:
- functional
Runs application on known input and check if returned result is correct - memory
Check code for memory leaks. Requires valgrind!
Specify --output-on-failure to print output of failing test.
Specify -j XX to run XX tests in parallel.
Run all tests:
cd build
ctest .
Run 4 tests with label memory in parallel:
cd build
ctest -L memory -j 4 --output-on-failure .
This software is released under the GPL v.3.