cryptominisat5 - Man Page

manual page for cryptominisat5 5.11.22

Synopsis

cryptominisat5 [--help] [--version] [--verb VAR] [--maxtime VAR] [--maxconfl VAR] [--random VAR] [--threads VAR] [--mult VAR] [--nextm VAR] [--memoutmult VAR] [--maxsol VAR] [--polar VAR] [--scc VAR] [--restart VAR] [--rstfirst VAR] [--gluehist VAR] [--lwrbndblkrest VAR] [--locgmult VAR] [--ratiogluegeom VAR] [--blockingglue VAR] [--gluecut0 VAR] [--gluecut1 VAR] [--adjustglue VAR] [--everylev1 VAR] [--everylev2 VAR] [--lev1usewithin VAR] [--branchstr VAR] [--nobansol] [--debuglib VAR] [--breakid VAR] [--breakideveryn VAR] [--breakidmaxlits VAR] [--breakidmaxcls VAR] [--breakidmaxvars VAR] [--breakidtime VAR] [--breakidcls VAR] [--breakidmatrix VAR] [--sls VAR] [--slstype VAR] [--slsmaxmem VAR] [--slseveryn VAR] [--yalsatmems VAR] [--walksatruns VAR] [--slsgetphase VAR] [--slsccnraspire VAR] [--slstobump VAR] [--slstobumpmaxpervar VAR] [--slsbumptype VAR] [--transred VAR] [--intree VAR] [--intreemaxm VAR] [--otfhyper VAR] [--schedsimp VAR] [--presimp VAR] [--allpresimp VAR] [--nonstop VAR] [--maxnumsimppersolve VAR] [--schedule VAR] [--preschedule VAR] [--occsimp VAR] [--confbtwsimp VAR] [--confbtwsimpinc VAR] [--tern VAR] [--terntimelim VAR] [--ternkeep VAR] [--terncreate VAR] [--ternbincreate VAR] [--occredmax VAR] [--occredmaxmb VAR] [--occirredmaxmb VAR] [--strengthen VAR] [--weakentimelim VAR] [--substimelim VAR] [--substimelimbinratio VAR] [--substimelimlongratio VAR] [--strstimelim VAR] [--sublonggothrough VAR] [--bva VAR] [--bvaeveryn VAR] [--bvalim VAR] [--bva2lit VAR] [--bvato VAR] [--varelim VAR] [--varelimto VAR] [--varelimover VAR] [--emptyelim VAR] [--varelimmaxmb VAR] [--eratio VAR] [--varelimcheckres VAR] [--xor VAR] [--maxxorsize VAR] [--xorfindtout VAR] [--maxxormat VAR] [--gates VAR] [--printgatedot VAR] [--gatefindto VAR] [--recur VAR] [--moreminim VAR] [--moremoreminim VAR] [--moremorealways VAR] [--decbased VAR] [--updateglueonanalysis VAR] [--maxgluehistltlimited VAR] [--diffdeclevelchrono VAR] [--verbstat VAR] [--verbrestart VAR] [--verballrestarts VAR] [--printsol,s VAR] [--restartprint VAR] [--distill VAR] [--distillbin VAR] [--distillmaxm VAR] [--distillincconf VAR] [--distillminconf VAR] [--distilltier0ratio VAR] [--distilltier1ratio VAR] [--distillirredalsoremratio VAR] [--distillirrednoremratio VAR] [--distillshuffleeveryn VAR] [--distillsort VAR] [--renumber VAR] [--mustconsolidate VAR] [--savemem VAR] [--mustrenumber VAR] [--fullwatchconseveryn VAR] [--strmaxt VAR] [--implicitmanip VAR] [--implsubsto VAR] [--implstrto VAR] [--cardfind VAR] [--sync VAR] [--clearinter VAR] [--zero-exit-status] [--printtimes VAR] [--maxsccdepth VAR] [--simfrat VAR] [--onlysampling] [--sampling VAR] [--assump VAR] [--maxmatrixrows VAR] [--maxmatrixcols VAR] [--autodisablegauss VAR] [--minmatrixrows VAR] [--maxnummatrices VAR] [--gaussusefulcutoff VAR] [--dumpresult VAR] files

Description

Positional arguments

files

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

Optional arguments

-h,  --help

shows help message and exits

-v,  --version

prints version information and exits

--verb

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

--maxtime

Stop solving after this much time (s)

--maxconfl

Stop solving after this many conflicts

-r,  --random

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

-t,  --threads

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

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

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

--scc

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

--restart

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

--rstfirst

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

--gluehist

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]

--lwrbndblkrest

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

--locgmult

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

--ratiogluegeom

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

--blockingglue

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

--gluecut0

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

--gluecut1

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

--adjustglue

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]

--everylev1

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

--everylev2

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

--lev1usewithin

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

--branchstr

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

--nobansol

Don't ban the solution once it's found

--debuglib

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

--breakid

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

--breakideveryn

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

--breakidmaxlits

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

--breakidmaxcls

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

--breakidmaxvars

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

--breakidtime

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

--breakidcls

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

--breakidmatrix

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

--sls

Run SLS during simplification [nargs=0..1] [default: 1]

--slstype

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

--slsmaxmem

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]

--slseveryn

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

--yalsatmems

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

--walksatruns

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

--slsgetphase

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

--slsccnraspire

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

--slstobump

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

--slstobumpmaxpervar

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

--slsbumptype

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

--transred

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

--intree

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

--intreemaxm

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

--otfhyper

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

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

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

--preschedule

Schedule for simplification at startup

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

--ternkeep

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

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

--bvaeveryn

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

--bvalim

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

--bva2lit

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

--bvato

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

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

--varelimcheckres

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

--xor

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

--maxxorsize

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

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

--updateglueonanalysis

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

--maxgluehistltlimited

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

--diffdeclevelchrono

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]

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

--printsol,s

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

--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 clause distillation [nargs=0..1] [default: 1]

--distillmaxm

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

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

--distilltier0ratio

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

--distilltier1ratio

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

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

--distillshuffleeveryn

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

--distillsort

Distill sorting type [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]

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

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

--simfrat

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

--onlysampling

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

--sampling

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

--assump

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

--maxmatrixrows

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

--maxmatrixcols

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

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

--maxnummatrices

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

--gaussusefulcutoff

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

--dumpresult

Write solution(s) to this file

See Also

The full documentation for cryptominisat5 is maintained as a Texinfo manual.  If the info and cryptominisat5 programs are properly installed at your site, the command

info cryptominisat5

should give you access to the complete manual.

Info

July 2024 cryptominisat5 5.11.22