Man page - cryptominisat5(1)

Packages contains this manual

Manual

CRYPTOMINISAT5

NAME
SYNOPSIS
DESCRIPTION
Positional arguments:
Optional arguments:
Normal run schedules:
SEE ALSO

NAME

cryptominisat5 - manual page for cryptominisat5 5.11.21

SYNOPSIS

cryptominisat5 [ --help ] [ --version ] [ --help VAR ] [ --version ] [ --verb VAR ] [ --maxtime VAR ] [ --maxconfl VAR ] [ --random VAR ] [ --threads VAR ] [ --mult VAR ] [ --nextm VAR ] [ --memoutmult VAR ] [ --maxsol VAR ] [ --polar VAR ] [ --scc VAR ] [ --restart VAR ] [ --rstfirst VAR ] [ --gluehist VAR ] [ --lwrbndblkrest VAR ] [ --locgmult VAR ] [ --ratiogluegeom VAR ] [ --blockingglue VAR ] [ --gluecut0 VAR ] [ --gluecut1 VAR ] [ --adjustglue VAR ] [ --everylev1 VAR ] [ --everylev2 VAR ] [ --lev1usewithin VAR ] [ --branchstr VAR ] [ --nobansol ] [ --debuglib VAR ] [ --breakid VAR ] [ --breakideveryn VAR ] [ --breakidmaxlits VAR ] [ --breakidmaxcls VAR ] [ --breakidmaxvars VAR ] [ --breakidtime VAR ] [ --breakidcls VAR ] [ --breakidmatrix VAR ] [ --sls VAR ] [ --slstype VAR ] [ --slsmaxmem VAR ] [ --slseveryn VAR ] [ --yalsatmems VAR ] [ --walksatruns VAR ] [ --slsgetphase VAR ] [ --slsccnraspire VAR ] [ --slstobump VAR ] [ --slstobumpmaxpervar VAR ] [ --slsbumptype VAR ] [ --transred VAR ] [ --intree VAR ] [ --intreemaxm VAR ] [ --otfhyper VAR ] [ --schedsimp VAR ] [ --presimp VAR ] [ --allpresimp VAR ] [ --nonstop VAR ] [ --maxnumsimppersolve VAR ] [ --schedule VAR ] [ --preschedule VAR ] [ --occsimp VAR ] [ --confbtwsimp VAR ] [ --confbtwsimpinc VAR ] [ --tern VAR ] [ --terntimelim VAR ] [ --ternkeep VAR ] [ --terncreate VAR ] [ --ternbincreate VAR ] [ --occredmax VAR ] [ --occredmaxmb VAR ] [ --occirredmaxmb VAR ] [ --strengthen VAR ] [ --weakentimelim VAR ] [ --substimelim VAR ] [ --substimelimbinratio VAR ] [ --substimelimlongratio VAR ] [ --strstimelim VAR ] [ --sublonggothrough VAR ] [ --bva VAR ] [ --bvaeveryn VAR ] [ --bvalim VAR ] [ --bva2lit VAR ] [ --bvato VAR ] [ --varelim VAR ] [ --varelimto VAR ] [ --varelimover VAR ] [ --emptyelim VAR ] [ --varelimmaxmb VAR ] [ --eratio VAR ] [ --varelimcheckres VAR ] [ --xor VAR ] [ --maxxorsize VAR ] [ --xorfindtout VAR ] [ --varsperxorcut VAR ] [ --maxxormat VAR ] [ --forcepreservexors VAR ] [ --gates VAR ] [ --printgatedot VAR ] [ --gatefindto VAR ] [ --recur VAR ] [ --moreminim VAR ] [ --moremoreminim VAR ] [ --moremorealways VAR ] [ --decbased VAR ] [ --updateglueonanalysis VAR ] [ --maxgluehistltlimited VAR ] [ --diffdeclevelchrono VAR ] [ --verbstat VAR ] [ --verbrestart VAR ] [ --verballrestarts VAR ] [ --printsol,s VAR ] [ --restartprint VAR ] [ --distill VAR ] [ --distillbin VAR ] [ --distillmaxm VAR ] [ --distillincconf VAR ] [ --distillminconf VAR ] [ --distilltier0ratio VAR ] [ --distilltier1ratio VAR ] [ --distillirredalsoremratio VAR ] [ --distillirrednoremratio VAR ] [ --distillshuffleeveryn VAR ] [ --distillsort VAR ] [ --renumber VAR ] [ --mustconsolidate VAR ] [ --savemem VAR ] [ --mustrenumber VAR ] [ --fullwatchconseveryn VAR ] [ --strmaxt VAR ] [ --implicitmanip VAR ] [ --implsubsto VAR ] [ --implstrto VAR ] [ --cardfind VAR ] [ --sync VAR ] [ --clearinter VAR ] [ --zero-exit-status ] [ --printtimes VAR ] [ --maxsccdepth VAR ] [ --simfrat VAR ] [ --sampling VAR ] [ --onlysampling ] [ --assump VAR ] [ --maxmatrixrows VAR ] [ --maxmatrixcols VAR ] [ --autodisablegauss VAR ] [ --minmatrixrows VAR ] [ --maxnummatrices VAR ] [ --detachxor VAR ] [ --useallmatrixes VAR ] [ --detachverb VAR ] [ --gaussusefulcutoff VAR ] [ --dumpresult VAR ] files

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 [frat-file]

