.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.47.16.
.TH CRYPTOMINISAT5 "1" "December 2020" "cryptominisat5 5.8.0" "User Commands"
.SH NAME
cryptominisat5 \- SAT\ solver
.SH DESCRIPTION
A universal, fast SAT solver with XOR and Gaussian Elimination support.
Input can be either plain or gzipped DIMACS with XOR extension
.PP
cryptominisat5 [options] inputfile [drat\-trim\-file]
.SS "Preprocessor usage:"
.IP
cryptominisat5 \fB\-\-preproc\fR 1 [options] inputfile simplified\-cnf\-file
.IP
cryptominisat5 \fB\-\-preproc\fR 2 [options] solution\-file
.SS "Main options:"
.TP
\fB\-h\fR [ \fB\-\-help\fR ]
Print simple help
.TP
\fB\-\-hhelp\fR
Print extensive help
.TP
\fB\-v\fR [ \fB\-\-version\fR ]
Print version info
.TP
\fB\-\-verb\fR arg (=1)
[0\-10] Verbosity of solver. 0 = only
solution
.TP
\fB\-r\fR [ \fB\-\-random\fR ] arg (=0)
[0..] Random seed
.TP
\fB\-t\fR [ \fB\-\-threads\fR ] arg (=1)
Number of threads
.TP
\fB\-\-maxtime\fR arg
Stop solving after this much time (s)
.TP
\fB\-\-maxconfl\fR arg
Stop solving after this many conflicts
.TP
\fB\-m\fR [ \fB\-\-mult\fR ] arg (=3)
Time multiplier for all simplification
cutoffs
.TP
\fB\-\-memoutmult\fR 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
.TP
\fB\-p\fR [ \fB\-\-preproc\fR ] arg (=0)
0 = normal run, 1 = preprocess and
dump, 2 = read back dump and solution
to produce final solution
.SS "Polarity options:"
.TP
\fB\-\-polar\fR 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')
.TP
\fB\-\-polarstablen\fR arg (=4)
When to use stable polarities. 0 =
always, otherwise every n. Negative is
special, see code
.TP
\fB\-\-lucky\fR arg (=20)
Try computing lucky polarities
.TP
\fB\-\-polarbestinvmult\fR arg (=9)
How often should we use inverted best
polarities instead of stable
.TP
\fB\-\-polarbestmult\fR arg (=1000)
How often should we use best polarities
instead of stable
.SS "Restart options:"
.TP
\fB\-\-restart\fR arg
{geom, glue, luby}  Restart strategy to
follow.
.TP
\fB\-\-gluehist\fR 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
.TP
\fB\-\-lwrbndblkrest\fR arg (=10000)
Lower bound on blocking restart \fB\-\-\fR
don't block before this many conflicts
.TP
\fB\-\-locgmult\fR arg (=0.8)
The multiplier used to determine if we
should restart during glue\-based
restart
.TP
\fB\-\-ratiogluegeom\fR arg (=5)
Ratio of glue vs geometric restarts \fB\-\-\fR
more is more glue
.SS "Printing options:"
.TP
\fB\-\-verbstat\fR arg (=2)
Change verbosity of statistics at the
end of the solving [0..3]
.TP
\fB\-\-verbrestart\fR arg (=0)
Print more thorough, but different
stats
.TP
\fB\-\-verballrestarts\fR arg (=0)
Print a line for every restart
.TP
\fB\-s\fR [ \fB\-\-printsol\fR ] arg (=1)
Print assignment if solution is SAT
.TP
\fB\-\-restartprint\fR arg (=8192)
Print restart status lines at least
every N conflicts
.TP
\fB\-\-dumpresult\fR arg
Write solution(s) to this file
.SS "Glue options:"
.TP
\fB\-\-updateglueonanalysis\fR arg (=1)
Update glues while analyzing
.TP
\fB\-\-maxgluehistltlimited\fR arg (=50)
Maximum glue used by glue\-based restart
strategy when populating glue history.
.SS "Propagation options:"
.TP
\fB\-\-diffdeclevelchrono\fR arg (=20)
Difference in decision level is more
than this, perform chonological
backtracking instead of
non\-chronological backtracking. Giving
\fB\-1\fR means it is never turned on
(overrides '\-\-confltochrono \fB\-1\fR' in this
case).
.SS "Redundant clause options:"
.TP
\fB\-\-gluecut0\fR arg (=3)
Glue value for lev 0 ('keep') cut
.TP
\fB\-\-gluecut1\fR arg (=6)
Glue value for lev 1 cut ('give another
shot'
.TP
\fB\-\-adjustglue\fR arg (=0.7)
If more than this % of clauses is LOW
glue (level 0) then lower the glue
cutoff by 1 \fB\-\-\fR once and never again
.TP
\fB\-\-everylev1\fR arg (=10000)
Reduce lev1 clauses every N
.TP
\fB\-\-everylev2\fR arg (=15000)
Reduce lev2 clauses every N
.TP
\fB\-\-lev1usewithin\fR arg (=70000)
Learnt clause must be used in lev1
within this timeframe or be dropped to
lev2
.TP
\fB\-\-dumpred\fR arg
Dump redundant clauses of gluecut0&1 to
this filename
.TP
\fB\-\-dumpredmaxlen\fR arg (=10000)
When dumping redundant clauses, only
dump clauses at most this long
.TP
\fB\-\-dumpredmaxglue\fR arg (=1000)
When dumping redundant clauses, only
dump clauses with at most this large
glue
.PP
Clause dumping after problem finishing:
.SS "Variable branching options:"
.TP
\fB\-\-branchstr\fR arg (=maple1+maple2+vsids2+maple1+maple2+vsids1)
Branch strategy. E.g.
\&'vmtf+vsids+maple+rnd'
.SS "Conflict options:"
.TP
\fB\-\-recur\fR arg (=1)
Perform recursive minimisation
.TP
\fB\-\-moreminim\fR arg (=1)
Perform strong minimisation at conflict
gen.
.TP
\fB\-\-moremoreminim\fR arg (=1)
Perform even stronger minimisation at
conflict gen.
.TP
\fB\-\-moremorealways\fR arg (=0)
Always strong\-minimise clause
.TP
\fB\-\-decbased\fR arg (=1)
Create decision\-based conflict clauses
when the UIP clause is too large
.SS "Iterative solve options:"
.TP
\fB\-\-maxsol\fR arg (=1)
Search for given amount of solutions.
Thanks to Jannis Harder for the
decision\-based banning idea
.TP
\fB\-\-nobansol\fR
Don't ban the solution once it's found
.TP
\fB\-\-debuglib\fR arg
Parse special comments to run
solve/simplify during parsing of CNF
.SS "Probing options:"
.TP
\fB\-\-transred\fR arg (=1)
Remove useless binary clauses
(transitive reduction)
.TP
\fB\-\-intree\fR arg (=1)
Carry out intree\-based probing
.TP
\fB\-\-intreemaxm\fR arg (=1200)
Time in mega\-bogoprops to perform
intree probing
.TP
\fB\-\-otfhyper\fR arg (=1)
Perform hyper\-binary resolution during
probing
.SS "Stochastic Local Search options:"
.TP
\fB\-\-sls\fR arg (=1)
Run SLS during simplification
.TP
\fB\-\-slstype\fR arg (=ccnr)
Which SLS to run. Allowed values:
walksat, yalsat, ccnr, ccnr_yalsat
.TP
\fB\-\-slsmaxmem\fR 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.
.TP
\fB\-\-slseveryn\fR arg (=2)
Run SLS solver every N simplifications
only
.TP
\fB\-\-yalsatmems\fR arg (=40)
Run Yalsat with this many mems*million
timeout. Limits time of yalsat run
.TP
\fB\-\-walksatruns\fR arg (=50)
Max 'runs' for WalkSAT. Limits time of
WalkSAT run
.TP
\fB\-\-slsgetphase\fR arg (=1)
Get phase from SLS solver, set as new
phase for CDCL
.TP
\fB\-\-slsccnraspire\fR arg (=1)
Turn aspiration on/off for CCANR
.TP
\fB\-\-slstobump\fR arg (=100)
How many variables to bump in CCNR
.TP
\fB\-\-slstobumpmaxpervar\fR arg (=100)
How many times to bump an individual
variable's activity in CCNR
.TP
\fB\-\-slsbumptype\fR arg (=6)
How to calculate what variable to bump.
1 = clause\-based, 2 = var\-flip\-based, 3
= var\-score\-based
.TP
\fB\-\-slsoffset\fR arg (=0)
Should SLS set the VSIDS/Maple offsetsd
.SS "Simplification schedules:"
.TP
\fB\-\-schedsimp\fR arg (=1)
Perform simplification rounds. If 0, we
never perform any.
.TP
\fB\-\-presimp\fR arg (=0)
Perform simplification at the very
start
.TP
\fB\-\-allpresimp\fR arg (=0)
Perform simplification at EVERY start
\fB\-\-\fR only matters in library mode
.TP
\fB\-n\fR [ \fB\-\-nonstop\fR ] arg (=0)
Never stop the search() process in
class SATSolver
.TP
\fB\-\-maxnumsimppersolve\fR arg (=25)
Maximum number of simplifiactions to
perform for every solve() call. After
this, no more inprocessing will take
place.
.TP
\fB\-\-schedule\fR arg
Schedule for simplification during run
.TP
\fB\-\-preschedule\fR arg
Schedule for simplification at startup
.TP
\fB\-\-occsimp\fR arg (=1)
Perform occurrence\-list\-based
optimisations (variable elimination,
subsumption, bounded variable
addition...)
.TP
\fB\-\-confbtwsimp\fR arg (=50000)
Start first simplification after this
many conflicts
.TP
\fB\-\-confbtwsimpinc\fR arg (=1.4)
Simp rounds increment by this power of
N
.SS "Occ-based simplification memory limits:"
.TP
\fB\-\-occredmax\fR arg (=200)
Don't add to occur list any redundant
clause larger than this
.TP
\fB\-\-occredmaxmb\fR arg (=600)
Don't allow redundant occur size to be
beyond this many MB
.TP
\fB\-\-occirredmaxmb\fR arg (=2500)
Don't allow irredundant occur size to
be beyond this many MB
.SS "Ternary resolution:"
.TP
\fB\-\-tern\fR arg (=1)
Perform Ternary resolution'
.TP
\fB\-\-terntimelim\fR arg (=100)
Time\-out in bogoprops M of ternary
resolution as per paper 'Look\-Ahead
Versus Look\-Back for Satisfiability
Problems'
.TP
\fB\-\-ternkeep\fR arg (=6)
Keep ternary resolution clauses only if
they are touched within this multiple
of 'lev1usewithin'
.TP
\fB\-\-terncreate\fR arg (=1)
Create only this multiple (of linked in
cls) ternary resolution clauses per
simp run
.TP
\fB\-\-ternbincreate\fR arg (=1)
Allow ternary resolving to generate
binary clauses
.SS "Occ-based subsumption and strengthening time limits:"
.TP
\fB\-\-strengthen\fR arg (=1)
Perform clause contraction through
self\-subsuming resolution as part of
the occurrence\-subsumption system
.TP
\fB\-\-substimelim\fR arg (=300)
Time\-out in bogoprops M of subsumption
of long clauses with long clauses,
after computing occur
.TP
\fB\-\-substimelimbinratio\fR arg (=0.10000000000000001)
Ratio of subsumption time limit to
spend on sub&str long clauses with bin
.TP
\fB\-\-substimelimlongratio\fR arg (=0.90000000000000002)
Ratio of subsumption time limit to
spend on sub long clauses with long
.TP
\fB\-\-strstimelim\fR arg (=300)
Time\-out in bogoprops M of
strengthening of long clauses with long
clauses, after computing occur
.TP
\fB\-\-sublonggothrough\fR arg (=1)
How many times go through subsume
.SS "BVE options:"
.TP
\fB\-\-varelim\fR arg (=1)
Perform variable elimination as per Een
and Biere
.TP
\fB\-\-varelimto\fR arg (=750)
Var elimination bogoprops M time limit
.TP
\fB\-\-varelimover\fR 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...
.TP
\fB\-\-emptyelim\fR arg (=1)
Perform empty resolvent elimination
using bit\-map trick
.TP
\fB\-\-varelimmaxmb\fR arg (=1000)
Maximum extra MB of memory to use for
new clauses during varelim
.TP
\fB\-\-eratio\fR arg (=1.6)
Eliminate this ratio of free variables
at most per variable elimination
iteration
.TP
\fB\-\-skipresol\fR arg (=1)
Skip BVE resolvents in case they belong
to a gate
.SS "BVA options:"
.TP
\fB\-\-bva\fR arg (=1)
Perform bounded variable addition
.TP
\fB\-\-bvaeveryn\fR arg (=7)
Perform BVA only every N occ\-simplify
calls
.TP
\fB\-\-bvalim\fR arg (=250000)
Maximum number of variables to add by
BVA per call
.TP
\fB\-\-bva2lit\fR arg (=1)
BVA with 2\-lit difference hack, too.
Beware, this reduces the effectiveness
of 1\-lit diff
.TP
\fB\-\-bvato\fR arg (=50)
BVA time limit in bogoprops M
.SS "Equivalent literal options:"
.TP
\fB\-\-scc\fR arg (=1)
Find equivalent literals through SCC
and replace them
.SS "Component options:"
.TP
\fB\-\-comps\fR arg (=0)
Perform component\-finding and separate
handling
.TP
\fB\-\-compsfrom\fR arg (=0)
Component finding only after this many
simplification rounds
.TP
\fB\-\-compsvar\fR arg (=1000000)
Only use components in case the number
of variables is below this limit
.TP
\fB\-\-compslimit\fR arg (=500)
Limit how much time is spent in
component\-finding
.SS "Memory saving options:"
.TP
\fB\-\-renumber\fR arg (=1)
Renumber variables to increase CPU
cache efficiency
.TP
\fB\-\-savemem\fR arg (=1)
Save memory by deallocating variable
space after renumbering. Only works if
renumbering is active.
.TP
\fB\-\-mustrenumber\fR arg (=0)
Treat all 'renumber' strategies as
\&'must\-renumber'
.TP
\fB\-\-fullwatchconseveryn\fR arg (=4000000)
Consolidate watchlists fully once every
N conflicts. Scheduled during
simplification rounds.
.SS "XOR-related options:"
.TP
\fB\-\-xor\fR arg (=1)
Discover long XORs
.TP
\fB\-\-maxxorsize\fR arg (=7)
Maximum XOR size to find
.TP
\fB\-\-xorfindtout\fR arg (=400)
Time limit for finding XORs
.TP
\fB\-\-varsperxorcut\fR 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
.TP
\fB\-\-maxxormat\fR arg (=400)
Maximum matrix size (=num elements)
that we should try to echelonize
.TP
\fB\-\-forcepreservexors\fR arg (=0)
Force preserving XORs when they have
been found. Easier to make sure XORs
are not lost through simplifiactions
such as strenghtening
.TP
\fB\-\-m4ri\fR arg (=1)
Use M4RI
.SS "Gate-related options:"
.TP
\fB\-\-gates\fR arg (=0)
Find gates. Disables all sub\-options
below
.TP
\fB\-\-gorshort\fR arg (=1)
Shorten clauses with OR gates
.TP
\fB\-\-gandrem\fR arg (=1)
Remove clauses with AND gates
.TP
\fB\-\-gateeqlit\fR arg (=1)
Find equivalent literals using gates
.TP
\fB\-\-printgatedot\fR arg (=0)
Print gate structure regularly to file
\&'gatesX.dot'
.TP
\fB\-\-gatefindto\fR arg (=200)
Max time in bogoprops M to find gates
.TP
\fB\-\-shortwithgatesto\fR arg (=200)
Max time to shorten with gates,
bogoprops M
.TP
\fB\-\-remwithgatesto\fR arg (=100)
Max time to remove with gates,
bogoprops M
.SS "Gauss options:"
.TP
\fB\-\-maxmatrixrows\fR arg (=5000)
Set maximum no. of rows for gaussian
matrix. Too large matricesshould bee
discarded for reasons of efficiency
.TP
\fB\-\-autodisablegauss\fR arg (=1)
Automatically disable gauss when
performing badly
.TP
\fB\-\-minmatrixrows\fR arg (=3)
Set minimum no. of rows for gaussian
matrix. Normally, too small matrices
are discarded for reasons of efficiency
.TP
\fB\-\-maxnummatrices\fR arg (=5)
Maximum number of matrices to treat.
.TP
\fB\-\-detachxor\fR arg (=0)
Detach and reattach XORs
.TP
\fB\-\-useallmatrixes\fR arg (=0)
Force using all matrices
.TP
\fB\-\-detachverb\fR arg (=0)
If set, verbosity for XOR detach code
is upped, ignoring normal verbosity
.TP
\fB\-\-gaussusefulcutoff\fR arg (=0.20000000000000001)
Turn off Gauss if less than this many
usefulenss ratio is recorded
.SS "Distill options:"
.TP
\fB\-\-distill\fR arg (=1)
Regularly execute clause distillation
.TP
\fB\-\-distillmaxm\fR arg (=20)
Maximum number of Mega\-bogoprops(~time)
to spend on vivifying/distilling long
cls by enqueueing and propagating
.TP
\fB\-\-distillto\fR arg (=120)
Maximum time in bogoprops M for
distillation
.TP
\fB\-\-distillincconf\fR arg (=0.02)
Multiplier for current number of
conflicts OTF distill
.TP
\fB\-\-distillminconf\fR arg (=10000)
Minimum number of conflicts between OTF
distill
.TP
\fB\-\-distilltier1ratio\fR arg (=0.029999999999999999)
How much of tier 1 to distill
.SS "Reconf options:"
.TP
\fB\-\-reconfat\fR arg (=2)
Reconfigure after this many
simplifications
.TP
\fB\-\-reconf\fR arg (=0)
Reconfigure after some time to this
solver configuration
[3,4,6,7,12,13,14,15,16]
.SS "Misc options:"
.TP
\fB\-\-strmaxt\fR arg (=30)
Maximum MBP to spend on distilling long
irred cls through watches
.TP
\fB\-\-implicitmanip\fR arg (=1)
Subsume and strengthen implicit clauses
with each other
.TP
\fB\-\-implsubsto\fR arg (=100)
Timeout (in bogoprop Millions) of
implicit subsumption
.TP
\fB\-\-implstrto\fR arg (=200)
Timeout (in bogoprop Millions) of
implicit strengthening
.TP
\fB\-\-cardfind\fR arg (=0)
Find cardinality constraints
.SS "Normal run schedules:"
.IP
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
.IP
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
.SS "Preproc run schedule:"
.IP
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
.SH "BUG TRACKER"
Please don't hesitate to file any and all issues at:

https://github.com/msoos/cryptominisat/issues
.SH AUTHORS
cryptominisat5 is written and maintained by
.B Mate Soos soos.mate@gmail.com
.SH COPYRIGHT
cryptominisat5 is under the
.B MIT
license. Please see https://opensource.org/licenses/MIT for the full text
.SH "SEE ALSO"
More documentation for the cryptominisat5 SAT solver can be found at https://www.msoos.org/cryptominisat5/