CaDiCaL Simplified Satisfiability Solver with FRAT-Style and LRAT-Style Proofs for Distributed Solvers
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.
The solver has the following usage cadical [ dimacs [ proof ] ]
.
See cadical -h
for more options.
The distributed solver implementation is used to produce UNSAT proofs for distributed, clause-sharing SAT solvers.
Because we are using FRAT and LRAT proofs for this, we need to create a clause ID for each clause that is unique across all solvers.
We generate the clause ID needed for clauses based on a formula: o + i + t * k
where
o
: number of original clausest
: total number of solvers runningi
: instance number of current solver (1
,2
, ...t
)k
: number of clauses generated by this instance (0
,1
,2
, ...)
Our algorithm for combining the proofs produced by various solver instances requires each added clause in the proof to have a proof hint.
However, not all techniques in CaDiCaL have proof hints being produced currently.
Therefore we have these techniques turned off, and require preprocessing the file with cadical <input.cnf> -c 0 -o <output.cnf>
before solving in order to produce valid proofs for composition.
In modifying CaDiCaL to work for distributed proof production, we also added two additional options for the proof output, in addition to those noted below:
--lrat
: If set totrue
, output the proofs in LRAT format rather than FRAT or DRAT. Since we require proof hints in the output, using FRAT is just using LRAT but with more characters. Therefore we added an LRAT option. This is set totrue
(produce LRAT proofs) by default.--proofdelete
: If set totrue
, output the delete lines into the proof; if set tofalse
, ignore delete lines and do not put them in the proof. Our proof composition ignores the clause deletions done by solvers during solving, since one solver might delete a clause while another is still using it. Therefore writing them to the proof is a waste if we are only going to use the proof for combining. This is set totrue
(produce the delete lines) by default.
The changes break down into the following parts:
-
Clause IDs were previously only enabled if you compile with the
LOGGING
preprocessor flag. Now they are required. -
Clause IDs are passed around in lots of places, changing many function signatures to include a
int64_t id
argument. -
A
chain
global variable is used to hold on to the proof of the clause that is about to be added. The way this variable gets filled depends on the proof step and is the most "creative" part of the modification. -
On code paths that do not provide proofs because I wasn't able to see an easy way to do it or I couldn't figure out the code, there is a call to the
PROOF_TODO (proof, reason, todo_id)
macro. Thereason
is a short description of the code path and appears only in logs, while thetodo_id
is a number that appears in at <todo_id> 0
step that is emitted as part of the FRAT proof. These steps can be analyzed by the FRAT toolchain to find out which code paths are most common / worth more thorough investigation. -
Unit literals are also clauses in the FRAT format, but CaDiCaL treats them separately. These also need IDs, and this is the function of the
unit_id
field inVar
, which is the ID of the clause that proves or disproves the literal, if it is fixed, and0
otherwise. -
There are some new functions to
finalize
a clause. The main function isInternal::finalize ()
. This is done after a proof ofunsat
is found, and just dumps the list of all clauses that are not yet deleted at the point that theunsat
is found. -
The actual formatting of the FRAT file on disk is performed by
tracer.cpp
. This implementation supports both ASCII and binary versions of the FRAT format; the binary version is default and the ASCII version is enabled with--frat=true --binary=false
. -
There are also some changes to
drat-trim.c
, which is used by the test harness, to make sure that it does not fail with exit code 0.