Sat Solver SATCH

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

The actual version number can be found in VERSION and changes in the latest release are documented in NEWS.md.

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 particularly Kissat, while still featuring most important implementation techniques needed to obtain a state-of-the-art SAT solver. However, even though current version has bounded variable elimination implemented, which is arguably the most important preprocessing and inprocessing procedure, but still lacks other preprocessing techniques and only supports incremental solving partially.

The code and its documentation is also meant to serve as a gentle introduction into the code base of CaDiCaL and Kissat.

It is possible to switch off general and more basic features at compile time by using different options to configure. 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 is the stand-alone solver binary
• satch.h is the solver API similar to IPASIR
• libsatch.a is the library with API in satch.h

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

• satch.c provides the library code of the SAT solver
• features.h checks consistency of feature selection
• colors.h defines shared code for using terminal colors
• rsort.h is a generic radix sort implementation (header file only)
• stack.h is a generic stack implementation (header file only)
• queue.h simplistic queue implementation (header file only)
• config.c provides build-information generated by mkconfig.sh
• main.c contains application code with parser and witness printer

In the features sub-directory reside the followings files read by features.h:

• features/check.h checks implied and clashing options
• features/diagnose.h diagnoses and print final set of options
• features/init.h initializes additional (implied) options

You might want to consult features/README.md for more information on their meaning and how they are generated.

The files used by the build process are the following:

• VERSION contains current version
• configure is the configuration utility
• .config saved last configuration
• makefile.in is a makefile template used by configure
• makefile is generated from makefile.in by configure
• mkconfig.sh generates config.c to provide build information

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 the cnfs and xnfs directories. See below for information on testing and debugging.

Refer to ./configure -h for build options and after building the solver to ./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
• xnfs directory containing XNF files for testing
• catch.h header file of internal proof checker for testing and debugging
• catch.c implementation of internal proof checker for testing and debugging
• testapi.c simple separate (preliminary) API test suite
• tatch.sh test suite for CNFs in cnfs and xnfs and for building and running testapi
• testapi binary built from testapi.c by tatch.sh

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

• 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)

We have a flexible combinatorial testing flow which uses gencombi to produce sets of configurations that can be tested with checkconfig.sh:

./gencombi         | ./checkconfig.sh    # covers all valid pairs
./gencombi -a 2    | ./checkconfig.sh    # 2-fold valid combinations
./gencombi -a 3    | ./checkconfig.sh    # 3-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. There are also corresponding make goals test-two-ways, test-all-pairs, and test-all-triples.

Armin Biere
May 2021