cryptominisat5 - SAT solver

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 [drat-trim-file]

cryptominisat5 --preproc 1 [options] inputfile simplified-cnf-file
cryptominisat5 --preproc 2 [options] solution-file

-h [ --help ]
Print simple help
Print extensive help
-v [ --version ]
Print version info
--verb arg (=1)
[0-10] Verbosity of solver. 0 = only solution
-r [ --random ] arg (=0)
[0..] Random seed
-t [ --threads ] arg (=1)
Number of threads
--maxtime arg
Stop solving after this much time (s)
--maxconfl arg
Stop solving after this many conflicts
-m [ --mult ] arg (=3)
Time multiplier for all simplification cutoffs
--memoutmult arg (=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
-p [ --preproc ] arg (=0)
0 = normal run, 1 = preprocess and dump, 2 = read back dump and solution to produce final solution

--polar arg (=auto)
{true,false,rnd,auto} 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')
--polarstablen arg (=4)
When to use stable polarities. 0 = always, otherwise every n. Negative is special, see code
--lucky arg (=20)
Try computing lucky polarities
--polarbestinvmult arg (=9)
How often should we use inverted best polarities instead of stable
--polarbestmult arg (=1000)
How often should we use best polarities instead of stable

--sql arg (=0)
Write to SQL. 0 = no SQL, 1 or 2 = sqlite
--sqlitedb arg
Where to put the SQLite database
--sqlitedboverwrite arg (=0)
Overwrite the SQLite database file if it exists
--cldatadumpratio arg (=0.01)
Only dump this ratio of clauses' data, randomly selected. Since machine learning doesn't need that much data, this can reduce the data you have to deal with.
--cllockdatagen arg (=0.10000000000000001)
Lock for data generation into lev0, setting locked_for_data_gen. Only works when clause is marked for dumping ('--cldatadumpratio' )

--restart arg
{geom, glue, luby} Restart strategy to follow.
--gluehist arg (=50)
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
--lwrbndblkrest arg (=10000)
Lower bound on blocking restart -- don't block before this many conflicts
--locgmult arg (=0.8)
The multiplier used to determine if we should restart during glue-based restart
--ratiogluegeom arg (=5)
Ratio of glue vs geometric restarts -- more is more glue

--verbstat arg (=2)
Change verbosity of statistics at the end of the solving [0..3]
--verbrestart arg (=0)
Print more thorough, but different stats
--verballrestarts arg (=0)
Print a line for every restart
-s [ --printsol ] arg (=1)
Print assignment if solution is SAT
--restartprint arg (=8192)
Print restart status lines at least every N conflicts
--dumpresult arg
Write solution(s) to this file

--updateglueonanalysis arg (=1)
Update glues while analyzing
--maxgluehistltlimited arg (=50)
Maximum glue used by glue-based restart strategy when populating glue history.

--diffdeclevelchrono arg (=20)
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).

