Sat Solver SATCH

This is the source code of SATCH a SAT solver written from scratch in C.

The main purpose of this solver is to provide a simple and clean code base for explaining and experimenting with SAT solvers. It is simpler than the source code of CaDiCaL and of Kissat in particular, while still featuring most important implementation techniques needed to obtain a state-of-the-art SAT solver (the current version still lacks preprocessing and incremental solving though). Thus is also serves as a gentle introduction into the code base of CaDiCaL and Kissat.

The code allows to switch off individual and more basic features at compile time by using different ./configure options. For instance completely disabling clause learning can be achieved with ./configure --no-learn. This not only gives a clean separation of features in the code but also makes it easier to disable (through the C pre-processor) redundant not needed code anymore if a certain feature is disabled.

For a more complete SAT solver you might want to use CaDiCaL, particularly for incremental usage, and for fastest solving fall back to Kissat.

Building

Run ./configure && make test to build and test the solver binary satch as well as the library libsatch.a:

satch stand-alone solver binary satch.h solver API similar to IPASIR libsatch.a library with API in satch.h

The source of the application and library consists of the following:

satch.c library code of the SAT solver stack.h generic stack implementation (header file only) rank.h generic radix-sort implementation (header file only) config.c provides build-information generated by mkconfig.sh main.c application code with parser and witness printer

The files used by the build process are the following:

VERSION current version configure configuration utility makefile.in makefile template used by configure makefile generated from makefile.in by configure mkconfig.sh generates config.c to provide build information

Some additional documentation can be found in these files:

README.md this file explains build process and files FEATURES.md compile time option and feature set-up

The configure script will generate makefile from the template makefile.in. The default make goal all first calls mkconfig.sh to generate config.c to record build and version information. Then the object files config.o, satch.o and main.o are compiled. The first two are combined to form the library libsatch.a which is linked against main.o to produce the solver binary satch. The test target will call the shell script tatch.sh, which performs tests on CNFs in cnfs. See below for information on testing and debugging.

See ./configure -h for build options and after building the solver satch -h for run-time options of the solver (solver usage is also shown at the top of main.c). For debugging you can use ./configure -g and optionally then at run-time also enable logging with ./satch -l.

Testing

For testing and debugging the following are used:

cnfs directory containing CNF files for testing catch.[ch] internal proof checker for testing and debugging testapi.c simple separate preliminary API test suite tatch.sh test suite for CNFs in cnfs and building testapi testapi binary built from testapi.c by tatch.sh

Furthermore, as we are having many different combinations of configurations, testing them is non-trivial and is achieved with the following:

combi4.sh complete 4-fold combinatorial testing of configurations gencombi.c generates configurations ("eat your own dogfood") gencombi binary built from gencombi.c (by make test) checkconfig.sh checks configurations (e.g., produced by gencombi)

Here are potential flows for testing configurations:

./combi.sh # Configure and test all 4-fold combinations # of configuration options (does not need gencombi). # Invalid combinations are tested too!

The previous command does not require gencombi and thus can be run without executing a preliminary build. Alternatively, the more flexible combinatorial testing flow does require ./configure && make gencombi first (or just ./configure && make which also builds gencombi):

./gencombi | ./checkconfig.sh # covers all valid pairs ./gencombi -a 4 | ./checkconfig.sh # 4-fold valid combinations ./gencombi -a 9 | ./checkconfig.sh # 9-fold valid combinations ./gencombi -a -i 2 | ./checkconfig.sh -i # check invalid option pairs

The first of these uses the SAT solver to generate a set of configurations which covers all valid pairs of options and at the same time makes sure that there is a configuration which does not contain it. It is also executed by the 'pairwise' make goal which also triggers the last command.

Armin Biere
February 2021