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]
Positionalarguments:
files input file and FRAT output [nargs: 0 or more]
Optionalarguments:-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
Normalrunschedules:
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
Install Now
SVG Icons
PNG Icons