cryptominisat5(1)

Positional arguments:

files

input file and proof output (XLRUP by default, see --xlrup) [nargs: 0 or more]

Optional arguments:

-h, --help

shows help message and exits

-v, --version

Print version information

--xlrup

Encoding of the XLRUP proof, checkable directly by cake_xlrup. 1 = text (cake_xlrup --no-binary), 2 = binary [1..2] [nargs=0..1] [default: 1]

--maxtime

Stop solving after this much time (s)

--maxconfl

Stop solving after this many conflicts

-t, --threads

Number of threads [nargs=0..1] [default: 1]

--maxsol

Search for given amount of solutions. Thanks to Jannis Harder for the decision-based banning idea [nargs=0..1] [default: 1]

--polar

{true,false,rnd,weight,auto} Selects polarity mode. 'true'/'false' -> always branch positive/negative. 'weight' -> random, biased by the per-variable weight. 'auto' -> CaDiCaL's saved/target/best phases with rephasing [nargs=0..1] [default: "auto"]

--nobansol

Don't ban the solution once it's found

--debuglib

Parse special comments to run solve/simplify during parsing of CNF

-s, --printsol

Print assignment if solution is SAT [nargs=0..1] [default: 1]

--clearinter

Interrupt threads cleanly, all the time [nargs=0..1] [default: 0]

--zero-exit-status

Exit with status zero in case the solving has finished without an issue

--sampling

Set sampling vars such as '1,84,44'. Can also be set via CNF using 'c p show 1 84 44 0'

--assump

Assumptions file [nargs=0..1] [default: ""]

--dumpresult

Write solution(s) to this file

--verb

[0-10] Verbosity of solver. 0 = only solution [nargs=0..1] [default: 1]

--prefix

Prefix of every comment line printed [nargs=0..1] [default: "c "]

-r, --seed

[0..] Random seed [nargs=0..1] [default: 0]

-m, --mult

Time multiplier for all simplification cutoffs [nargs=0..1] [default: 3]

--nextm

Global multiplier when the next inprocessing should take place [nargs=0..1] [default: 1]

--memoutmult

Multiplier for memory-out checks on inprocessing functions. It limits things such as clause-link-in. Useful when you have limited memory but still want to do some inprocessing [nargs=0..1] [default: 1]

--scc

Find equivalent literals through SCC and replace them [nargs=0..1] [default: 1]

--restart

Enable restarts [nargs=0..1] [default: 1]

--restartint

Minimum number of conflicts between restarts [nargs=0..1] [default: 2]

--restartmargin

Percent the fast glue EMA must be above the slow one to restart [nargs=0..1] [default: 10]

--emagluefast

Window size of the fast glue EMA [nargs=0..1] [default: 33]

--emaglueslow

Window size of the slow glue EMA [nargs=0..1] [default: 100000]

--stabilize

Alternate stable (reluctant doubling) and focused (glue EMA) phases [nargs=0..1] [default: 1]

--stabilizeint

Length of first stabilizing phase, in conflicts [nargs=0..1] [default: 1000]

--stabilizefactor

Multiplier of stabilizing phase length at each phase change [nargs=0..1] [default: 2]

--stabilizemaxint

Maximum stabilizing phase length [nargs=0..1] [default: 2000000000]

--reluctant

Reluctant doubling base period for stable-phase restarts, 0 = never restart there [nargs=0..1] [default: 1024]

--reluctantmax

Maximum reluctant doubling period multiplier [nargs=0..1] [default: 1048576]

--reduce

Enable learnt clause DB reduction [nargs=0..1] [default: 1]

--reduceint

Base reduce interval, in conflicts [nargs=0..1] [default: 1000]

--reducetarget

Percent of unused reduce candidates removed per reduce [nargs=0..1] [default: 75]

--reducelow

Fraction per mille of reduce candidates removed at the first reduce, rising towards --reducehigh as kissat. Set >= reducehigh to use --reducetarget [nargs=0..1] [default: 750]

--reducehigh

Asymptotic fraction per mille of reduce candidates removed [nargs=0..1] [default: 750]

--reducerounds

Number of reduces a learnt clause is kept for after it was learnt or last used [nargs=0..1] [default: 2]

--reducekeepused

Keep every learnt clause used since the last reduce, as CaDiCaL. 0: kissat, tier3 is always a candidate [nargs=0..1] [default: 1]

