cryptominisat5 - Man Page

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

shows help message and exits

Print version information

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

Emit the proof in XLRUP format, checkable directly by cake_xlrup. Set to 0 to emit raw FRAT instead, for debugging proof generation with frat-rs [0..1] [nargs=0..1] [default: 1]

Stop solving after this much time (s)

Stop solving after this many conflicts

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

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

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

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

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]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Don't ban the solution once it's found

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

Run BreakID to break symmetries. [nargs=0..1] [default: false]

Run BreakID every N simplification iterations [nargs=0..1] [default: 5]

Maximum number of literals in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 3500]

Maximum number of clauses in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 600]

Maximum number of variables in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 300]

Maximum number of steps taken during automorphism finding. [nargs=0..1] [default: 2000]

Maximum number of breaking clauses per permutation. [nargs=0..1] [default: 50]

Detect matrix row interchangability [nargs=0..1] [default: true]

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

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

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

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

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

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

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

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

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]

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]

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]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Schedule for simplification during run

Schedule for simplification at startup

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Perform BVA only every N occ-simplify calls [nargs=0..1] [default: 7]

Maximum number of variables to add by BVA per call [nargs=0..1] [default: 250000]

BVA with 2-lit difference hack, too. Beware, this reduces the effectiveness of 1-lit diff [nargs=0..1] [default: 1]

BVA time limit in bogoprops M [nargs=0..1] [default: 50]

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

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

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]

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

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

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

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]

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

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]

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

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

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

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

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

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

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

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

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

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]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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]

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

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

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

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

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

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

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

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

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

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

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

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

Per-mille of search props to spend distilling red cls [nargs=0..1] [default: 20]

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

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

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]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Write solution(s) to this file