cryptominisat5 man page

cryptominisat5 — 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

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

Bug Tracker

Please don't hesitate to file any and all issues at:

https://github.com/msoos/cryptominisat/issues

Authors

cryptominisat5 is written and maintained by Mate Soos soos.mate@gmail.com

See Also

More documentation for the cryptominisat5 SAT solver can be found at https://www.msoos.org/cryptominisat5/

Info

August 2018 cryptominisat5 5.6.4 User Commands