Positional arguments:

files

input file and FRAT output [nargs: 0 or more]

Optional arguments:

-h , --help

shows help message and exits

-v , --version

prints version information and exits

-h , --help

Print extensive help [nargs=0..1] [default: false]

-v , --version

Print version info

--verb

[0-10] Verbosity of solver. 0 = only solution [nargs=0..1] [default: 1]

--maxtime

Stop solving after this much time (s)

--maxconfl

Stop solving after this many conflicts

-r , --random

[0..] Random seed [nargs=0..1] [default: 0]

-t , --threads

Number of threads [nargs=0..1] [default: 1]

-m , --mult

Time multiplier for all simplification cutoffs [nargs=0..1] [default: 3]

--nextm

Global multiplier when the next inprocessing should take place [nargs=0..1] [default: 1]

--memoutmult

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 [nargs=0..1] [default: 1]

--maxsol

Search for given amount of solutions. Thanks to Jannis Harder for the decision-based banning idea [nargs=0..1] [default: 1]

--polar

{true,false,rnd,auto,stable} 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ā€™) [nargs=0..1] [default: "auto"]

--scc

Find equivalent literals through SCC and replace them [nargs=0..1] [default: 1]

--restart

{geom, glue, luby} Restart strategy to follow. [nargs=0..1] [default: "auto"]

--rstfirst

The size of the base restart [nargs=0..1] [default: 100]

--gluehist

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 [nargs=0..1] [default: 50]

--lwrbndblkrest

Lower bound on blocking restart -- donā€™t block before this many conflicts [nargs=0..1] [default: 10000]

--locgmult

The multiplier used to determine if we should restart during glue-based restart [nargs=0..1] [default: 0.8]

--ratiogluegeom

Ratio of glue vs geometric restarts -- more is more glue [nargs=0..1] [default: 5]

--blockingglue

Do blocking restart for glues [nargs=0..1] [default: 1]

--gluecut0

Glue value for lev 0 (ā€™keepā€™) cut [nargs=0..1] [default: 3]

--gluecut1

Glue value for lev 1 cut (ā€™give another shotā€™ [nargs=0..1] [default: 6]

--adjustglue

If more than this % of clauses is LOW glue (level 0) then lower the glue cutoff by 1 -- once and never again [nargs=0..1] [default: 0.7]

--everylev1

Reduce lev1 clauses every N [nargs=0..1] [default: 10000]

--everylev2

Reduce lev2 clauses every N [nargs=0..1] [default: 15000]

--lev1usewithin

Learnt clause must be used in lev1 within this timeframe or be dropped to lev2 [nargs=0..1] [default: 70000]

--branchstr

Branch strategy string that switches between different branch strategies while solving e.g. ā€™vsids1+vsids2ā€™ [nargs=0..1] [default: "vmtf+vsids"]

--nobansol

Donā€™t ban the solution once itā€™s found

--debuglib

Parse special comments to run solve/simplify during parsing of CNF

--breakid

Run BreakID to break symmetries. [nargs=0..1] [default: true]

--breakideveryn

Run BreakID every N simplification iterations [nargs=0..1] [default: 5]

--breakidmaxlits

Maximum number of literals in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 3500]

