cadical - Man Page

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]

--backbone=0..2

binary clause backbone [1]

--backboneeffort=0..1e5

binary effort in per mile [20]

--backbonemaxrounds=0..1e5 backbone rounds limit [1e3]

--backbonerounds=0..1e5

backbone rounds limit [100]

--backbonethresh=0..1e9

delay if ticks smaller thresh*clauses [5]

--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]

--bumpreasonlimit=1..2e9

bump reason limit [10]

--bumpreasonrate=1..2e9

bump reason decision rate [100]

--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=0..3

1=drat, 2=lrat, 3=both [3]

--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]

--conditioneffort=1..1e5

relative efficiency per mille [100]

--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 [0]

--congruence=bool

congruence closure [true]

--congruenceand=bool

extract AND gates [true]

--congruenceandarity=2..5e7 AND gate arity limit [1e6]

--congruencebinaries=bool

extract binary and strengthen ternary clauses [true]

--congruenceite=bool

extract ITE gates [true]

--congruencexor=bool

extract XOR gates [true]

--congruencexorarity=2..31 XOR gate arity limit [4]

--congruencexorcounts=1..5e6 XOR gate round [1]

--cover=bool

covered clause elimination [false]

--covereffort=1..1e5

relative efficiency per mille [4]

--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 [0]

--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]

--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]

--elimdef=bool

mine definitions with kitten [false]

--elimdefcores=1..100

number of unsat cores [1]

--elimdefticks=0..2e9

kitten ticks limit [2e5]

--elimeffort=1..1e5

relative efficiency per mille [1e3]

--elimequivs=bool

find equivalence gates [true]

--elimint=1..2e9

elimination interval [2e3]

--elimites=bool

find if-then-else gates [true]

--elimlimited=bool

limit resolutions [true]

--elimmaxeff=0..2e9

maximum elimination efficiency [2e9]

--elimmineff=0..2e9

minimum elimination efficiency [1e7]

--elimocclim=0..2e9

occurrence limit [1e2]

--elimprod=0..1e4

elim score product weight [1]

--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]

--emadecisions=1..2e9

window decision rate [1e5]

--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]

--exteagerreasons=bool

eagerly ask for all reasons (0: only when needed) [true]

--exteagerrecalc=bool

after eagerly asking for reasons recalculate all levels (0: trust the external tool) [true]

--externallrat=bool

external lrat [false]

--factor=bool

bounded variable addition [false]

--factorcandrounds=0..2e9

candidates reduction rounds [2]

--factordelay=0..12

delay bounded variable addition between eliminations [4]

--factoreffort=0..1e6

relative effort per mille [50]

--factoriniticks=1..1e6

initial effort in millions [300]

--factorsize=2..2e9

clause size limit [5]

--factorthresh=0..100

delay if ticks smaller thresh*clauses [7]

--factorunbump=bool

extension variable with lowest importance [1: as in kissat] [true]

--fastelim=bool

fast BVE during preprocessing [true]

--fastelimbound=1..1e3

fast BVE bound during preprocessing [8]

--fastelimclslim=2..2e9

fast BVE resolvent size limit [1e2]

--fastelimocclim=1..2e9

fast BVE occurence limit during preprocessing [100]

--fastelimrounds=1..512

number of fastelim rounds [4]

--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]

--frat=0..2

1=frat(lrat), 2=frat(drat) [0]

--idrup=bool

incremental proof format [false]

--ilb=0..2

ILB (incremental lazy backtrack) (0: no, 1: assumptions only, 2: everything) [0]

--incdecay=0..4

decay clauses when doing incremental clauses [1]

--incdecayint=1..2e9

decay interval when doing incremental clauses [1e6]

--inprobeint=1..2e9

inprobing interval [100]

--inprobing=bool

enable probe inprocessing [true]

--inprocessing=bool

enable general 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]

--lidrup=bool

linear incremental proof format [false]

--lrat=bool

use LRAT proof format [false]

--lucky=bool

lucky phases [true]

--luckyassumptions=bool

lucky phases with assumptions [true]

--luckyearly=bool

lucky phases before preprocessing [true]

--luckylate=bool

lucky phases after preprocessing [true]

--minimize=bool

minimize learned clauses [true]

--minimizedepth=0..1e3

minimization depth [1e3]

--minimizeticks=bool

increment ticks in minimization [true]

--otfs=bool

on-the-fly self subsumption [true]

--phase=bool

initial phase [true]

--preprocessinit=0..2e9

initial preprocessing base limit [2e6]

--preprocesslight=bool

lightweight preprocessing [true]

--probe=bool

failed literal probing [true]

--probeeffort=1..1e5

relative efficiency per mille [8]

--probehbr=bool

learn hyper binary clauses [true]

--probethresh=0..100

delay if ticks smaller thresh*clauses [0]

--profile=0..4

profiling level [2]

--quiet=bool

disable all messages [false]

--radixsortlim=0..2e9

radix sort limit [32]

--randec=bool

random decisions [false]

--randecfocused=bool

random decisions in focused mode [true]

--randecinit=2..2e9

inital random decision interval [1e3]

--randecint=0..2e9

random conflict length [500]

--randeclength=1..1e9

length random decisions phases [10]

--randecstable=bool

random decisions in stable mode [false]

--realtime=bool

real instead of process time [false]

--recomputetier=bool

