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.