--breakidmaxcls

Maximum number of clauses in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 600]

--breakidmaxvars

Maximum number of variables in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 300]

--breakidtime

Maximum number of steps taken during automorphism finding. [nargs=0..1] [default: 2000]

--breakidcls

Maximum number of breaking clauses per permutation. [nargs=0..1] [default: 50]

--breakidmatrix

Detect matrix row interchangability [nargs=0..1] [default: true]

--sls

Run SLS during simplification [nargs=0..1] [default: 1]

--slstype

Which SLS to run. Allowed values: walksat, yalsat, ccnr, ccnr_yalsat [nargs=0..1] [default: "ccnr"]

--slsmaxmem

Maximum number of MB to give to SLS solver. Doesnā€™t run SLS solver if the memory usage would be more than this. [nargs=0..1] [default: 500]

--slseveryn

Run SLS solver every N simplifications only [nargs=0..1] [default: 2]

--yalsatmems

Run Yalsat with this many mems*million timeout. Limits time of yalsat run [nargs=0..1] [default: 10]

--walksatruns

Max ā€™runsā€™ for WalkSAT. Limits time of WalkSAT run [nargs=0..1] [default: 50]

--slsgetphase

Get phase from SLS solver, set as new phase for CDCL [nargs=0..1] [default: 1]

--slsccnraspire

Turn aspiration on/off for CCANR [nargs=0..1] [default: 1]

--slstobump

How many variables to bump in CCNR [nargs=0..1] [default: 100]

--slstobumpmaxpervar

How many times to bump an individual variableā€™s activity in CCNR [nargs=0..1] [default: 100]

--slsbumptype

How to calculate what variable to bump. 1 = clause-based, 2 = var-flip-based, 3 = var-score-based [nargs=0..1] [default: 6]

--transred

Remove useless binary clauses (transitive reduction) [nargs=0..1] [default: 1]

--intree

Carry out intree-based probing [nargs=0..1] [default: 1]

--intreemaxm

Time in mega-bogoprops to perform intree probing [nargs=0..1] [default: 400]

--otfhyper

Perform hyper-binary resolution during probing [nargs=0..1] [default: 1]

--schedsimp

Perform simplification rounds. If 0, we never perform any. [nargs=0..1] [default: 1]

--presimp

Perform simplification at the very start [nargs=0..1] [default: 0]

--allpresimp

Perform simplification at EVERY start -- only matters in library mode [nargs=0..1] [default: 0]

-n , --nonstop

Never stop the search() process in class SATSolver [nargs=0..1] [default: 0]

--maxnumsimppersolve

Maximum number of simplifiactions to perform for every solve() call. After this, no more inprocessing will take place. [nargs=0..1] [default: 25]

--schedule

Schedule for simplification during run

--preschedule

Schedule for simplification at startup

--occsimp

Perform occurrence-list-based optimisations (variable elimination, subsumption, bounded variable addition...) [nargs=0..1] [default: 1]

--confbtwsimp

Start first simplification after this many conflicts [nargs=0..1] [default: 40000]

--confbtwsimpinc

Simp rounds increment by this power of N [nargs=0..1] [default: 1.4]

--tern

Perform Ternary resolution [nargs=0..1] [default: true]

--terntimelim

Time-out in bogoprops M of ternary resolution as per paper ā€™Look-Ahead Versus Look-Back for Satisfiability Problemsā€™ [nargs=0..1] [default: 100]

--ternkeep

Keep ternary resolution clauses only if they are touched within this multiple of ā€™lev1usewithinā€™ [nargs=0..1] [default: 5]

--terncreate

Create only this multiple (of linked in cls) ternary resolution clauses per simp run [nargs=0..1] [default: 0.3]

--ternbincreate

Allow ternary resolving to generate binary clauses [nargs=0..1] [default: 0]

--occredmax

Donā€™t add to occur list any redundant clause larger than this [nargs=0..1] [default: 50]

--occredmaxmb

Donā€™t allow redundant occur size to be beyond this many MB [nargs=0..1] [default: 600]

--occirredmaxmb

Donā€™t allow irredundant occur size to be beyond this many MB [nargs=0..1] [default: 2500]

--strengthen

