cadical - Man Page

manual page for cadical 1.2.1

Description

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

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

-h

list of common options

--help

list of advanced options

--version

print version

-n

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

-v

increase verbosity (see also '--verbose')

-q

be quiet (same as '--quiet')

-t <sec>

set wall clock time limit

or one of the less common options

-O<level>

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

-P<rounds>

enable preprocessing initially (default '0' rounds)

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

--strict

enforce strict parsing

-s <sol>

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

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

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

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

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

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

--conditionmineff=0..2e9

minimum condition efficiency [1e6]

--conditionreleff=1..1e5

relative efficiency in 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 [4]

--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 binary clauses [true]

--eagersubsume=bool

subsume eagerly 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 [1e3]

--elimprod=0..1e4

elimination score product [1]

--elimreleff=1..1e5

relative efficiency per mille [1e3]

--elimrounds=1..512

usual number of rounds [2]

--elimsubst=bool

elimination by substitution [true]

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

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

--shuffle=bool

shuffle variables [false]

--shufflequeue=bool

shuffle variable queue [true]

--shufflerandom=bool

not reverse but random [false]

--shufflescores=bool

shuffle variable scores [true]

--simplify=bool

enable simplifier [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]

--stabilizephase=bool

use target variable phase [true]

--subsume=bool

enable clause subsumption [true]

--subsumebinlim=0..2e9

watch list length limit [1e4]

--subsumeclslim=0..2e9

clause length limit [1e3]

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

--ternary=bool

hyper ternary resolution [true]

--ternarymaxadd=0..1e4

maximum 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 in 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 [1e8]

--vivifymineff=0..2e9

minimum efficiency [1e5]

--vivifyonce=0..2

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

--vivifyredeff=0..1e3

redundant efficiency per mille [300]

--vivifyreleff=1..1e5

relative efficiency per mille [80]

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

There are also the following pre-defined configurations of options

--sat

target satisfiable instances

--unsat

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.

Info

January 2020 cadical 1.2.1