NAME

cadical - CaDiCaL Simplified Satisfiability Solver

DESCRIPTION

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

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

-h: print alternatively only a list of common options
--help: print this complete list of all options
--version: print version
-n: do not print witness (same as '--no-witness')
-v: increase verbosity (see also '--verbose' below)
-q: be quiet (same as '--quiet')
-t <sec>: set wall clock time limit

Or '<option>' is one of the less common options

-L<rounds>: run local search initially (default '0' rounds)
-O<level>: increase limits by '2^<level>' or '10^<level>'
-P<rounds>: initial preprocessing (default '0' rounds)

Note there is no separating space for the options above while the following options require a space after the option name:

-c <limit>: limit the number of conflicts (default unlimited)
-d <limit>: limit the number of decisions (default unlimited)
-o <output>: write simplified CNF in DIMACS format to file
-e <extend>: write reconstruction/extension stack to file
--force | -f: parsing broken DIMACS header and writing proofs
--strict: strict parsing (no white space in header)
-r <sol>: read solution in competition output format to check consistency of learned clauses during testing and debugging
-w <sol>: write result including a potential witness solution in competition format to the given file
--colors: force colored output
--no-colors: disable colored output to terminal
--no-witness: do not print witness (see also '-n' above)
--build: print build configuration
--copyright: print copyright information

There are pre-defined configurations of advanced internal options:

--default: set default advanced internal options
--plain: disable all internal preprocessing options
--sat: set internal options to target satisfiable instances
--unsat: set internal options to target unsatisfiable instances

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

--arena=bool: allocate clauses in arena [true]
--arenacompact=bool: keep clauses compact [true]
--arenasort=bool: sort clauses in arena [true]
--arenatype=1..3: 1=clause, 2=var, 3=queue [3]
--binary=bool: use binary proof format [true]
--block=bool: blocked clause elimination [false]
--blockmaxclslim=1..2e9: maximum clause size [1e5]
--blockminclslim=2..2e9: minimum clause size [2]
--blockocclim=1..2e9: occurrence limit [1e2]
--bump=bool: bump variables [true]
--bumpreason=bool: bump reason literals too [true]
--bumpreasondepth=1..3: bump reason depth [1]
--check=bool: enable internal checking [false]
--checkassumptions=bool: check assumptions satisfied [true]
--checkconstraint=bool: check constraint satisfied [true]
--checkfailed=bool: check failed literals form core [true]
--checkfrozen=bool: check all frozen semantics [false]
--checkproof=bool: check proof internally [true]
--checkwitness=bool: check witness internally [true]
--chrono=0..2: chronological backtracking [1]
--chronoalways=bool: force always chronological [false]
--chronolevelim=0..2e9: chronological level limit [1e2]
--chronoreusetrail=bool: reuse trail chronologically [true]
--compact=bool: compact internal variables [true]
--compactint=1..2e9: compacting interval [2e3]
--compactlim=0..1e3: inactive limit per mille [1e2]
--compactmin=1..2e9: minimum inactive limit [1e2]
--condition=bool: globally blocked clause elim [false]
--conditionint=1..2e9: initial conflict interval [1e4]
--conditionmaxeff=0..2e9: maximum condition efficiency [1e7]
--conditionmaxrat=1..2e9: maximum clause variable ratio [100]
--conditionmineff=0..2e9: minimum condition efficiency [1e6]
--conditionreleff=1..1e5: relative efficiency per mille [100]
--cover=bool: covered clause elimination [false]
--covermaxclslim=1..2e9: maximum clause size [1e5]
--covermaxeff=0..2e9: maximum cover efficiency [1e8]
--coverminclslim=2..2e9: minimum clause size [2]
--covermineff=0..2e9: minimum cover efficiency [1e6]
--coverreleff=1..1e5: relative efficiency per mille [4]
--decompose=bool: decompose BIG in SCCs and ELS [true]
--decomposerounds=1..16: number of decompose rounds [2]
--deduplicate=bool: remove duplicated binaries [true]
--eagersubsume=bool: subsume recently learned [true]
--eagersubsumelim=1..1e3: limit on subsumed candidates [20]
--elim=bool: bounded variable elimination [true]
--elimands=bool: find AND gates [true]
--elimaxeff=0..2e9: maximum elimination efficiency [2e9]
--elimbackward=bool: eager backward subsumption [true]
--elimboundmax=-1..2e6: maximum elimination bound [16]
--elimboundmin=-1..2e6: minimum elimination bound [0]
--elimclslim=2..2e9: resolvent size limit [1e2]
--elimequivs=bool: find equivalence gates [true]
--elimineff=0..2e9: minimum elimination efficiency [1e7]
--elimint=1..2e9: elimination interval [2e3]
--elimites=bool: find if-then-else gates [true]
--elimlimited=bool: limit resolutions [true]
--elimocclim=0..2e9: occurrence limit [1e2]
--elimprod=0..1e4: elim score product weight [1]
--elimreleff=1..1e5: relative efficiency per mille [1e3]
--elimrounds=1..512: usual number of rounds [2]
--elimsubst=bool: elimination by substitution [true]
--elimsum=0..1e4: elimination score sum weight [1]
--elimxorlim=2..27: maximum XOR size [5]
--elimxors=bool: find XOR gates [true]
--emagluefast=1..2e9: window fast glue [33]
--emaglueslow=1..2e9: window slow glue [1e5]
--emajump=1..2e9: window back-jump level [1e5]
--emalevel=1..2e9: window back-track level [1e5]
--emasize=1..2e9: window learned clause size [1e5]
--ematrailfast=1..2e9: window fast trail [1e2]
--ematrailslow=1..2e9: window slow trail [1e5]
--flush=bool: flush redundant clauses [false]
--flushfactor=1..1e3: interval increase [3]
--flushint=1..2e9: initial limit [1e5]
--forcephase=bool: always use initial phase [false]
--inprocessing=bool: enable inprocessing [true]
--instantiate=bool: variable instantiation [false]

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

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

