CADICAL(1)

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

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

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

--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=bool
    ILB (incremental lazy backtrack) [false]

--ilbassumptions=bool
    trail reuse for assumptions (ILB-like) [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]

--lidrup=bool
    linear incremental proof format [false]

--lrat=bool
    use LRAT proof format [false]

--lucky=bool
    search for lucky phases [true]

--minimize=bool
    minimize learned clauses [true]

--minimizedepth=0..1e3
    minimization depth [1e3]

--otfs=bool
    on-the-fly self subsumption [true]

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

--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 (1=only with binary, 2=minimize when 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]

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

--stats=bool
    print all statistics at the end of the run [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]

--veripb=0..4
    odd=checkdeletions, > 2=drat [0]

--vivify=bool
    vivification [true]

--vivifyinst=bool
    instantiate last literal when vivify [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.