cryptominisat5 - Man Page

input file and FRAT output [nargs: 0 or more]

shows help message and exits

prints version information and exits

[0-10] Verbosity of solver. 0 = only solution [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,auto,stable} Selects polarity mode. 'true' -> selects only positive polarity when branching. 'false' -> selects only negative polarity when branching. 'auto' -> selects last polarity used (also called 'caching') [nargs=0..1] [default: "auto"]

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

{geom, glue, luby}  Restart strategy to follow. [nargs=0..1] [default: "auto"]

The size of the base restart [nargs=0..1] [default: 100]

The size of the moving window for short-term glue history of redundant clauses. If higher, the minimal number of conflicts between restarts is longer [nargs=0..1] [default: 50]

Lower bound on blocking restart -- don't block before this many conflicts [nargs=0..1] [default: 10000]

The multiplier used to determine if we should restart during glue-based restart [nargs=0..1] [default: 0.8]

Ratio of glue vs geometric restarts -- more is more glue [nargs=0..1] [default: 5]

Do blocking restart for glues [nargs=0..1] [default: 1]

Glue value for lev 0 ('keep') cut [nargs=0..1] [default: 3]

Glue value for lev 1 cut ('give another shot' [nargs=0..1] [default: 6]

If more than this % of clauses is LOW glue (level 0) then lower the glue cutoff by 1 -- once and never again [nargs=0..1] [default: 0.7]

Reduce lev1 clauses every N [nargs=0..1] [default: 10000]

Reduce lev2 clauses every N [nargs=0..1] [default: 15000]

Learnt clause must be used in lev1 within this timeframe or be dropped to lev2 [nargs=0..1] [default: 70000]

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 SLS during simplification [nargs=0..1] [default: 1]

Which SLS to run. Allowed values: walksat, yalsat, ccnr, ccnr_yalsat [nargs=0..1] [default: "ccnr"]

Maximum number of MB to give to SLS solver. Doesn't run SLS solver if the memory usage would be more than this. [nargs=0..1] [default: 500]

Run SLS solver every N simplifications only [nargs=0..1] [default: 2]

Run Yalsat with this many mems*million timeout. Limits time of yalsat run [nargs=0..1] [default: 10]

Max 'runs' for WalkSAT. Limits time of WalkSAT run [nargs=0..1] [default: 50]

Get phase from SLS solver, set as new phase for CDCL [nargs=0..1] [default: 1]

Turn aspiration on/off for CCANR [nargs=0..1] [default: 1]

How many variables to bump in CCNR [nargs=0..1] [default: 100]

How many times to bump an individual variable's activity in CCNR [nargs=0..1] [default: 100]

How to calculate what variable to bump. 1 = clause-based, 2 = var-flip-based, 3 = var-score-based [nargs=0..1] [default: 6]

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

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

Keep ternary resolution clauses only if they are touched within this multiple of 'lev1usewithin' [nargs=0..1] [default: 5]

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

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

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

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

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]

Update glues while analyzing [nargs=0..1] [default: 1]

Maximum glue used by glue-based restart strategy when populating glue history. [nargs=0..1] [default: 50]

Difference in decision level is more than this, perform chonological 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]

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

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]

How much of tier 0 to distill [nargs=0..1] [default: 10]

How much of tier 1 to distill [nargs=0..1] [default: 0.03]

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]

Shuffle to-be-distilled clauses every N cases randomly [nargs=0..1] [default: 3]

Distill sorting type [nargs=0..1] [default: 1]

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

Simulate FRAT [nargs=0..1] [default: 0]

Print and ban(!) solutions' vars only in 'c ind' or as --sampling '...'

Set sampling vars such as '1,84,44'

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

Set maximum no. of rows for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 2000]

Set maximum no. of columns for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 1000]

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

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

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

Write solution(s) to this file