Perform clause contraction through self-subsuming resolution as part of the occurrence-subsumption system [nargs=0..1] [default: 1]

--weakentimelim

Time-out in bogoprops M of weakeaning used [nargs=0..1] [default: 300]

--substimelim

Time-out in bogoprops M of subsumption of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]

--substimelimbinratio

Ratio of subsumption time limit to spend on sub&str long clauses with bin [nargs=0..1] [default: 0.1]

--substimelimlongratio

Ratio of subsumption time limit to spend on sub long clauses with long [nargs=0..1] [default: 0.9]

--strstimelim

Time-out in bogoprops M of strengthening of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]

--sublonggothrough

How many times go through subsume [nargs=0..1] [default: 1]

--bva

Perform bounded variable addition [nargs=0..1] [default: 1]

--bvaeveryn

Perform BVA only every N occ-simplify calls [nargs=0..1] [default: 7]

--bvalim

Maximum number of variables to add by BVA per call [nargs=0..1] [default: 250000]

--bva2lit

BVA with 2-lit difference hack, too. Beware, this reduces the effectiveness of 1-lit diff [nargs=0..1] [default: 1]

--bvato

BVA time limit in bogoprops M [nargs=0..1] [default: 50]

--varelim

Perform variable elimination as per Een and Biere [nargs=0..1] [default: 1]

--varelimto

Var elimination bogoprops M time limit [nargs=0..1] [default: 750]

--varelimover

Do BVE until the resulting no. of clause increase is less than X. Only power of 2 makes sense, i.e. 2,4,8... [nargs=0..1] [default: 16]

--emptyelim

Perform empty resolvent elimination using bit-map trick [nargs=0..1] [default: 1]

--varelimmaxmb

Maximum extra MB of memory to use for new clauses during varelim [nargs=0..1] [default: 1000]

--eratio

Eliminate this ratio of free variables at most per variable elimination iteration [nargs=0..1] [default: 1.6]

--varelimcheckres

BVE should check whether resolvents subsume others and check for exact size increase [nargs=0..1] [default: 0]

--xor

Discover long XORs [nargs=0..1] [default: 1]

--maxxorsize

Maximum XOR size to find [nargs=0..1] [default: 7]

--xorfindtout

Time limit for finding XORs [nargs=0..1] [default: 400]

--varsperxorcut

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 [nargs=0..1] [default: 2]

--maxxormat

Maximum matrix size (=num elements) that we should try to echelonize [nargs=0..1] [default: 400]

--forcepreservexors

Force preserving XORs when they have been found. Easier to make sure XORs are not lost through simplifiactions such as strenghtening [nargs=0..1] [default: 1]

--gates

Find gates. [nargs=0..1] [default: 0]

--printgatedot

Print gate structure regularly to file ā€™gatesX.dotā€™ [nargs=0..1] [default: 0]

--gatefindto

Max time in bogoprops M to find gates [nargs=0..1] [default: 200]

--recur

Perform recursive minimisation [nargs=0..1] [default: 1]

--moreminim

Perform strong minimisation at conflict gen. [nargs=0..1] [default: 1]

--moremoreminim

Perform even stronger minimisation at conflict gen. [nargs=0..1] [default: 2]

--moremorealways

Always strong-minimise clause [nargs=0..1] [default: 0]

--decbased

Create decision-based conflict clauses when the UIP clause is too large [nargs=0..1] [default: 1]

--updateglueonanalysis

Update glues while analyzing [nargs=0..1] [default: 1]

--maxgluehistltlimited

Maximum glue used by glue-based restart strategy when populating glue history. [nargs=0..1] [default: 50]

--diffdeclevelchrono

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). [nargs=0..1] [default: 20]

--verbstat

Change verbosity of statistics at the end of the solving [0..3] [nargs=0..1] [default: 2]

--verbrestart

Print more thorough, but different stats [nargs=0..1] [default: 0]

--verballrestarts

Print a line for every restart [nargs=0..1] [default: 0]

--printsol ,s

Print assignment if solution is SAT [nargs=0..1] [default: 1]

--restartprint

Print restart status lines at least every N conflicts [nargs=0..1] [default: 8192]

--distill

Regularly execute clause distillation [nargs=0..1] [default: 1]

--distillbin