--eagersubsume

Demote the last learnt clauses subsumed by a new one, as kissat [nargs=0..1] [default: 1]

--reducetier1glue

Glue at/below which learnt clauses are kept forever [nargs=0..1] [default: 2]

--reducetier2glue

Glue at/below which learnt clauses get a double life [nargs=0..1] [default: 6]

--dyntiers

Recompute tier1/tier2 glue limits from glue usage at each reduce, as kissat [nargs=0..1] [default: 0]

--flush

Once in a while flush ALL unused redundant clauses [nargs=0..1] [default: 0]

--flushfactor

Flush interval multiplier [nargs=0..1] [default: 3]

--flushint

Initial flush interval, in conflicts [nargs=0..1] [default: 100000]

--branchstr

Branch strategy string that switches between different branch strategies while solving e.g. 'vsids1+vsids2' [nargs=0..1] [default: "vmtf+vsids"]

--sls

Run local search ('walk') during rephasing [nargs=0..1] [default: 1]

--walknonstable

Run local search during focused phases too [nargs=0..1] [default: 1]

--walkseedphase

Start local search off the CDCL phases, as CaDiCaL does [nargs=0..1] [default: 0]

--walkinitially

Local search rounds to run before simplifying and searching, 0=none [nargs=0..1] [default: 2]

--walkxorweight

Weight of XOR constraints in yalsat's break values, times 100 (range 0-1000) [nargs=0..1] [default: 500]

--walkmineff

Minimum local search effort, in yalsat mems [nargs=0..1] [default: 1000000]

--walkmaxeff

Maximum local search effort, in yalsat mems [nargs=0..1] [default: 100000000]

--walkreleff

Local search effort per mille of the search propagations done so far [nargs=0..1] [default: 20]

--slsmaxmem

Maximum number of MB to give to the local search solver. Skips local search if handing over the formula would need more. [nargs=0..1] [default: 500]

--ccnrneighmaxsz

CCNR builds no neighbor edges for clauses longer than this. The neighborhood is quadratic in clause size, so one huge clause costs GBs and makes every flip of its vars charge thousands of mems [nargs=0..1] [default: 256]

--backboneccnrlim

Mems budget, in millions, for each of the CCNR local search tries that pre-filter backbone candidates. Too low and no model is found, so cadiback must test every variable [nargs=0..1] [default: 300]

--rephase

Enable resetting the saved phases [nargs=0..1] [default: 1]

--rephaseint

Rephase interval, in conflicts. The interval grows arithmetically. [nargs=0..1] [default: 1000]

--phase

Default decision polarity [nargs=0..1] [default: 1]

--lucky

Search for lucky phases before the CDCL loop [nargs=0..1] [default: 1]

--target

Decide on target phases. 0 = never, 1 = stable phases only, 2 = always [nargs=0..1] [default: 1]

--transred

Remove useless binary clauses (transitive reduction) [nargs=0..1] [default: 1]

--intree

Carry out intree-based probing [nargs=0..1] [default: 1]

--fullprobe

Regularly probe both polarities of variables during search [nargs=0..1] [default: 0]

--fullprobemaxm

Time in mega-bogoprops to perform full probing [nargs=0..1] [default: 20]

--intreemaxm

Time in mega-bogoprops to perform intree probing [nargs=0..1] [default: 400]

--intreeeff

Intree probing budget as a fraction of all propagations since its last call [nargs=0..1] [default: 0.8]

--absbudget

Intree, distill-bin and irred distill-long budgets are absolute, not relative to search effort [nargs=0..1] [default: false]

--otfhyper

Perform hyper-binary resolution during probing [nargs=0..1] [default: 1]

--hyperkeepconfl

Conflicts an unused intree hyper-bin is kept for before being dropped [nargs=0..1] [default: 15000]

--schedsimp

Perform simplification rounds. If 0, we never perform any. [nargs=0..1] [default: 1]

--presimp

Perform simplification at the very start [nargs=0..1] [default: 1]

--allpresimp

Perform simplification at EVERY start -- only matters in library mode [nargs=0..1] [default: 0]

-n, --nonstop

Never stop the search() process in class SATSolver [nargs=0..1] [default: 0]

--maxnumsimppersolve

Maximum number of simplifications to perform for every solve() call. After this, no more inprocessing will take place. [nargs=0..1] [default: 25]

--schedule

