Provided by: cryptominisat_5.11.21+dfsg1-2_amd64 
NAME
cryptominisat5 - manual page for cryptominisat5 5.11.21
SYNOPSIS
cryptominisat5 [--help] [--version] [--help VAR] [--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]
[--varsperxorcut VAR] [--maxxormat VAR] [--forcepreservexors 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] [--sampling VAR]
[--onlysampling] [--assump VAR] [--maxmatrixrows VAR] [--maxmatrixcols VAR] [--autodisablegauss VAR]
[--minmatrixrows VAR] [--maxnummatrices VAR] [--detachxor VAR] [--useallmatrixes VAR] [--detachverb VAR]
[--gaussusefulcutoff VAR] [--dumpresult VAR] files
DESCRIPTION
A universal, fast SAT solver with XOR and Gaussian Elimination support. Input can be either plain or
gzipped DIMACS with XOR extension
cryptominisat5 [options] inputfile [frat-file]
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
-h, --help
Print extensive help [nargs=0..1] [default: false]
-v, --version
Print version info
--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: true]
--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: 1]
--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]
--varsperxorcut
Number of _real_ variables per XOR when cutting them. So 2 will have XORs of size 4 because 1 =
connecting to previous, 1 = connecting to next, 2 in the midde. If the XOR is 4 long, it will be
just one 4-long XOR, no connectors [nargs=0..1] [default: 2]
--maxxormat
Maximum matrix size (=num elements) that we should try to echelonize [nargs=0..1] [default: 400]
--forcepreservexors
Force preserving XORs when they have been found. Easier to make sure XORs are not lost through
simplifiactions such as strenghtening [nargs=0..1] [default: 1]
--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]
--sampling
Sampling vars, separated by comma [nargs=0..1] [default: ""]
--onlysampling
Print and ban(!) solutions' vars only in 'c ind' or as --sampling '...'
--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]
--detachxor
Detach and reattach XORs [nargs=0..1] [default: false]
--useallmatrixes
Force using all matrices [nargs=0..1] [default: false]
--detachverb
If set, verbosity for XOR detach code is upped, ignoring normal verbosity [nargs=0..1] [default:
0]
--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
Normal run schedules:
Default schedule:
scc-vrepl,sub-impl,breakid,occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,card-find,cl-consolidate,scc-vrepl,renumber,bosphorus,louvain-comms
Schedule at startup: sub-impl, occ-backw-sub,scc-vrepl,breakid, occ-bve,occ-xor
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.
cryptominisat5 5.11.21 May 2025 CRYPTOMINISAT5(1)