Provided by: cryptominisat_5.6.4+dfsg.1-1ubuntu1_amd64 bug


       cryptominisat5 - a SAT solver


       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

              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

   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 ''

       --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,


       cryptominisat was primarily written by Mate Soos.


       Full    documentation    for    the    cryptominisat    suite    can    be    found     at