--gluecut0 arg (=3)
Glue value for lev 0 ('keep') cut
--gluecut1 arg (=6)
Glue value for lev 1 cut ('give another shot'
--adjustglue arg (=0.7)
If more than this % of clauses is LOW glue (level 0) then lower the glue cutoff by 1 -- once and never again
--everylev1 arg (=10000)
Reduce lev1 clauses every N
--everylev2 arg (=15000)
Reduce lev2 clauses every N
--lev1usewithin arg (=70000)
Learnt clause must be used in lev1 within this timeframe or be dropped to lev2
--dumpred arg
Dump redundant clauses of gluecut0&1 to this filename
--dumpredmaxlen arg (=10000)
When dumping redundant clauses, only dump clauses at most this long
--dumpredmaxglue arg (=1000)
When dumping redundant clauses, only dump clauses with at most this large glue

Clause dumping after problem finishing:

--branchstr arg (=maple1+maple2+vsids2+maple1+maple2+vsids1)
Branch strategy. E.g. 'vmtf+vsids+maple+rnd'

--recur arg (=1)
Perform recursive minimisation
--moreminim arg (=1)
Perform strong minimisation at conflict gen.
--moremoreminim arg (=1)
Perform even stronger minimisation at conflict gen.
--moremorealways arg (=0)
Always strong-minimise clause
--decbased arg (=1)
Create decision-based conflict clauses when the UIP clause is too large

--maxsol arg (=1)
Search for given amount of solutions. Thanks to Jannis Harder for the decision-based banning idea
Don't ban the solution once it's found
--debuglib arg
Parse special comments to run solve/simplify during parsing of CNF

--transred arg (=1)
Remove useless binary clauses (transitive reduction)
--intree arg (=1)
Carry out intree-based probing
--intreemaxm arg (=1200)
Time in mega-bogoprops to perform intree probing
--otfhyper arg (=1)
Perform hyper-binary resolution during probing

--sls arg (=1)
Run SLS during simplification
--slstype arg (=ccnr)
Which SLS to run. Allowed values: walksat, yalsat, ccnr, ccnr_yalsat
--slsmaxmem arg (=500)
Maximum number of MB to give to SLS solver. Doesn't run SLS solver if the memory usage would be more than this.
--slseveryn arg (=2)
Run SLS solver every N simplifications only
--yalsatmems arg (=40)
Run Yalsat with this many mems*million timeout. Limits time of yalsat run
--walksatruns arg (=50)
Max 'runs' for WalkSAT. Limits time of WalkSAT run
--slsgetphase arg (=1)
Get phase from SLS solver, set as new phase for CDCL
--slsccnraspire arg (=1)
Turn aspiration on/off for CCANR
--slstobump arg (=100)
How many variables to bump in CCNR
--slstobumpmaxpervar arg (=100)
How many times to bump an individual variable's activity in CCNR
--slsbumptype arg (=6)
How to calculate what variable to bump. 1 = clause-based, 2 = var-flip-based, 3 = var-score-based
--slsoffset arg (=0)
Should SLS set the VSIDS/Maple offsetsd

--schedsimp arg (=1)
Perform simplification rounds. If 0, we never perform any.
--presimp arg (=0)
Perform simplification at the very start
--allpresimp arg (=0)
Perform simplification at EVERY start -- only matters in library mode
-n [ --nonstop ] arg (=0)
Never stop the search() process in class SATSolver
--maxnumsimppersolve arg (=25)
Maximum number of simplifiactions to perform for every solve() call. After this, no more inprocessing will take place.
--schedule arg
Schedule for simplification during run
--preschedule arg
Schedule for simplification at startup
--occsimp arg (=1)
Perform occurrence-list-based optimisations (variable elimination, subsumption, bounded variable addition...)
--confbtwsimp arg (=50000)
Start first simplification after this many conflicts
--confbtwsimpinc arg (=1.4)
Simp rounds increment by this power of N

--occredmax arg (=200)
Don't add to occur list any redundant clause larger than this
--occredmaxmb arg (=600)
Don't allow redundant occur size to be beyond this many MB
--occirredmaxmb arg (=2500)
Don't allow irredundant occur size to be beyond this many MB

--tern arg (=1)
Perform Ternary resolution'
--terntimelim arg (=100)
Time-out in bogoprops M of ternary resolution as per paper 'Look-Ahead Versus Look-Back for Satisfiability Problems'
--ternkeep arg (=6)
Keep ternary resolution clauses only if they are touched within this multiple of 'lev1usewithin'
--terncreate arg (=1)
Create only this multiple (of linked in cls) ternary resolution clauses per simp run
--ternbincreate arg (=1)
Allow ternary resolving to generate binary clauses

--strengthen arg (=1)
Perform clause contraction through self-subsuming resolution as part of the occurrence-subsumption system
--substimelim arg (=300)
Time-out in bogoprops M of subsumption of long clauses with long clauses, after computing occur
--substimelimbinratio arg (=0.10000000000000001)
Ratio of subsumption time limit to spend on sub&str long clauses with bin
--substimelimlongratio arg (=0.90000000000000002)
Ratio of subsumption time limit to spend on sub long clauses with long
--strstimelim arg (=300)
Time-out in bogoprops M of strengthening of long clauses with long clauses, after computing occur
--sublonggothrough arg (=1)
How many times go through subsume

--varelim arg (=1)
Perform variable elimination as per Een and Biere
--varelimto arg (=750)
Var elimination bogoprops M time limit
--varelimover arg (=32)
Do BVE until the resulting no. of clause increase is less than X. Only power of 2 makes sense, i.e. 2,4,8...
--emptyelim arg (=1)
Perform empty resolvent elimination using bit-map trick
--varelimmaxmb arg (=1000)
Maximum extra MB of memory to use for new clauses during varelim
--eratio arg (=1.6)
Eliminate this ratio of free variables at most per variable elimination iteration
--skipresol arg (=1)
Skip BVE resolvents in case they belong to a gate

--bva arg (=1)
Perform bounded variable addition
--bvaeveryn arg (=7)
Perform BVA only every N occ-simplify calls
--bvalim arg (=250000)
Maximum number of variables to add by BVA per call
--bva2lit arg (=1)
BVA with 2-lit difference hack, too. Beware, this reduces the effectiveness of 1-lit diff
--bvato arg (=50)
BVA time limit in bogoprops M

--scc arg (=1)
Find equivalent literals through SCC and replace them

--comps arg (=0)
Perform component-finding and separate handling
--compsfrom arg (=0)
Component finding only after this many simplification rounds
--compsvar arg (=1000000)
Only use components in case the number of variables is below this limit
--compslimit arg (=500)
Limit how much time is spent in component-finding

--renumber arg (=1)
Renumber variables to increase CPU cache efficiency
--savemem arg (=1)
Save memory by deallocating variable space after renumbering. Only works if renumbering is active.
--mustrenumber arg (=0)
Treat all 'renumber' strategies as 'must-renumber'
--fullwatchconseveryn arg (=4000000)
Consolidate watchlists fully once every N conflicts. Scheduled during simplification rounds.
--xor arg (=1)
Discover long XORs
--maxxorsize arg (=7)
Maximum XOR size to find
--xorfindtout arg (=400)
Time limit for finding XORs
--varsperxorcut arg (=2)
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
--maxxormat arg (=400)
Maximum matrix size (=num elements) that we should try to echelonize
--forcepreservexors arg (=0)
Force preserving XORs when they have been found. Easier to make sure XORs are not lost through simplifiactions such as strenghtening
--gates arg (=0)
Find gates. Disables all sub-options below
--gorshort arg (=1)
Shorten clauses with OR gates
--gandrem arg (=1)
Remove clauses with AND gates
--gateeqlit arg (=1)
Find equivalent literals using gates
--printgatedot arg (=0)
Print gate structure regularly to file ''
--gatefindto arg (=200)
Max time in bogoprops M to find gates
--shortwithgatesto arg (=200)
Max time to shorten with gates, bogoprops M
--remwithgatesto arg (=100)
Max time to remove with gates, bogoprops M

--maxmatrixrows arg (=5000)
Set maximum no. of rows for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency
--autodisablegauss arg (=1)
Automatically disable gauss when performing badly
--minmatrixrows arg (=3)
Set minimum no. of rows for gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency
--maxnummatrices arg (=5)
Maximum number of matrices to treat.
--detachxor arg (=0)
Detach and reattach XORs
--useallmatrixes arg (=0)
Force using all matrices
--detachverb arg (=0)
If set, verbosity for XOR detach code is upped, ignoring normal verbosity
--gaussusefulcutoff arg (=0.20000000000000001)
Turn off Gauss if less than this many usefulenss ratio is recorded

--distill arg (=1)
Regularly execute clause distillation
--distillmaxm arg (=20)
Maximum number of Mega-bogoprops(~time) to spend on vivifying/distilling long cls by enqueueing and propagating
--distillto arg (=120)
Maximum time in bogoprops M for distillation
--distillincconf arg (=0.02)
Multiplier for current number of conflicts OTF distill
--distillminconf arg (=10000)
Minimum number of conflicts between OTF distill
--distilltier1ratio arg (=0.029999999999999999)
How much of tier 1 to distill

--reconfat arg (=2)
Reconfigure after this many simplifications
--reconf arg (=0)
Reconfigure after some time to this solver configuration [3,4,6,7,12,13,14,15,16]

--strmaxt arg (=30)
Maximum MBP to spend on distilling long irred cls through watches
--implicitmanip arg (=1)
Subsume and strengthen implicit clauses with each other
--implsubsto arg (=100)
Timeout (in bogoprop Millions) of implicit subsumption
--implstrto arg (=200)
Timeout (in bogoprop Millions) of implicit strengthening
--cardfind arg (=0)
Find cardinality constraints

Default schedule: handle-comps,scc-vrepl,sub-impl,intree-probe,sub-str-cls-with-bin,distill-cls,scc-vrepl,sub-impl,str-impl,sub-impl,breakid,occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,card-find,cl-consolidate,str-impl,sub-str-cls-with-bin,distill-cls,scc-vrepl,renumber,bosphorus,sls,lucky
Schedule at startup: sub-impl,breakid, occ-backw-sub-str, occ-clean-implicit, occ-bve,occ-ternary-res, occ-backw-sub-str, occ-xor, card-find,cl-consolidate,scc-vrepl,sub-cls-with-bin,bosphorus,sls,lucky

handle-comps,scc-vrepl,sub-impl,sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,breakid, occ-backw-sub-str, occ-clean-implicit, occ-bve, occ-bva,occ-ternary-res, occ-xor,cl-consolidate,str-impl, sub-str-cls-with-bin, distill-cls, scc-vrepl, sub-impl,str-impl, sub-impl, sub-str-cls-with-bin,intree-probe, must-renumber

Please don't hesitate to file any and all issues at:

cryptominisat5 is written and maintained by Mate Soos

cryptominisat5 is under the MIT license. Please see for the full text

More documentation for the cryptominisat5 SAT solver can be found at
December 2020 cryptominisat5 5.8.0