Provided by: cryptominisat_5.8.0+dfsg1-2_amd64 
NAME
cryptominisat5 - SAT solver
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 [drat-trim-file]
Preprocessor usage:
cryptominisat5 --preproc 1 [options] inputfile simplified-cnf-file
cryptominisat5 --preproc 2 [options] solution-file
Main options:
-h [ --help ]
Print simple help
--hhelp
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
Polarity options:
--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
Restart options:
--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
Printing options:
--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
Glue options:
--updateglueonanalysis arg (=1)
Update glues while analyzing
--maxgluehistltlimited arg (=50)
Maximum glue used by glue-based restart strategy when populating glue history.
Propagation options:
--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).
Redundant clause options:
--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:
Variable branching options:
--branchstr arg (=maple1+maple2+vsids2+maple1+maple2+vsids1)
Branch strategy. E.g. 'vmtf+vsids+maple+rnd'
Conflict options:
--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
Iterative solve options:
--maxsol arg (=1)
Search for given amount of solutions. Thanks to Jannis Harder for the
decision-based banning idea
--nobansol
Don't ban the solution once it's found
--debuglib arg
Parse special comments to run solve/simplify during parsing of CNF
Probing options:
--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
Stochastic Local Search options:
--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
Simplification schedules:
--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
Occ-based simplification memory limits:
--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
Ternary resolution:
--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
Occ-based subsumption and strengthening time limits:
--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
BVE options:
--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 options:
--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
Equivalent literal options:
--scc arg (=1)
Find equivalent literals through SCC and replace them
Component options:
--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
Memory saving options:
--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-related options:
--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
--m4ri arg (=1)
Use M4RI
Gate-related options:
--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 'gatesX.dot'
--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
Gauss options:
--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 options:
--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
Reconf options:
--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]
Misc options:
--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
Normal run schedules:
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
Preproc run schedule:
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
BUG TRACKER
Please don't hesitate to file any and all issues at:
https://github.com/msoos/cryptominisat/issues
AUTHORS
cryptominisat5 is written and maintained by Mate Soos soos.mate@gmail.com
COPYRIGHT
cryptominisat5 is under the MIT license. Please see https://opensource.org/licenses/MIT
for the full text
SEE ALSO
More documentation for the cryptominisat5 SAT solver can be found at
https://www.msoos.org/cryptominisat5/