cadical - Man Page

manual page for cadical 1.2.1


usage: cadical [ <option> ... ] [ <dimacs> [ <proof> ] ]

where '<option>' is one of the following common options


list of common options


list of advanced options


print version


do not print witness (same as '--no-witness')


increase verbosity (see also '--verbose')


be quiet (same as '--quiet')

-t <sec>

set wall clock time limit

or one of the less common options


increase limits by '{2,10}^<level>' (default '0')


enable preprocessing initially (default '0' rounds)


run local search initialially (default '0' rounds)

-c <limit>

limit the number of conflicts (default unlimited)

-d <limit>

limit the number of decisions (default unlimited)

-o <dimacs>

write simplified CNF in DIMACS format to file

-e <extend>

write reconstruction/extension stack to file

-f | --force

parse completely broken DIMACS header


enforce strict parsing

-s <sol>

read solution in competition output format to check consistency of learned clauses during testing and debugging


force colored output


disable colored output to terminal


do not print witness (see also '-n' above)


print build configuration


print copyright information

or '<option>' is one of the following advanced internal options


allocate clauses in arena [true]


keep clauses compact [true]


sort clauses in arena [true]


1=clause, 2=var, 3=queue [3]


use binary proof format [true]


blocked clause elimination [false]


maximum clause size [1e5]


minimum clause size [4]


occurrence limit [1e2]


bump variables [true]


bump reason literals too [true]


bump reason depth [1]


enable internal checking [false]


check assumptions satisfied [true]


check failed literals form core [true]


check all frozen semantics [false]


check proof internally [true]


check witness internally [true]


chronological backtracking [1]


force always chronological [false]


chronological level limit [1e2]


reuse trail chronologically [true]


compact internal variables [true]


compacting interval [2e3]


inactive limit in per mille [1e2]


minimum inactive limit [1e2]


globally blocked clause elim [false]


initial conflict interval [1e4]


maximum condition efficiency [1e7]

--conditionmaxratio=1..2e9 maximum clause variable ratio [100]


minimum condition efficiency [1e6]


relative efficiency in per mille [100]


covered clause elimination [false]


maximum clause size [1e5]


maximum cover efficiency [1e8]


minimum clause size [4]


minimum cover efficiency [1e6]


relative efficiency per mille [4]


decompose BIG in SCCs and ELS [true]


number of decompose rounds [2]


remove duplicated binary clauses [true]


subsume eagerly recently learned [true]


limit on subsumed candidates [20]


bounded variable elimination [true]


find AND gates [true]


maximum elimination efficiency [2e9]


eager backward subsumption [true]


maximum elimination bound [16]


minimum elimination bound [0]


resolvent size limit [1e2]


find equivalence gates [true]


minimum elimination efficiency [1e7]


elimination interval [2e3]


find if-then-else gates [true]


limit resolutions [true]


occurrence limit [1e3]


elimination score product [1]


relative efficiency per mille [1e3]


usual number of rounds [2]


elimination by substitution [true]


maximum XOR size [5]


find XOR gates [true]


window fast glue [33]


window slow glue [1e5]


window back-jump level [1e5]


window back-track level [1e5]


window learned clause size [1e5]


window fast trail [1e2]


window slow trail [1e5]


flush redundant clauses [false]


interval increase [3]


initial limit [1e5]


always use initial phase [false]


enable inprocessing [true]


variable instantiation [false]

--instantiateclslim=2..2e9 minimum clause size [3]

--instantiateocclim=1..2e9 maximum occurrence limit [1]


instantiate each clause once [true]


search for lucky phases [true]


minimize learned clauses [true]


minimization depth [1e3]


initial phase [true]


failed literal probing [true]


learn hyper binary clauses [true]


probing interval [5e3]


maximum probing efficiency [1e8]


minimum probing efficiency [1e6]


relative efficiency per mille [20]


probing rounds [1]


profiling level [2]


disable all messages [false]


radix sort limit [800]


real instead of process time [false]


reduce useless clauses [true]


reduce interval [300]


reduce fraction in percent [75]


glue of kept learned clauses [2]


glue of tier two clauses [6]


reluctant doubling period [1024]


reluctant doubling period [1048576]


enable resetting phase [true]


rephase interval [1e3]


enable reporting [true]


report even if not successful [false]


use solving not process time [false]


enable restarts [true]


restart interval [2]


slow fast margin in percent [10]


enable trail reuse [true]


restore all clauses (2=really) [0]


remove satisfied clauses [false]


reverse variable ordering [false]


use EVSIDS scores [true]


score factor per mille [950]


random seed [0]


shuffle variables [false]


shuffle variable queue [true]


not reverse but random [false]


shuffle variable scores [true]


enable simplifier [true]


enable stabilizing phases [true]

--stabilizefactor=101..2e9 phase increase in percent [200]


stabilizing interval [1e3]


maximum stabilizing phase [2e9]


only stabilizing phases [false]


use target variable phase [true]


enable clause subsumption [true]


watch list length limit [1e4]


clause length limit [1e3]


subsume interval [1e4]


limit subsumption checks [true]


maximum subsuming efficiency [1e8]


minimum subsuming efficiency [1e6]


watch list length limit [1e2]


relative efficiency per mille [1e3]


strengthen during subsume [true]


hyper ternary resolution [true]


maximum clauses added in percent [1e3]


ternary maximum efficiency [1e8]


minimum ternary efficiency [1e6]


ternary occurrence limit [1e2]


relative efficiency in per mille [10]


maximum ternary rounds [2]


transitive reduction of BIG [true]


maximum efficiency [1e8]


minimum efficiency [1e6]


relative efficiency per mille [1e2]


more verbose messages [0]


vivification [true]


maximum efficiency [1e8]


minimum efficiency [1e5]


vivify once: 1=red, 2=red+irr [0]


redundant efficiency per mille [300]


relative efficiency per mille [80]


enable random walks [true]


maximum efficiency [1e7]


minimum efficiency [1e5]


walk in non-stabilizing phase [true]


walk redundant clauses too [false]


relative efficiency per mille [20]

The internal options have their default value printed in brackets after their description.  They can also be used in the form '--<name>' which is equivalent to '--<name>=1' and in the form '--no-<name>' which is equivalent to '--<name>=0'.  One can also use 'true' instead of '1', 'false' instead of '0', as well as numbers with positive exponent such as '1e3' instead of '1000'.

Alternatively option values can also be specified in the header of the DIMACS file, e.g., 'c --elim=false', or through environment variables, such as 'CADICAL_ELIM=false'.  The embedded options in the DIMACS file have highest priority, followed by command line options and then values specified through environment variables.

There are also the following pre-defined configurations of options


target satisfiable instances


target unsatisfiable instances

The input is read from '<dimacs>' assumed to be in DIMACS format. If '<proof>' is given then a DRAT proof is written to that file.

If '<dimacs>' is missing then the solver reads from '<stdin>', also if '-' is used as input path name '<dimacs>'.  Similarly, if '-' is specified as '<proof>' path then a proof is generated and printed to '<stdout>'.

By default the proof is stored in the binary DRAT format unless the option '--no-binary' is specified or the proof is written to  '<stdout>' and '<stdout>' is connected to a terminal.

The input is assumed to be compressed if it is given explicitly and has a '.gz', '.bz2', '.xz' or '.7z' suffix.  The same applies to the output file.  In order to use compression and decompression the corresponding utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are required and need to be installed on the system.


January 2020 cadical 1.2.1