recompute tiers [true]

--reduce=bool

reduce useless clauses [true]

--reduceinit=1..1e6

initial interval [300]

--reduceint=2..1e6

reduce interval [25]

--reduceopt=0..2

0=prct,1=sqrt,2=max [1]

--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=bool

stable reluctant doubling restarts [true]

--reluctantint=0..2e9

reluctant doubling period [1024]

--reluctantmax=0..2e9

maximum reluctant doubling period [1048576]

--rephase=0..2

enable resetting phase (0=no,1=always,2=stable-only) [1]

--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]

--restartmarginfocused=0..25 focused slow fast margin in percent [10]

--restartmarginstable=0..25 stable slow fast margin in percent [25]

--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 (1=binary-only,2=minimize-on-pulling,3=full) [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]

--stabilizeinit=1..2e9

stabilizing interval [1e3]

--stabilizeonly=bool

only stabilizing phases [false]

--stats=bool

print all statistics at the end of the run [false]

--stubbornIOfocused=bool

force phases to I/O in focused mode every once in a while (requires rephase==2) [false]

--subsume=bool

enable clause subsumption [true]

--subsumebinlim=0..2e9

watch list length limit [1e4]

--subsumeclslim=0..2e9

clause length limit [1e2]

--subsumeeffort=1..1e5

relative efficiency per mille [1e3]

--subsumelimited=bool

limit subsumption checks [true]

--subsumemaxeff=0..2e9

maximum subsuming efficiency [1e8]

--subsumemineff=0..2e9

minimum subsuming efficiency [0]

--subsumeocclim=0..2e9

watch list length limit [1e2]

--subsumestr=bool

subsume strengthen [true]

--sweep=bool

enable SAT sweeping [true]

--sweepclauses=0..2e9

environment clauses [1024]

--sweepcomplete=bool

run SAT sweeping to completion [false]

--sweepcountbinary=bool

count binaries to environment [true]

--sweepdepth=0..2e9

environment depth [2]

--sweepeffort=0..1e4

relative effort in ticks per mille [1e2]

--sweepfliprounds=0..2e9

flipping rounds [1]

--sweepmaxclauses=2..2e9

maximum environment clauses [3e5]

--sweepmaxdepth=1..2e9

maximum environment depth [3]

--sweepmaxvars=2..2e9

maximum environment variables [8192]

--sweeprand=bool

randomize sweeping environment [false]

--sweepthresh=0..100

delay if ticks smaller thresh*clauses [5]

--sweepvars=0..2e9

environment variables [256]

--target=0..2

target phases (1=stable only) [1]

--terminateint=0..1e4

termination check interval [10]

--ternary=bool

hyper ternary resolution [true]

--ternaryeffort=1..1e5

relative efficiency per mille [8]

--ternarymaxadd=0..1e4

max clauses added in percent [1e3]

--ternaryocclim=1..2e9

ternary occurrence limit [1e2]

--ternaryrounds=1..16

maximum ternary rounds [2]

--ternarythresh=0..100

delay if ticks smaller thresh*clauses [6]

--tier1limit=0..100

limit of tier1 usage in percentage [50]

--tier1minglue=0..100

lowest tier1 limit [0]

--tier2limit=0..100

limit of tier2 usage in percentage [90]

--tier2minglue=0..100

lowest tier2 limit [0]

--transred=bool

transitive reduction of BIG [true]

--transredeffort=1..1e5

relative efficiency per mille [1e2]

--transredmaxeff=0..2e9

maximum efficiency [1e8]

--transredmineff=0..2e9

minimum efficiency [0]

--verbose=0..3

more verbose messages [0]

--veripb=0..4

odd=check-deletions, >2 drat [0]

--vivify=bool

vivification [true]

--vivifycalctier=bool

recalculate tier limits [false]

--vivifydemote=bool

demote irredundant or delete directly [false]

--vivifyeffort=0..1e5

overall efficiency per mille [50]

--vivifyflush=bool

flush subsumed before vivification rounds [true]

--vivifyinst=bool

instantiate last literal when vivify [true]

--vivifyirred=bool

vivification of irredundant clauses [true]

--vivifyirredeff=1..100

irredundant efficiency per mille [3]

--vivifyonce=0..2

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

--vivifyretry=0..5

re-vivify clause if vivify was successful [0]

--vivifyschedmax=10..2e9

maximum schedule size [5e3]

--vivifythresh=0..100

delay if ticks smaller thresh*clauses [20]

--vivifytier1=bool

vivification tier1 [true]

--vivifytier1eff=0..100

relative tier1 effort [4]

--vivifytier2=bool

vivification tier2 [true]

--vivifytier2eff=1..100

relative tier2 effort [2]

--vivifytier3=bool

vivification tier3 [true]

--vivifytier3eff=1..100

relative tier3 effort [1]

--walk=bool

enable random walks [true]

--walkeffort=1..1e5

relative efficiency per mille [80]

--walkfullocc=bool

use Kissat's full occurrences instead of the single watched [false]

--walkmaxeff=0..2e9

maximum efficiency (in 1e3 ticks) [1e7]

--walkmineff=0..1e7

minimum efficiency [0]

--walknonstable=bool

walk in non-stabilizing phase [true]

--walkredundant=bool

walk redundant clauses too [false]

--warmup=bool

warmup before walk using propagation [true]

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.