cryptominisat5 man page

cryptominisat5 — manual page for cryptominisat5 5.6.3

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

See Also

The full documentation for cryptominisat5 is maintained as a Texinfo manual.  If the info and cryptominisat5 programs are properly installed at your site, the command

info cryptominisat5

should give you access to the complete manual.

Info

June 2018 cryptominisat5 5.6.3 User Commands