--instantiateonce=bool: instantiate each clause once [true]
--lucky=bool: search for lucky phases [true]
--minimize=bool: minimize learned clauses [true]
--minimizedepth=0..1e3: minimization depth [1e3]
--phase=bool: initial phase [true]
--probe=bool: failed literal probing [true]
--probehbr=bool: learn hyper binary clauses [true]
--probeint=1..2e9: probing interval [5e3]
--probemaxeff=0..2e9: maximum probing efficiency [1e8]
--probemineff=0..2e9: minimum probing efficiency [1e6]
--probereleff=1..1e5: relative efficiency per mille [20]
--proberounds=1..16: probing rounds [1]
--profile=0..4: profiling level [2]
--quiet=bool: disable all messages [false]
--radixsortlim=0..2e9: radix sort limit [800]
--realtime=bool: real instead of process time [false]
--reduce=bool: reduce useless clauses [true]
--reduceint=10..1e6: reduce interval [300]
--reducetarget=10..1e2: reduce fraction in percent [75]
--reducetier1glue=1..2e9: glue of kept learned clauses [2]
--reducetier2glue=1..2e9: glue of tier two clauses [6]
--reluctant=0..2e9: reluctant doubling period [1024]
--reluctantmax=0..2e9: reluctant doubling period [1048576]
--rephase=bool: enable resetting phase [true]
--rephaseint=1..2e9: rephase interval [1e3]
--report=bool: enable reporting [false]
--reportall=bool: report even if not successful [false]
--reportsolve=bool: use solving not process time [false]
--restart=bool: enable restarts [true]
--restartint=1..2e9: restart interval [2]
--restartmargin=0..1e2: slow fast margin in percent [10]
--restartreusetrail=bool: enable trail reuse [true]
--restoreall=0..2: restore all clauses (2=really) [0]
--restoreflush=bool: remove satisfied clauses [false]
--reverse=bool: reverse variable ordering [false]
--score=bool: use EVSIDS scores [true]
--scorefactor=500..1e3: score factor per mille [950]
--seed=0..2e9: random seed [0]
--shrink=0..3: shrink conflict clause [3]
--shrinkreap=bool: use a reap for shrinking [true]
--shuffle=bool: shuffle variables [false]
--shufflequeue=bool: shuffle variable queue [true]
--shufflerandom=bool: not reverse but random [false]
--shufflescores=bool: shuffle variable scores [true]
--stabilize=bool: enable stabilizing phases [true]

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

