Debugging SAT Solvers
Fuzzing and Delta-Debugging
On https://fmv.jku.at/fuzzddtools/, you can find various tools for CNF fuzzing and delta debugging. You can start with CNFuzzDD, and if you need lower-level fuzzing and delta debugging, you can use ddsexpr.
You can also try generating various CNFs using tools like concealSATgen or CNFgen. Unfortunately, though, these tools are written in Python and thus slow when generating large instances.
Performance Debugging using gperftools
sudo apt install google-perftools
Put something like this in your code:
#ifdef PROFILE
#include <gperftools/profiler.h>
#endif
#ifdef PROFILE
ProfilerStart("babysat.prof");
#endif
int res = solve();
#ifdef PROFILE
ProfilerStop();
#endif
Compile using -DPROFILE and -lprofile after -o program program.cpp.
Run the program normally with an instance
google-pprof --pdf ./babysat babysat.prof > 03_prof_squeezed.pdf
You will have to change the makefile:
profile=no
COMPILE="g++ -Wall -Wextra -Weffc++ -static"
LINK=""
[ $profile = yes ] && symbols=yes
[ $profile = yes ] && COMPILE="$COMPILE -DPROFILE" && LINK="$LINK -lprofiler"
echo "configure: using '$COMPILE$LINK'"
sed -e "s#@COMPILE@#$COMPILE#" -e "s#@LINK@#$LINK#" makefile.in > makefile
The makefile template:
COMPILE=@COMPILE@
LINK=@LINK@
all: babysat
babysat: babysat.cpp config.hpp makefile
$(COMPILE) -o $@ $< $(LINK)
This is also a nice resource.
GDB
sudo apt install gdb
gdb --args ./babysat cnfs/add4.cnf
Then, in gdb:
run
bt
fr <frame>
print <var>