cryptominisat5 - Man Page
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
SQL options
- --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 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.
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:
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/