CaDiCaL Simplified Satisfiability Solver

This is a modified version of the original CaDiCaL repository on GitHub. We are releasing this version of CaDiCaL as a fork of the original CaDiCaL repository because this is preferred by the original author, Armin Biere. The version of CaDiCaL presented here can store the most relevant parts of its state (irredundant clauses, redundant clauses, and the reconstruction stack) in files, and it can also read this state from files at startup. This allows you to stop CaDiCaL in the middle of a run (e.g., by specifying a timeout via the -t argument), store its state, and later resume the solver run by loading the previously stored state. Details are described in the paper Migrating Solver State (Armin Biere, Md Solimul Chowdhury, Marijn J.H. Heule, Benjamin Kiesl, and Michael W. Whalen; SAT 2022). For usage instructions on storing and restoring state, see the end of this README.

The goal of the development of CaDiCaL was to obtain a CDCL solver which is easy to understand and change, while at the same time not being much slower than other state-of-the-art CDCL solvers.

Originally we wanted to also radically simplify the design and internal data structures, but that goal was only achieved partially, at least for instance compared to Lingeling.

However, the code is much better documented and CaDiCaL actually became in general faster than Lingeling even though it is missing some preprocessors (mostly parity and cardinality constraint reasoning), which would be crucial to solve certain instances.

Use ./configure && make to configure and build cadical and the library libcadical.a in the default build sub-directory. The header file of the library is src/cadical.hpp and includes an example for API usage.

See BUILD.md for options and more details related to the build process and test/README.md for testing the library and the solver. Since release 1.5.1 we have a NEWS.md file.

The solver has the following usage cadical [ dimacs [ proof ] ]. See cadical -h for more options.

If you want to cite CaDiCaL please use the solver description in the latest SAT competition proceedings:

  @inproceedings{BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers,
    author    = {Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger},
    title     = {{CaDiCaL}, {Kissat}, {Paracooba}, {Plingeling} and {Treengeling}
		 Entering the {SAT Competition 2020}},
    pages     = {51--53},
    editor    = {Tomas Balyo and Nils Froleyks and Marijn Heule and 
		 Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
    booktitle = {Proc.~of {SAT Competition} 2020 -- Solver and Benchmark Descriptions},
    volume    = {B-2020-1},
    series    = {Department of Computer Science Report Series B},
    publisher = {University of Helsinki},
    year      = 2020,
  }

You might also find more information on CaDiCaL at http://fmv.jku.at/cadical.

Armin Biere

Storing and Restoring State

Use the following command-line arguments for storing and restoring state (file formats for state are described further down):

• --ic-out <irredundant-clause-file>: write irredundant clauses to file <learned-clause-file> at the end of the solver run.
• Read irredundant clauses from a file by just passing them as input formula to the solver.
• --lc-out <learned-clause-file>: write learned clauses to file <learned-clause-file> at the end of the solver run.
• --lc-in <learned-clause-file>: read learned clauses from file <learned-clause-file> at startup.
• --rs-out <reconstruction-stack-file>: write reconstruction stack to file <reconstruction-stack-file> at the end of the solver run.
• --rs-in <reconstruction-stack-file>: read reconstruction stack from file <reconstruction-stack-file> at startup.
• --state-binary: write state (irredundant clauses, redundant clauses, and reconstruction stack) in binary format, otherwise use plain-text format. Also, if --state-binary is passed to the solver, the reconstruction stack is read in binary format, otherwise it is read in plain-text format. (For irredundant clauses and learned clauses, the corresponding files contain enough information to distinguish between binary/plain-text, so no explicit flag is needed when reading them.)

Example (run CaDiCaL with a timeout of 100 seconds and store state in plain-text format at the end of the solver run):

cadical -t 100 --rs-out <reconstruction-stack-file> --lc-out <learned-clause-file> --ic-out <irredundant-clause-file> <input-formula>

Example (run CaDiCaL with a timeout of 100 seconds and store state in binary format at the end of the solver run):

cadical -t 100 --state-binary --rs-out <reconstruction-stack-file> --lc-out <learned-clause-file> --ic-out <irredundant-clause-file> <input-formula>

Example (read state at startup; reconstruction stack must be passed in plain-text format, learned clauses and irredundant clauses can be passed in either plain-text or binary format):

cadical --rs-in <reconstruction-stack-file> --lc-in <learned-clause-file> <irredundant-clause-file>

Example (read state at startup; reconstruction stack must be passed in binary format, learned clauses and irredundant clauses can be passed in either plain-text or binary format):

cadical --state-binary --rs-in <reconstruction-stack-file> --lc-in <learned-clause-file> <irredundant-clause-file>

File Format for Irredundant Clauses

Irredundant clauses can be stored either in conventional DIMACS format or in a dedicated binary DIMACS format. The binary format relies on the same integer encoding as the binary format of DRAT: Literals are mapped to positive integers that are in turn encoded as variable-length big-endian byte strings (check the paper Migrating Solver State for details).

A binary DIMACS file starts with 0x00, i.e., with a 0-byte (this initial 0-byte allows a solver/parser to identify the file as a binary DIMACS file) and is then followed by a sequence of clauses where each clause is represented by a sequence of integers (encoded in the above-mentioned variable-length encoding) that is followed by 0x00. Similar to DIMACS, positive literals are mapped to positive integers and negative literals are mapped to negative integers before they are encoded.

File Format for Learned Clauses

Each line of a learned-clause file contains the literals of a clause, then a 0, followed by a non-negative integer for the LBD, and finally another 0. More formally, a file is a list of lines, which are defined as follows:

<line> = <clause> "0" <glue> "0\n"
<clause> = <literal>*
<literal> = <number> | -<number>
<glue> = <number>
<number> = [1-9][0-9]*

Example:

1 3 -2 0 1 0
2 1 0 2 0
-3 -4 -5 0 2 0

In the binary format, redundant clauses are serialized in a similar way as irredundant clauses. Files start with a 0-byte and then list the clauses, with the only difference being that for each clause and its corresponding usefulness score U, we add (the variable-length encoding of) U after the clause’s concluding 0-byte.

File Format for the Reconstruction Stack

Reconstruction stacks are serialized bottom-to-top, meaning that clause-witness pairs that occur earlier in the stack will also occur earlier in the file. Each line of a reconstruction-stack file contains the literals of a clause, then a 0, followed by the literals of the witness, and finally another 0. More formally, a file is a list of lines, which are defined as follows:

<line> = <clause> "0" <clause> "0\n"
<clause> = <literal>*
<literal> = <number> | -<number>
<number> = [1-9][0-9]*

In its current version, the solver produces only witnesses with exactly one literal.

Example:

1 3 -2 0 1 0
2 1 0 2 0
-3 -4 -5 0 -3 0

In binary format, we do not start files with a 0-byte. This allows for straight-forward concatenation of multiple reconstruction-stack files, which is often useful. Given a reconstruction stack s = (C₁, w₁),...,(C_n, w_n), we can view it as a list C₁, w₁,...,C_n, w_n of clauses, which is then encoded in the same way as the irredundant clauses, by adding a 0-byte after each clause.