--stabilizeint=1..2e9: stabilizing interval [1e3]
--stabilizemaxint=1..2e9: maximum stabilizing phase [2e9]
--stabilizeonly=bool: only stabilizing phases [false]
--subsume=bool: enable clause subsumption [true]
--subsumebinlim=0..2e9: watch list length limit [1e4]
--subsumeclslim=0..2e9: clause length limit [1e2]
--subsumeint=1..2e9: subsume interval [1e4]
--subsumelimited=bool: limit subsumption checks [true]
--subsumemaxeff=0..2e9: maximum subsuming efficiency [1e8]
--subsumemineff=0..2e9: minimum subsuming efficiency [1e6]
--subsumeocclim=0..2e9: watch list length limit [1e2]
--subsumereleff=1..1e5: relative efficiency per mille [1e3]
--subsumestr=bool: strengthen during subsume [true]
--target=0..2: target phases (1=stable only) [1]
--terminateint=0..1e4: termination check interval [10]
--ternary=bool: hyper ternary resolution [true]
--ternarymaxadd=0..1e4: max clauses added in percent [1e3]
--ternarymaxeff=0..2e9: ternary maximum efficiency [1e8]
--ternarymineff=1..2e9: minimum ternary efficiency [1e6]
--ternaryocclim=1..2e9: ternary occurrence limit [1e2]
--ternaryreleff=1..1e5: relative efficiency per mille [10]
--ternaryrounds=1..16: maximum ternary rounds [2]
--transred=bool: transitive reduction of BIG [true]
--transredmaxeff=0..2e9: maximum efficiency [1e8]
--transredmineff=0..2e9: minimum efficiency [1e6]
--transredreleff=1..1e5: relative efficiency per mille [1e2]
--verbose=0..3: more verbose messages [0]
--vivify=bool: vivification [true]
--vivifymaxeff=0..2e9: maximum efficiency [2e7]
--vivifymineff=0..2e9: minimum efficiency [2e4]
--vivifyonce=0..2: vivify once: 1=red, 2=red+irr [0]
--vivifyredeff=0..1e3: redundant efficiency per mille [75]
--vivifyreleff=1..1e5: relative efficiency per mille [20]
--walk=bool: enable random walks [true]
--walkmaxeff=0..2e9: maximum efficiency [1e7]
--walkmineff=0..1e7: minimum efficiency [1e5]
--walknonstable=bool: walk in non-stabilizing phase [true]
--walkredundant=bool: walk redundant clauses too [false]
--walkreleff=1..1e5: 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.

The input is read from '<input>' assumed to be in DIMACS format. Incremental 'p inccnf' files are supported too with cubes at the end. If '<proof>' is given then a DRAT proof is written to that file.

If '<input>' is missing then the solver reads from '<stdin>', also if '-' is used as input path name '<input>'. Similarly,

For incremental files each cube is solved in turn. The solver stops at the first satisfied cube if there is one and uses that one for the witness to print. Conflict and decision limits are applied to each individual cube solving call while '-P', '-L' and '-t' remain global. Only if all cubes were unsatisfiable the solver prints the standard unsatisfiable solution line ('s UNSATISFIABLE').

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. The solver checks file type signatures though and falls back to non-compressed file reading if the signature does not match.

November 2022

cadical 1.5.3