Schedule for simplification during run [nargs=0..1] [default: "scc-vrepl,sub-impl,occ-backw-sub-str,occ-clean-implicit,occ-sweep,occ-bve,occ-ternary-res,occ-xor,must-scc-vrepl,card-find,cl-consolidate,scc-vrepl,renumber,"]

--preschedule

Schedule for simplification at startup [nargs=0..1] [default: "sub-impl, occ-backw-sub,scc-vrepl,occ-sweep, occ-bve,occ-xor,must-scc-vrepl"]

--occsimp

Perform occurrence-list-based optimisations (variable elimination, subsumption, bounded variable addition...) [nargs=0..1] [default: 1]

--confbtwsimp

Start first simplification after this many conflicts [nargs=0..1] [default: 40000]

--confbtwsimpinc

Simp rounds increment by this power of N [nargs=0..1] [default: 1.4]

--tern

Perform Ternary resolution [nargs=0..1] [default: true]

--terntimelim

Time-out in bogoprops M of ternary resolution as per paper 'Look-Ahead Versus Look-Back for Satisfiability Problems' [nargs=0..1] [default: 100]

--terncreate

Create only this multiple (of linked in cls) ternary resolution clauses per simp run [nargs=0..1] [default: 0.3]

--ternbincreate

Allow ternary resolving to generate binary clauses [nargs=0..1] [default: 0]

--occredmax

Don't add to occur list any redundant clause larger than this [nargs=0..1] [default: 50]

--occredmaxmb

Don't allow redundant occur size to be beyond this many MB [nargs=0..1] [default: 600]

--occirredmaxmb

Don't allow irredundant occur size to be beyond this many MB [nargs=0..1] [default: 2500]

--strengthen

Perform clause contraction through self-subsuming resolution as part of the occurrence-subsumption system [nargs=0..1] [default: 1]

--weakentimelim

Time-out in bogoprops M of weakening used [nargs=0..1] [default: 300]

--substimelim

Time-out in bogoprops M of subsumption of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]

--substimelimbinratio

Ratio of subsumption time limit to spend on sub&str long clauses with bin [nargs=0..1] [default: 0.1]

--substimelimlongratio

Ratio of subsumption time limit to spend on sub long clauses with long [nargs=0..1] [default: 0.9]

--strstimelim

Time-out in bogoprops M of strengthening of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]

--sublonggothrough

How many times go through subsume [nargs=0..1] [default: 1]

--bva

Perform bounded variable addition [nargs=0..1] [default: 0]

--varelim

Perform variable elimination as per Een and Biere [nargs=0..1] [default: 1]

--varelimto

Var elimination bogoprops M time limit [nargs=0..1] [default: 750]

--varelimover

Do BVE until the resulting no. of clause increase is less than X. Only power of 2 makes sense, i.e. 2,4,8... [nargs=0..1] [default: 16]

--emptyelim

Perform empty resolvent elimination using bit-map trick [nargs=0..1] [default: 1]

--varelimmaxmb

Maximum extra MB of memory to use for new clauses during varelim [nargs=0..1] [default: 1000]

--eratio

Eliminate this ratio of free variables at most per variable elimination iteration [nargs=0..1] [default: 1.6]

--varelimocclim

Don't try to eliminate a variable whose more frequent polarity occurs more than this many times. 0 = no limit [nargs=0..1] [default: 0]

--varelimprodlim

Don't try to eliminate a variable whose pos*neg occurrence product is over this [nargs=0..1] [default: 10000]

--varelimschedtouched

