Provided by: cryptominisat_5.6.4+dfsg.1-1ubuntu1_amd64 
NAME
cryptominisat5 - a 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 (=MAX)
Stop solving after this much time (s)
--maxconfl arg (=MAX)
Stop solving after this many conflicts
-m [ --mult ] arg (=4)
Time multiplier for all simplification cutoffs
--memoutmult arg (=1)
Multiplier for memory-out checks on variables and clause-link-in, etc. Useful when
you have limited memory.
-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')
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
--blkrest arg (=1)
Perform blocking restarts as per Glucose 3.0
--blkrestlen arg (=5000)
Length of the long term trail size for blocking restart
--blkrestmultip arg (=1.4)
Multiplier used for blocking restart cut-off (called 'R' in Glucose 3.0)
--lwrbndblkrest arg (=10000)
Lower bound on blocking restart -- don't block before this many conflicts
--locgmult arg (=0.80000000000000004) The multiplier used to determine if we
should restart during glue-based restart
--brokengluerest arg (=1)
Should glue restart be broken as before 8e74cb5010bb4
--ratiogluegeom arg (=5)
Ratio of glue vs geometric restarts -- more is more glue
Printing options:
--verbstat arg (=1)
Change verbosity of statistics at the end of the solving [0..2]
--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 (=4096)
Print restart status lines at least every N conflicts
Propagation options:
--updateglueonanalysis arg (=1)
Update glues while analyzing
--otfhyper arg (=1)
Perform hyper-binary resolution at dec. level 1 after every restart and during
probing
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
--ml arg (=0)
Use ML model to guess clause effectiveness
--everylev1 arg (=10000)
Reduce lev1 clauses every N
--everylev2 arg (=15000)
Reduce lev2 clauses every N
--lev1usewithin arg (=30000)
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
Variable branching options:
--vardecaystart arg (=0.8)
variable activity increase divider (MUST be smaller than multiplier)
--vardecaymax arg (=0.95)
variable activity increase divider (MUST be smaller than multiplier)
--vincstart arg (=1)
variable activity increase stars with this value. Make sure that this multiplied by
multiplier and divided by divider is larger than itself
--freq arg (=0)
[0 - 1] freq. of picking var at random
--maple arg (=1)
Use maple-type variable picking sometimes
--maplemod arg (=3)
Use maple N-1 of N rounds. Normally, N is 2, so used every other round. Set to 3 so
it will use maple 2/3rds of the time.
--maplemorebump arg (=0)
Bump variable usefulness more when glue is HIGH
Conflict options:
--recur arg (=1)
Perform recursive minimisation
--moreminim arg (=1)
Perform strong minimisation at conflict gen.
--moremoreminim arg (=0)
Perform even stronger minimisation at conflict gen.
--moremorecachelimit arg (=400)
Time-out in microsteps for each more minimisation with cache. Only active if
'moreminim' is on
--moremorestamp arg (=0)
Use cache for otf more minim of learnt clauses
--moremorealways arg (=0)
Always strong-minimise clause
--otfsubsume arg (=0)
Perform on-the-fly subsumption
Iterative solve options:
--maxsol arg (=1)
Search for given amount of solutions
--debuglib arg
MainSolver at specific 'solve()' points in CNF file
--dumpresult arg
Write solution(s) to this file
Probing options:
--bothprop arg (=1)
Do propagations solely to propagate the same value twice
--probe arg (=0)
Carry out probing
--probemaxm arg (=800)
Time in mega-bogoprops to perform probing
--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
Stamping options:
--stamp arg (=0)
Use time stamping as per Heule&Jarvisalo&Biere paper
--cache arg (=0)
Use implication cache -- may use a lot of memory
--cachesize arg (=2048)
Maximum size of the implication cache in MB. It may temporarily reach higher usage,
but will be deleted&disabled if this limit is reached.
--cachecutoff arg (=2000)
If the number of literals propagated by a literal is more than this, it's not
included into the implication cache
Simplification options:
--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
--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.3999999999999999)
Simp rounds increment by this power of N
--varelim arg (=1)
Perform variable elimination as per Een and Biere
--varelimto arg (=350)
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
--strengthen arg (=1)
Perform clause contraction through self-subsuming resolution as part of the
occurrence-subsumption system
--bva arg (=0)
Perform bounded variable addition
--bvalim arg (=150000)
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 (=100)
BVA time limit in bogoprops M
--eratio arg (=norm: 1.6 preproc: 1)
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
--occredmax arg (=200)
Don't add to occur list any redundant clause larger than this
--occirredmaxmb arg (=2500)
Don't allow irredundant occur size to be beyond this many MB
--occredmaxmb arg (=600)
Don't allow redundant occur size to be beyond this many MB
--substimelim arg (=300)
Time-out in bogoprops M of subsumption of long clauses with long clauses, after
computing occur
--strstimelim arg (=300)
Time-out in bogoprops M of strengthening of long clauses with long clauses, after
computing occur
--agrelimtimelim arg (=300)
Time-out in bogoprops M of aggressive(=uses reverse distillation) var-elimination
Equivalent literal options:
--scc arg (=1)
Find equivalent literals through SCC and replace them
--extscc arg (=1)
Perform SCC using cache
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
XOR-related options:
--xor arg (=1)
Discover long XORs
--xorcache arg (=0)
Use cache when finding XORs. Finds a LOT more XORs, but takes a lot more time
--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
--echelonxor arg (=1)
Extract data from XORs through echelonization (TOP LEVEL ONLY)
--maxxormat arg (=400)
Maximum matrix size (=num elements) that we should try to echelonize
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
Misc 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
Reconf options:
--reconfat arg (=2)
Reconfigure after this many simplifications
--reconf arg (=0)
Reconfigure after some time to this solver configuration [0..15]
Misc options:
--strcachemaxm arg (=30)
Maximum number of Mega-bogoprops(~time) to spend on vivifying long irred cls
through watches, cache and stamps
--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.
--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
Normal run schedules:
Default schedule: handle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl,
intree-probe, probe,sub-str-cls-with-bin, distill-cls,scc-vrepl, sub-impl,
str-impl, sub-impl,occ-backw-sub-str, occ-clean-implicit, occ-bve, occ-bva,
occ-xor,str-impl, cache-clean, sub-str-cls-with-bin, distill-cls,scc-vrepl,
check-cache-size, renumber
Schedule at startup: sub-impl,occ-backw-sub-str, occ-clean-implicit,
occ-bve,occ-backw-sub-str, occ-xor,scc-vrepl,sub-cls-with-bin
Preproc run schedule:
handle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl,sub-str-cls-with-bin,
distill-cls, scc-vrepl, sub-impl,occ-backw-sub-str, occ-xor, occ-clean-implicit,
occ-bve, occ-bva,str-impl, cache-clean, sub-str-cls-with-bin, distill-cls,
scc-vrepl, sub-impl,str-impl, sub-impl, sub-str-cls-with-bin,intree-probe,
probe,must-renumber
AUTHORS
cryptominisat was primarily written by Mate Soos.
SEE ALSO
Full documentation for the cryptominisat suite can be found at
https://www.msoos.org/cryptominisat5/