1CRYPTOMINISAT5(1)                User Commands               CRYPTOMINISAT5(1)
2
3
4

NAME

6       cryptominisat5 - SAT solver
7

DESCRIPTION

9       A universal, fast SAT solver with XOR and Gaussian Elimination support.
10       Input can be either plain or gzipped DIMACS with XOR extension
11
12       cryptominisat5 [options] inputfile [drat-trim-file]
13
14   Preprocessor usage:
15              cryptominisat5   --preproc   1   [options]   inputfile   simpli‐
16              fied-cnf-file
17
18              cryptominisat5 --preproc 2 [options] solution-file
19
20   Main options:
21       -h [ --help ]
22              Print simple help
23
24       --hhelp
25              Print extensive help
26
27       -v [ --version ]
28              Print version info
29
30       --verb arg (=1)
31              [0-10] Verbosity of solver. 0 = only solution
32
33       -r [ --random ] arg (=0)
34              [0..] Random seed
35
36       -t [ --threads ] arg (=1)
37              Number of threads
38
39       --maxtime arg
40              Stop solving after this much time (s)
41
42       --maxconfl arg
43              Stop solving after this many conflicts
44
45       -m [ --mult ] arg (=3)
46              Time multiplier for all simplification cutoffs
47
48       --memoutmult arg (=1)
49              Multiplier  for  memory-out checks on inprocessing functions. It
50              limits things such as clause-link-in. Useful when you have  lim‐
51              ited memory but still want to do some inprocessing
52
53       -p [ --preproc ] arg (=0)
54              0  = normal run, 1 = preprocess and dump, 2 = read back dump and
55              solution to produce final solution
56
57   Polarity options:
58       --polar arg (=auto)
59              {true,false,rnd,auto} Selects polarity mode. 'true'  ->  selects
60              only  positive  polarity when branching. 'false' -> selects only
61              negative polarity when branching. 'auto' -> selects last  polar‐
62              ity used (also called 'caching')
63
64       --polarstablen arg (=4)
65              When  to  use  stable polarities. 0 = always, otherwise every n.
66              Negative is special, see code
67
68       --lucky arg (=20)
69              Try computing lucky polarities
70
71       --polarbestinvmult arg (=9)
72              How often should we use inverted best polarities instead of sta‐
73              ble
74
75       --polarbestmult arg (=1000)
76              How often should we use best polarities instead of stable
77
78   SQL options:
79       --sql arg (=0)
80              Write to SQL. 0 = no SQL, 1 or 2 = sqlite
81
82       --sqlitedb arg
83              Where to put the SQLite database
84
85       --sqlitedboverwrite arg (=0)
86              Overwrite the SQLite database file if it exists
87
88       --cldatadumpratio arg (=0.01)
89              Only  dump this ratio of clauses' data, randomly selected. Since
90              machine learning doesn't need that much data,  this  can  reduce
91              the data you have to deal with.
92
93       --cllockdatagen arg (=0.10000000000000001)
94              Lock for data generation into lev0, setting locked_for_data_gen.
95              Only works when clause is marked for  dumping  ('--cldatadumpra‐
96              tio' )
97
98   Restart options:
99       --restart arg
100              {geom, glue, luby}  Restart strategy to follow.
101
102       --gluehist arg (=50)
103              The size of the moving window for short-term glue history of re‐
104              dundant clauses. If higher, the minimal number of conflicts  be‐
105              tween restarts is longer
106
107       --lwrbndblkrest arg (=10000)
108              Lower  bound on blocking restart -- don't block before this many
109              conflicts
110
111       --locgmult arg (=0.8)
112              The multiplier used to determine if  we  should  restart  during
113              glue-based restart
114
115       --ratiogluegeom arg (=5)
116              Ratio of glue vs geometric restarts -- more is more glue
117
118   Printing options:
119       --verbstat arg (=2)
120              Change verbosity of statistics at the end of the solving [0..3]
121
122       --verbrestart arg (=0)
123              Print more thorough, but different stats
124
125       --verballrestarts arg (=0)
126              Print a line for every restart
127
128       -s [ --printsol ] arg (=1)
129              Print assignment if solution is SAT
130
131       --restartprint arg (=8192)
132              Print restart status lines at least every N conflicts
133
134       --dumpresult arg
135              Write solution(s) to this file
136
137   Glue options:
138       --updateglueonanalysis arg (=1)
139              Update glues while analyzing
140
141       --maxgluehistltlimited arg (=50)
142              Maximum glue used by glue-based restart strategy when populating
143              glue history.
144
145   Propagation options:
146       --diffdeclevelchrono arg (=20)
147              Difference in decision level is more than this,  perform  chono‐
148              logical  backtracking instead of non-chronological backtracking.
149              Giving -1  means  it  is  never  turned  on  (overrides  '--con‐
150              fltochrono -1' in this case).
151
152   Redundant clause options:
153       --gluecut0 arg (=3)
154              Glue value for lev 0 ('keep') cut
155
156       --gluecut1 arg (=6)
157              Glue value for lev 1 cut ('give another shot'
158
159       --adjustglue arg (=0.7)
160              If  more than this % of clauses is LOW glue (level 0) then lower
161              the glue cutoff by 1 -- once and never again
162
163       --everylev1 arg (=10000)
164              Reduce lev1 clauses every N
165
166       --everylev2 arg (=15000)
167              Reduce lev2 clauses every N
168
169       --lev1usewithin arg (=70000)
170              Learnt clause must be used in lev1 within this timeframe  or  be
171              dropped to lev2
172
173       --dumpred arg
174              Dump redundant clauses of gluecut0&1 to this filename
175
176       --dumpredmaxlen arg (=10000)
177              When  dumping  redundant clauses, only dump clauses at most this
178              long
179
180       --dumpredmaxglue arg (=1000)
181              When dumping redundant clauses, only dump clauses with  at  most
182              this large glue
183
184       Clause dumping after problem finishing:
185
186   Variable branching options:
187       --branchstr arg (=maple1+maple2+vsids2+maple1+maple2+vsids1)
188              Branch strategy. E.g.  'vmtf+vsids+maple+rnd'
189
190   Conflict options:
191       --recur arg (=1)
192              Perform recursive minimisation
193
194       --moreminim arg (=1)
195              Perform strong minimisation at conflict gen.
196
197       --moremoreminim arg (=1)
198              Perform even stronger minimisation at conflict gen.
199
200       --moremorealways arg (=0)
201              Always strong-minimise clause
202
203       --decbased arg (=1)
204              Create  decision-based  conflict  clauses when the UIP clause is
205              too large
206
207   Iterative solve options:
208       --maxsol arg (=1)
209              Search for given amount of solutions.  Thanks to  Jannis  Harder
210              for the decision-based banning idea
211
212       --nobansol
213              Don't ban the solution once it's found
214
215       --debuglib arg
216              Parse  special  comments to run solve/simplify during parsing of
217              CNF
218
219   Probing options:
220       --transred arg (=1)
221              Remove useless binary clauses (transitive reduction)
222
223       --intree arg (=1)
224              Carry out intree-based probing
225
226       --intreemaxm arg (=1200)
227              Time in mega-bogoprops to perform intree probing
228
229       --otfhyper arg (=1)
230              Perform hyper-binary resolution during probing
231
232   Stochastic Local Search options:
233       --sls arg (=1)
234              Run SLS during simplification
235
236       --slstype arg (=ccnr)
237              Which  SLS  to  run.  Allowed  values:  walksat,  yalsat,  ccnr,
238              ccnr_yalsat
239
240       --slsmaxmem arg (=500)
241              Maximum  number  of  MB  to  give to SLS solver. Doesn't run SLS
242              solver if the memory usage would be more than this.
243
244       --slseveryn arg (=2)
245              Run SLS solver every N simplifications only
246
247       --yalsatmems arg (=40)
248              Run Yalsat with this many mems*million timeout. Limits  time  of
249              yalsat run
250
251       --walksatruns arg (=50)
252              Max 'runs' for WalkSAT. Limits time of WalkSAT run
253
254       --slsgetphase arg (=1)
255              Get phase from SLS solver, set as new phase for CDCL
256
257       --slsccnraspire arg (=1)
258              Turn aspiration on/off for CCANR
259
260       --slstobump arg (=100)
261              How many variables to bump in CCNR
262
263       --slstobumpmaxpervar arg (=100)
264              How many times to bump an individual variable's activity in CCNR
265
266       --slsbumptype arg (=6)
267              How  to  calculate what variable to bump.  1 = clause-based, 2 =
268              var-flip-based, 3 = var-score-based
269
270       --slsoffset arg (=0)
271              Should SLS set the VSIDS/Maple offsetsd
272
273   Simplification schedules:
274       --schedsimp arg (=1)
275              Perform simplification rounds. If 0, we never perform any.
276
277       --presimp arg (=0)
278              Perform simplification at the very start
279
280       --allpresimp arg (=0)
281              Perform simplification at EVERY start -- only matters in library
282              mode
283
284       -n [ --nonstop ] arg (=0)
285              Never stop the search() process in class SATSolver
286
287       --maxnumsimppersolve arg (=25)
288              Maximum  number  of simplifiactions to perform for every solve()
289              call. After this, no more inprocessing will take place.
290
291       --schedule arg
292              Schedule for simplification during run
293
294       --preschedule arg
295              Schedule for simplification at startup
296
297       --occsimp arg (=1)
298              Perform occurrence-list-based optimisations  (variable  elimina‐
299              tion, subsumption, bounded variable addition...)
300
301       --confbtwsimp arg (=50000)
302              Start first simplification after this many conflicts
303
304       --confbtwsimpinc arg (=1.4)
305              Simp rounds increment by this power of N
306
307   Occ-based simplification memory limits:
308       --occredmax arg (=200)
309              Don't add to occur list any redundant clause larger than this
310
311       --occredmaxmb arg (=600)
312              Don't allow redundant occur size to be beyond this many MB
313
314       --occirredmaxmb arg (=2500)
315              Don't allow irredundant occur size to be beyond this many MB
316
317   Ternary resolution:
318       --tern arg (=1)
319              Perform Ternary resolution'
320
321       --terntimelim arg (=100)
322              Time-out  in  bogoprops  M  of  ternary  resolution as per paper
323              'Look-Ahead Versus Look-Back for Satisfiability Problems'
324
325       --ternkeep arg (=6)
326              Keep ternary resolution clauses only if they are touched  within
327              this multiple of 'lev1usewithin'
328
329       --terncreate arg (=1)
330              Create  only this multiple (of linked in cls) ternary resolution
331              clauses per simp run
332
333       --ternbincreate arg (=1)
334              Allow ternary resolving to generate binary clauses
335
336   Occ-based subsumption and strengthening time limits:
337       --strengthen arg (=1)
338              Perform clause contraction through self-subsuming resolution  as
339              part of the occurrence-subsumption system
340
341       --substimelim arg (=300)
342              Time-out in bogoprops M of subsumption of long clauses with long
343              clauses, after computing occur
344
345       --substimelimbinratio arg (=0.10000000000000001)
346              Ratio of subsumption time limit to spend on sub&str long clauses
347              with bin
348
349       --substimelimlongratio arg (=0.90000000000000002)
350              Ratio  of  subsumption  time  limit to spend on sub long clauses
351              with long
352
353       --strstimelim arg (=300)
354              Time-out in bogoprops M of strengthening of  long  clauses  with
355              long clauses, after computing occur
356
357       --sublonggothrough arg (=1)
358              How many times go through subsume
359
360   BVE options:
361       --varelim arg (=1)
362              Perform variable elimination as per Een and Biere
363
364       --varelimto arg (=750)
365              Var elimination bogoprops M time limit
366
367       --varelimover arg (=32)
368              Do  BVE  until the resulting no. of clause increase is less than
369              X. Only power of 2 makes sense, i.e. 2,4,8...
370
371       --emptyelim arg (=1)
372              Perform empty resolvent elimination using bit-map trick
373
374       --varelimmaxmb arg (=1000)
375              Maximum extra MB of memory to use for new clauses during varelim
376
377       --eratio arg (=1.6)
378              Eliminate this ratio of free  variables  at  most  per  variable
379              elimination iteration
380
381       --skipresol arg (=1)
382              Skip BVE resolvents in case they belong to a gate
383
384   BVA options:
385       --bva arg (=1)
386              Perform bounded variable addition
387
388       --bvaeveryn arg (=7)
389              Perform BVA only every N occ-simplify calls
390
391       --bvalim arg (=250000)
392              Maximum number of variables to add by BVA per call
393
394       --bva2lit arg (=1)
395              BVA  with  2-lit difference hack, too.  Beware, this reduces the
396              effectiveness of 1-lit diff
397
398       --bvato arg (=50)
399              BVA time limit in bogoprops M
400
401   Equivalent literal options:
402       --scc arg (=1)
403              Find equivalent literals through SCC and replace them
404
405   Component options:
406       --comps arg (=0)
407              Perform component-finding and separate handling
408
409       --compsfrom arg (=0)
410              Component finding only after this many simplification rounds
411
412       --compsvar arg (=1000000)
413              Only use components in case the number  of  variables  is  below
414              this limit
415
416       --compslimit arg (=500)
417              Limit how much time is spent in component-finding
418
419   Memory saving options:
420       --renumber arg (=1)
421              Renumber variables to increase CPU cache efficiency
422
423       --savemem arg (=1)
424              Save  memory  by  deallocating variable space after renumbering.
425              Only works if renumbering is active.
426
427       --mustrenumber arg (=0)
428              Treat all 'renumber' strategies as 'must-renumber'
429
430       --fullwatchconseveryn arg (=4000000)
431              Consolidate watchlists fully once every N  conflicts.  Scheduled
432              during simplification rounds.
433
434   XOR-related options:
435       --xor arg (=1)
436              Discover long XORs
437
438       --maxxorsize arg (=7)
439              Maximum XOR size to find
440
441       --xorfindtout arg (=400)
442              Time limit for finding XORs
443
444       --varsperxorcut arg (=2)
445              Number  of _real_ variables per XOR when cutting them. So 2 will
446              have XORs of size 4 because 1 = connecting to previous, 1 = con‐
447              necting  to  next, 2 in the midde. If the XOR is 4 long, it will
448              be just one 4-long XOR, no connectors
449
450       --maxxormat arg (=400)
451              Maximum matrix size (=num elements) that we should try to echel‐
452              onize
453
454       --forcepreservexors arg (=0)
455              Force  preserving XORs when they have been found. Easier to make
456              sure XORs are not lost through simplifiactions such as strenght‐
457              ening
458
459       --m4ri arg (=1)
460              Use M4RI
461
462   Gate-related options:
463       --gates arg (=0)
464              Find gates. Disables all sub-options below
465
466       --gorshort arg (=1)
467              Shorten clauses with OR gates
468
469       --gandrem arg (=1)
470              Remove clauses with AND gates
471
472       --gateeqlit arg (=1)
473              Find equivalent literals using gates
474
475       --printgatedot arg (=0)
476              Print gate structure regularly to file 'gatesX.dot'
477
478       --gatefindto arg (=200)
479              Max time in bogoprops M to find gates
480
481       --shortwithgatesto arg (=200)
482              Max time to shorten with gates, bogoprops M
483
484       --remwithgatesto arg (=100)
485              Max time to remove with gates, bogoprops M
486
487   Gauss options:
488       --maxmatrixrows arg (=5000)
489              Set  maximum  no.  of rows for gaussian matrix. Too large matri‐
490              cesshould bee discarded for reasons of efficiency
491
492       --autodisablegauss arg (=1)
493              Automatically disable gauss when performing badly
494
495       --minmatrixrows arg (=3)
496              Set minimum no. of rows for gaussian matrix. Normally, too small
497              matrices are discarded for reasons of efficiency
498
499       --maxnummatrices arg (=5)
500              Maximum number of matrices to treat.
501
502       --detachxor arg (=0)
503              Detach and reattach XORs
504
505       --useallmatrixes arg (=0)
506              Force using all matrices
507
508       --detachverb arg (=0)
509              If  set, verbosity for XOR detach code is upped, ignoring normal
510              verbosity
511
512       --gaussusefulcutoff arg (=0.20000000000000001)
513              Turn off Gauss if  less  than  this  many  usefulenss  ratio  is
514              recorded
515
516   Distill options:
517       --distill arg (=1)
518              Regularly execute clause distillation
519
520       --distillmaxm arg (=20)
521              Maximum  number  of  Mega-bogoprops(~time)  to  spend on vivify‐
522              ing/distilling long cls by enqueueing and propagating
523
524       --distillto arg (=120)
525              Maximum time in bogoprops M for distillation
526
527       --distillincconf arg (=0.02)
528              Multiplier for current number of conflicts OTF distill
529
530       --distillminconf arg (=10000)
531              Minimum number of conflicts between OTF distill
532
533       --distilltier1ratio arg (=0.029999999999999999)
534              How much of tier 1 to distill
535
536   Reconf options:
537       --reconfat arg (=2)
538              Reconfigure after this many simplifications
539
540       --reconf arg (=0)
541              Reconfigure  after  some  time  to  this  solver   configuration
542              [3,4,6,7,12,13,14,15,16]
543
544   Misc options:
545       --strmaxt arg (=30)
546              Maximum  MBP  to  spend  on  distilling  long  irred cls through
547              watches
548
549       --implicitmanip arg (=1)
550              Subsume and strengthen implicit clauses with each other
551
552       --implsubsto arg (=100)
553              Timeout (in bogoprop Millions) of implicit subsumption
554
555       --implstrto arg (=200)
556              Timeout (in bogoprop Millions) of implicit strengthening
557
558       --cardfind arg (=0)
559              Find cardinality constraints
560
561   Normal run schedules:
562              Default      schedule:       handle-comps,scc-vrepl,sub-impl,in‐
563              tree-probe,sub-str-cls-with-bin,dis‐
564              till-cls,scc-vrepl,sub-impl,str-impl,sub-impl,breakid,occ-backw-sub-str,occ-clean-im‐
565              plicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,card-find,cl-con‐
566              solidate,str-impl,sub-str-cls-with-bin,dis‐
567              till-cls,scc-vrepl,renumber,bosphorus,sls,lucky
568
569              Schedule   at   startup:   sub-impl,breakid,  occ-backw-sub-str,
570              occ-clean-implicit, occ-bve,occ-ternary-res,  occ-backw-sub-str,
571              occ-xor,                                   card-find,cl-consoli‐
572              date,scc-vrepl,sub-cls-with-bin,bosphorus,sls,lucky
573
574   Preproc run schedule:
575              handle-comps,scc-vrepl,sub-impl,sub-str-cls-with-bin,       dis‐
576              till-cls,    scc-vrepl,   sub-impl,breakid,   occ-backw-sub-str,
577              occ-clean-implicit,      occ-bve,       occ-bva,occ-ternary-res,
578              occ-xor,cl-consolidate,str-impl,    sub-str-cls-with-bin,   dis‐
579              till-cls,      scc-vrepl,      sub-impl,str-impl,      sub-impl,
580              sub-str-cls-with-bin,intree-probe, must-renumber
581

BUG TRACKER

583       Please don't hesitate to file any and all issues at:
584
585       https://github.com/msoos/cryptominisat/issues
586

AUTHORS

588       cryptominisat5    is    written    and    maintained   by   Mate   Soos
589       soos.mate@gmail.com
590
592       cryptominisat5 is under  the  MIT  license.  Please  see  https://open
593       source.org/licenses/MIT for the full text
594

SEE ALSO

596       More  documentation  for  the cryptominisat5 SAT solver can be found at
597       https://www.msoos.org/cryptominisat5/
598
599
600
601cryptominisat5 5.8.0             January 2022                CRYPTOMINISAT5(1)
Impressum