Regularly execute clause distillation [nargs=0..1] [default: 1]

--distillmaxm

Maximum number of Mega-bogoprops(Ėœtime) to spend on vivifying/distilling long cls by enqueueing and propagating [nargs=0..1] [default: 20]

--distillincconf

Multiplier for current number of conflicts OTF distill [nargs=0..1] [default: 0.1]

--distillminconf

Minimum number of conflicts between OTF distill [nargs=0..1] [default: 10000]

--distilltier0ratio

How much of tier 0 to distill [nargs=0..1] [default: 10]

--distilltier1ratio

How much of tier 1 to distill [nargs=0..1] [default: 0.03]

--distillirredalsoremratio

How much of irred to distill when doing also removal [nargs=0..1] [default: 1.2]

--distillirrednoremratio

How much of irred to distill when doing no removal [nargs=0..1] [default: 1]

--distillshuffleeveryn

Shuffle to-be-distilled clauses every N cases randomly [nargs=0..1] [default: 3]

--distillsort

Distill sorting type [nargs=0..1] [default: 1]

--renumber

Renumber variables to increase CPU cache efficiency [nargs=0..1] [default: 1]

--mustconsolidate

Always consolidate, even if not useful. This is used for debugging ONLY [nargs=0..1] [default: 0]

--savemem

Save memory by deallocating variable space after renumbering. Only works if renumbering is active. [nargs=0..1] [default: 1]

--mustrenumber

Treat all ā€™renumberā€™ strategies as ā€™must-renumberā€™ [nargs=0..1] [default: 0]

--fullwatchconseveryn

Consolidate watchlists fully once every N conflicts. Scheduled during simplification rounds. [nargs=0..1] [default: 4000000]

--strmaxt

Maximum MBP to spend on distilling long irred cls through watches [nargs=0..1] [default: 20]

--implicitmanip

Subsume and strengthen implicit clauses with each other [nargs=0..1] [default: 1]

--implsubsto

Timeout (in bogoprop Millions) of implicit subsumption [nargs=0..1] [default: 100]

--implstrto

Timeout (in bogoprop Millions) of implicit strengthening [nargs=0..1] [default: 200]

--cardfind

Find cardinality constraints [nargs=0..1] [default: 0]

--sync

Sync threads every N conflicts [nargs=0..1] [default: 7000]

--clearinter

Interrupt threads cleanly, all the time [nargs=0..1] [default: 0]

--zero-exit-status

Exit with status zero in case the solving has finished without an issue

--printtimes

Print time it took for each simplification run. If set to 0, logs are easier to compare [nargs=0..1] [default: 1]

--maxsccdepth

The maximum for scc search depth [nargs=0..1] [default: 10000]

--simfrat

Simulate FRAT [nargs=0..1] [default: 0]

--sampling

Sampling vars, separated by comma [nargs=0..1] [default: ""]

--onlysampling

Print and ban(!) solutionsā€™ vars only in ā€™c indā€™ or as --sampling ā€™...ā€™

--assump

Assumptions file [nargs=0..1] [default: ""]

--maxmatrixrows

Set maximum no. of rows for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 2000]

--maxmatrixcols

Set maximum no. of columns for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 1000]

--autodisablegauss

Automatically disable gauss when performing badly [nargs=0..1] [default: true]

--minmatrixrows

Set minimum no. of rows for gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency [nargs=0..1] [default: 3]

--maxnummatrices

Maximum number of matrices to treat. [nargs=0..1] [default: 5]

--detachxor

Detach and reattach XORs [nargs=0..1] [default: false]

--useallmatrixes

Force using all matrices [nargs=0..1] [default: false]

--detachverb

If set, verbosity for XOR detach code is upped, ignoring normal verbosity [nargs=0..1] [default: 0]

--gaussusefulcutoff

Turn off Gauss if less than this many usefulenss ratio is recorded [nargs=0..1] [default: 0.2]

--dumpresult

Write solution(s) to this file

Normal run schedules:

Default schedule: scc-vrepl,sub-impl,breakid,occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,card-find,cl-consolidate,scc-vrepl,renumber,bosphorus,louvain-comms

Schedule at startup: sub-impl, occ-backw-sub,scc-vrepl,breakid, occ-bve,occ-xor

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.