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