Only schedule for elimination the vars whose clauses changed since BVE last looked (CaDiCaL's Flags::elim). 0 = schedule every eligible var [nargs=0..1] [default: 0]

--weakenclsmaxsz

Don't weaken a clause longer than this during BVE. 0 = no limit [nargs=0..1] [default: 0]

--varelimclsmaxsz

Don't try to eliminate a variable that occurs in a clause longer than this. 0 = no limit [nargs=0..1] [default: 0]

--varelimclslim

Maximum resolvent size during BVE, -1 = no limit [nargs=0..1] [default: 100]

--varelimirregocclim

Don't run kitten-based irregular gate finding if the variable has more occurrences than this [nargs=0..1] [default: 100]

--varelimirregconfl

Picosat conflict budget for one irregular gate query during BVE [nargs=0..1] [default: 300]

--varelimirregunit

Turn a one-sided irregular-gate core into a unit instead of a gate [nargs=0..1] [default: 1]

--varelimprod

Weight of pos*neg in the BVE ordering score [nargs=0..1] [default: 1]

--varelimsum

Weight of pos+neg in the BVE ordering score [nargs=0..1] [default: 1]

--varelimcheckres

BVE should check whether resolvents subsume others and check for exact size increase [nargs=0..1] [default: 0]

--occrelocatelim

When strengthening removes a literal whose occurrence list is longer than this, move the clause to a new place instead of searching the list [nargs=0..1] [default: 1000]

--xor

Discover long XORs [nargs=0..1] [default: 1]

--maxxorsize

Maximum XOR size to find [nargs=0..1] [default: 12]

--xorfindtout

Time limit for finding XORs [nargs=0..1] [default: 400]

--maxxormat

Maximum matrix size (=num elements) that we should try to echelonize [nargs=0..1] [default: 400]

--gates

Find gates. [nargs=0..1] [default: 0]

--printgatedot

Print gate structure regularly to file 'gatesX.dot' [nargs=0..1] [default: 0]

--gatefindto

Max time in bogoprops M to find gates [nargs=0..1] [default: 200]

--recur

Perform recursive minimisation [nargs=0..1] [default: 1]

--moreminim

Perform strong minimisation at conflict gen. [nargs=0..1] [default: 1]

--moremoreminim

Perform even stronger minimisation at conflict gen. [nargs=0..1] [default: 2]

--moremorealways

Always strong-minimise clause [nargs=0..1] [default: 0]

--decbased

Create decision-based conflict clauses when the UIP clause is too large [nargs=0..1] [default: 1]

--bumpreasondepth

Bump vars in reasons of learnt clause lits up to this depth. 0 = off [nargs=0..1] [default: 1]

--shrink

All-UIP shrinking of learnt clauses [nargs=0..1] [default: 1]

--otfs

On-the-fly strengthening of clauses during conflict analysis [nargs=0..1] [default: 1]

--diffdeclevelchrono

Difference in decision level is more than this, perform chronological backtracking instead of non-chronological backtracking. Giving -1 means it is never turned on (overrides '--confltochrono -1' in this case). [nargs=0..1] [default: 20]

--chronoreusetrail

On backjump, only backtrack to the level of the best-ranked var above the jump level [nargs=0..1] [default: 1]

--restartreusetrail

On restart, keep decisions that would be re-made anyway [nargs=0..1] [default: 1]

--verbstat

Change verbosity of statistics at the end of the solving [0..3] [nargs=0..1] [default: 2]

--verbrestart

Print more thorough, but different stats [nargs=0..1] [default: 0]

--verballrestarts

Print a line for every restart [nargs=0..1] [default: 0]

--restartprint

Print restart status lines at least every N conflicts [nargs=0..1] [default: 8192]

--distill

Regularly execute clause distillation [nargs=0..1] [default: 1]

--distillbin

Regularly execute binary clause distillation [nargs=0..1] [default: 1]

--distillbineff

Binary clause distillation budget as a fraction of all propagations since its last call [nargs=0..1] [default: 0.02]

--distillmaxm

Maximum number of Mega-bogoprops(~time) to spend on vivifying/distilling long cls by enqueueing and propagating [nargs=0..1] [default: 200]

--distillincconf

Multiplier for current number of conflicts OTF distill [nargs=0..1] [default: 0.1]

--distillminconf

Minimum number of conflicts between OTF distill [nargs=0..1] [default: 10000]

--distillredreleff

Per-mille of all bogoprops since last call to spend distilling red cls [nargs=0..1] [default: 70]

--distillirredreleff

Per-mille of all bogoprops since last call to spend distilling irred cls [nargs=0..1] [default: 30]

--distillmineffm

Floor of the distill effort reference, in mega-bogoprops [nargs=0..1] [default: 10]

--distillschedmax

Max clauses scheduled per distill pass [nargs=0..1] [default: 20000]

--distillinst

Try to remove the last literal during distillation [nargs=0..1] [default: 1]

--xorgatemaxsize

Largest clause XOR-gate finding considers, before the log2 occurrence cap [nargs=0..1] [default: 12]

--distillremlevel

Clause removal during distillation. 0 = never, 1 = only on a real conflict, 2 = also when a literal is positively implied [nargs=0..1] [default: 2]

--distillirredalsoremratio

How much of irred to distill when doing also removal [nargs=0..1] [default: 1.2]

--distillirrednoremratio

How much of irred to distill when doing no removal [nargs=0..1] [default: 1]

--oraclemult

Time multiplier for all oracle-based (oracle-vivif*, oracle-sparsify*) cutoffs [nargs=0..1] [default: 1]

--oraclegetlearnts

Keep the clauses the oracle learnt during vivification as redundant clauses [nargs=0..1] [default: 0]

--oracleremovedislearnt

Clauses removed by the oracle are re-added as redundant instead of being deleted [nargs=0..1] [default: 0]

--oraclefindbins

[0..] Effort spent looking for binary clauses during oracle vivification. 0 = off [nargs=0..1] [default: 0]

--congruence

Congruence closure over AND/XOR gates (the 'congruence' schedule token) [nargs=0..1] [default: 1]

--congruenceandsz

Max clause size of AND gates for congruence closure [nargs=0..1] [default: 64]

--congruencexorsz

Max clause size of XOR gates for congruence closure [nargs=0..1] [default: 4]

--sweep

Perform SAT sweeping with kitten (occ-sweep) [nargs=0..1] [default: 1]

--sweeptimelimM

Tick limit cap for one occ-sweep run, in millions [nargs=0..1] [default: 150]

--sweepeff

occ-sweep budget as a fraction of all bogoprops since its last call [nargs=0..1] [default: 0.1]

--sweepmineffm

Floor of the occ-sweep budget, in mega-ticks [nargs=0..1] [default: 10]

--sweepvars

Starting number of variables in a sweeping environment [nargs=0..1] [default: 256]

--sweepclauses

Starting number of clauses in a sweeping environment [nargs=0..1] [default: 1024]

--sweepdepth

Starting depth of a sweeping environment [nargs=0..1] [default: 2]

--sweepfliprounds

Rounds of model flipping during sweeping [nargs=0..1] [default: 1]

--renumber

Renumber variables to increase CPU cache efficiency [nargs=0..1] [default: 1]

--mustconsolidate

Always consolidate, even if not useful. This is used for debugging ONLY [nargs=0..1] [default: 0]

--savemem

Save memory by deallocating variable space after renumbering. Only works if renumbering is active. [nargs=0..1] [default: 1]

--mustrenumber

Treat all 'renumber' strategies as 'must-renumber' [nargs=0..1] [default: 0]

--fullwatchconseveryn

Consolidate watchlists fully once every N conflicts. Scheduled during simplification rounds. [nargs=0..1] [default: 4000000]

--strmaxt

Maximum MBP to spend on distilling long irred cls through watches [nargs=0..1] [default: 20]

--implicitmanip

Subsume and strengthen implicit clauses with each other [nargs=0..1] [default: 1]

--implsubsto

Timeout (in bogoprop Millions) of implicit subsumption [nargs=0..1] [default: 100]

--implstrto

Timeout (in bogoprop Millions) of implicit strengthening [nargs=0..1] [default: 200]

--cardfind

Find cardinality constraints [nargs=0..1] [default: 0]

--sync

Sync threads every N conflicts [nargs=0..1] [default: 7000]

--printtimes

Print time it took for each simplification run. If set to 0, logs are easier to compare [nargs=0..1] [default: 1]

--maxsccdepth

The maximum for scc search depth [nargs=0..1] [default: 30000]

--maxmatrixrows

Set maximum no. of rows for gaussian matrix. Too large matrices should be discarded for reasons of efficiency [nargs=0..1] [default: 100000]

--maxmatrixcols

Set maximum no. of columns for gaussian matrix. Too large matrices should be discarded for reasons of efficiency [nargs=0..1] [default: 100000]

--autodisablegauss

Automatically disable gauss when performing badly [nargs=0..1] [default: true]

--minmatrixrows

Set minimum no. of rows for gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency [nargs=0..1] [default: 10]

--maxnummatrices

Maximum number of matrices to treat. [nargs=0..1] [default: 1000000]

--gaussusefulcutoff

Turn off Gauss if less than this many usefulness ratio is recorded [nargs=0..1] [default: 0.1]

--gaussmincalls

Only consider disabling a matrix after this many Gauss calls [nargs=0..1] [default: 200]

--gausscheckevery

Check whether to disable a matrix every this many conflicts [nargs=0..1] [default: 1024]