1CRYPTOMINISAT5(1) User Commands CRYPTOMINISAT5(1)
2
6 cryptominisat5 - SAT solver
7
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 cryptominisat5 [options] inputfile [drat-trim-file]
13 Preprocessor usage:
15 cryptominisat5 --preproc 1 [options] inputfile simpli‐
16 fied-cnf-file
17 cryptominisat5 --preproc 2 [options] solution-file
19 Main options:
21 -h [ --help ]
22 Print simple help
23 --hhelp
25 Print extensive help
26 -v [ --version ]
28 Print version info
29 --verb arg (=1)
31 [0-10] Verbosity of solver. 0 = only solution
32 -r [ --random ] arg (=0)
34 [0..] Random seed
35 -t [ --threads ] arg (=1)
37 Number of threads
38 --maxtime arg
40 Stop solving after this much time (s)
41 --maxconfl arg
43 Stop solving after this many conflicts
44 -m [ --mult ] arg (=3)
46 Time multiplier for all simplification cutoffs
47 --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 -p [ --preproc ] arg (=0)
54 0 = normal run, 1 = preprocess and dump, 2 = read back dump and
55 solution to produce final solution
56 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 --polarstablen arg (=4)
65 When to use stable polarities. 0 = always, otherwise every n.
66 Negative is special, see code
67 --lucky arg (=20)
69 Try computing lucky polarities
70 --polarbestinvmult arg (=9)
72 How often should we use inverted best polarities instead of sta‐
73 ble
74 --polarbestmult arg (=1000)
76 How often should we use best polarities instead of stable
77 SQL options:
79 --sql arg (=0)
80 Write to SQL. 0 = no SQL, 1 or 2 = sqlite
81 --sqlitedb arg
83 Where to put the SQLite database
84 --sqlitedboverwrite arg (=0)
86 Overwrite the SQLite database file if it exists
87 --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 --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 Restart options:
99 --restart arg
100 {geom, glue, luby} Restart strategy to follow.
101 --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 --lwrbndblkrest arg (=10000)
108 Lower bound on blocking restart -- don't block before this many
109 conflicts
110 --locgmult arg (=0.8)
112 The multiplier used to determine if we should restart during
113 glue-based restart
114 --ratiogluegeom arg (=5)
116 Ratio of glue vs geometric restarts -- more is more glue
117 Printing options:
119 --verbstat arg (=2)
120 Change verbosity of statistics at the end of the solving [0..3]
121 --verbrestart arg (=0)
123 Print more thorough, but different stats
124 --verballrestarts arg (=0)
126 Print a line for every restart
127 -s [ --printsol ] arg (=1)
129 Print assignment if solution is SAT
130 --restartprint arg (=8192)
132 Print restart status lines at least every N conflicts
133 --dumpresult arg
135 Write solution(s) to this file
136 Glue options:
138 --updateglueonanalysis arg (=1)
139 Update glues while analyzing
140 --maxgluehistltlimited arg (=50)
142 Maximum glue used by glue-based restart strategy when populating
143 glue history.
144 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 Redundant clause options:
153 --gluecut0 arg (=3)
154 Glue value for lev 0 ('keep') cut
155 --gluecut1 arg (=6)
157 Glue value for lev 1 cut ('give another shot'
158 --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 --everylev1 arg (=10000)
164 Reduce lev1 clauses every N
165 --everylev2 arg (=15000)
167 Reduce lev2 clauses every N
168 --lev1usewithin arg (=70000)
170 Learnt clause must be used in lev1 within this timeframe or be
171 dropped to lev2
172 --dumpred arg
174 Dump redundant clauses of gluecut0&1 to this filename
175 --dumpredmaxlen arg (=10000)
177 When dumping redundant clauses, only dump clauses at most this
178 long
179 --dumpredmaxglue arg (=1000)
181 When dumping redundant clauses, only dump clauses with at most
182 this large glue
183 Clause dumping after problem finishing:
185 Variable branching options:
187 --branchstr arg (=maple1+maple2+vsids2+maple1+maple2+vsids1)
188 Branch strategy. E.g. 'vmtf+vsids+maple+rnd'
189 Conflict options:
191 --recur arg (=1)
192 Perform recursive minimisation
193 --moreminim arg (=1)
195 Perform strong minimisation at conflict gen.
196 --moremoreminim arg (=1)
198 Perform even stronger minimisation at conflict gen.
199 --moremorealways arg (=0)
201 Always strong-minimise clause
202 --decbased arg (=1)
204 Create decision-based conflict clauses when the UIP clause is
205 too large
206 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 --nobansol
213 Don't ban the solution once it's found
214 --debuglib arg
216 Parse special comments to run solve/simplify during parsing of
217 CNF
218 Probing options:
220 --transred arg (=1)
221 Remove useless binary clauses (transitive reduction)
222 --intree arg (=1)
224 Carry out intree-based probing
225 --intreemaxm arg (=1200)
227 Time in mega-bogoprops to perform intree probing
228 --otfhyper arg (=1)
230 Perform hyper-binary resolution during probing
231 Stochastic Local Search options:
233 --sls arg (=1)
234 Run SLS during simplification
235 --slstype arg (=ccnr)
237 Which SLS to run. Allowed values: walksat, yalsat, ccnr,
238 ccnr_yalsat
239 --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 --slseveryn arg (=2)
245 Run SLS solver every N simplifications only
246 --yalsatmems arg (=40)
248 Run Yalsat with this many mems*million timeout. Limits time of
249 yalsat run
250 --walksatruns arg (=50)
252 Max 'runs' for WalkSAT. Limits time of WalkSAT run
253 --slsgetphase arg (=1)
255 Get phase from SLS solver, set as new phase for CDCL
256 --slsccnraspire arg (=1)
258 Turn aspiration on/off for CCANR
259 --slstobump arg (=100)
261 How many variables to bump in CCNR
262 --slstobumpmaxpervar arg (=100)
264 How many times to bump an individual variable's activity in CCNR
265 --slsbumptype arg (=6)
267 How to calculate what variable to bump. 1 = clause-based, 2 =
268 var-flip-based, 3 = var-score-based
269 --slsoffset arg (=0)
271 Should SLS set the VSIDS/Maple offsetsd
272 Simplification schedules:
274 --schedsimp arg (=1)
275 Perform simplification rounds. If 0, we never perform any.
276 --presimp arg (=0)
278 Perform simplification at the very start
279 --allpresimp arg (=0)
281 Perform simplification at EVERY start -- only matters in library
282 mode
283 -n [ --nonstop ] arg (=0)
285 Never stop the search() process in class SATSolver
286 --maxnumsimppersolve arg (=25)
288 Maximum number of simplifiactions to perform for every solve()
289 call. After this, no more inprocessing will take place.
290 --schedule arg
292 Schedule for simplification during run
293 --preschedule arg
295 Schedule for simplification at startup
296 --occsimp arg (=1)
298 Perform occurrence-list-based optimisations (variable elimina‐
299 tion, subsumption, bounded variable addition...)
300 --confbtwsimp arg (=50000)
302 Start first simplification after this many conflicts
303 --confbtwsimpinc arg (=1.4)
305 Simp rounds increment by this power of N
306 Occ-based simplification memory limits:
308 --occredmax arg (=200)
309 Don't add to occur list any redundant clause larger than this
310 --occredmaxmb arg (=600)
312 Don't allow redundant occur size to be beyond this many MB
313 --occirredmaxmb arg (=2500)
315 Don't allow irredundant occur size to be beyond this many MB
316 Ternary resolution:
318 --tern arg (=1)
319 Perform Ternary resolution'
320 --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 --ternkeep arg (=6)
326 Keep ternary resolution clauses only if they are touched within
327 this multiple of 'lev1usewithin'
328 --terncreate arg (=1)
330 Create only this multiple (of linked in cls) ternary resolution
331 clauses per simp run
332 --ternbincreate arg (=1)
334 Allow ternary resolving to generate binary clauses
335 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 --substimelim arg (=300)
342 Time-out in bogoprops M of subsumption of long clauses with long
343 clauses, after computing occur
344 --substimelimbinratio arg (=0.10000000000000001)
346 Ratio of subsumption time limit to spend on sub&str long clauses
347 with bin
348 --substimelimlongratio arg (=0.90000000000000002)
350 Ratio of subsumption time limit to spend on sub long clauses
351 with long
352 --strstimelim arg (=300)
354 Time-out in bogoprops M of strengthening of long clauses with
355 long clauses, after computing occur
356 --sublonggothrough arg (=1)
358 How many times go through subsume
359 BVE options:
361 --varelim arg (=1)
362 Perform variable elimination as per Een and Biere
363 --varelimto arg (=750)
365 Var elimination bogoprops M time limit
366 --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 --emptyelim arg (=1)
372 Perform empty resolvent elimination using bit-map trick
373 --varelimmaxmb arg (=1000)
375 Maximum extra MB of memory to use for new clauses during varelim
376 --eratio arg (=1.6)
378 Eliminate this ratio of free variables at most per variable
379 elimination iteration
380 --skipresol arg (=1)
382 Skip BVE resolvents in case they belong to a gate
383 BVA options:
385 --bva arg (=1)
386 Perform bounded variable addition
387 --bvaeveryn arg (=7)
389 Perform BVA only every N occ-simplify calls
390 --bvalim arg (=250000)
392 Maximum number of variables to add by BVA per call
393 --bva2lit arg (=1)
395 BVA with 2-lit difference hack, too. Beware, this reduces the
396 effectiveness of 1-lit diff
397 --bvato arg (=50)
399 BVA time limit in bogoprops M
400 Equivalent literal options:
402 --scc arg (=1)
403 Find equivalent literals through SCC and replace them
404 Component options:
406 --comps arg (=0)
407 Perform component-finding and separate handling
408 --compsfrom arg (=0)
410 Component finding only after this many simplification rounds
411 --compsvar arg (=1000000)
413 Only use components in case the number of variables is below
414 this limit
415 --compslimit arg (=500)
417 Limit how much time is spent in component-finding
418 Memory saving options:
420 --renumber arg (=1)
421 Renumber variables to increase CPU cache efficiency
422 --savemem arg (=1)
424 Save memory by deallocating variable space after renumbering.
425 Only works if renumbering is active.
426 --mustrenumber arg (=0)
428 Treat all 'renumber' strategies as 'must-renumber'
429 --fullwatchconseveryn arg (=4000000)
431 Consolidate watchlists fully once every N conflicts. Scheduled
432 during simplification rounds.
433 XOR-related options:
435 --xor arg (=1)
436 Discover long XORs
437 --maxxorsize arg (=7)
439 Maximum XOR size to find
440 --xorfindtout arg (=400)
442 Time limit for finding XORs
443 --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 --maxxormat arg (=400)
451 Maximum matrix size (=num elements) that we should try to echel‐
452 onize
453 --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 --m4ri arg (=1)
460 Use M4RI
461 Gate-related options:
463 --gates arg (=0)
464 Find gates. Disables all sub-options below
465 --gorshort arg (=1)
467 Shorten clauses with OR gates
468 --gandrem arg (=1)
470 Remove clauses with AND gates
471 --gateeqlit arg (=1)
473 Find equivalent literals using gates
474 --printgatedot arg (=0)
476 Print gate structure regularly to file 'gatesX.dot'
477 --gatefindto arg (=200)
479 Max time in bogoprops M to find gates
480 --shortwithgatesto arg (=200)
482 Max time to shorten with gates, bogoprops M
483 --remwithgatesto arg (=100)
485 Max time to remove with gates, bogoprops M
486 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 --autodisablegauss arg (=1)
493 Automatically disable gauss when performing badly
494 --minmatrixrows arg (=3)
496 Set minimum no. of rows for gaussian matrix. Normally, too small
497 matrices are discarded for reasons of efficiency
498 --maxnummatrices arg (=5)
500 Maximum number of matrices to treat.
501 --detachxor arg (=0)
503 Detach and reattach XORs
504 --useallmatrixes arg (=0)
506 Force using all matrices
507 --detachverb arg (=0)
509 If set, verbosity for XOR detach code is upped, ignoring normal
510 verbosity
511 --gaussusefulcutoff arg (=0.20000000000000001)
513 Turn off Gauss if less than this many usefulenss ratio is
514 recorded
515 Distill options:
517 --distill arg (=1)
518 Regularly execute clause distillation
519 --distillmaxm arg (=20)
521 Maximum number of Mega-bogoprops(~time) to spend on vivify‐
522 ing/distilling long cls by enqueueing and propagating
523 --distillto arg (=120)
525 Maximum time in bogoprops M for distillation
526 --distillincconf arg (=0.02)
528 Multiplier for current number of conflicts OTF distill
529 --distillminconf arg (=10000)
531 Minimum number of conflicts between OTF distill
532 --distilltier1ratio arg (=0.029999999999999999)
534 How much of tier 1 to distill
535 Reconf options:
537 --reconfat arg (=2)
538 Reconfigure after this many simplifications
539 --reconf arg (=0)
541 Reconfigure after some time to this solver configuration
542 [3,4,6,7,12,13,14,15,16]
543 Misc options:
545 --strmaxt arg (=30)
546 Maximum MBP to spend on distilling long irred cls through
547 watches
548 --implicitmanip arg (=1)
550 Subsume and strengthen implicit clauses with each other
551 --implsubsto arg (=100)
553 Timeout (in bogoprop Millions) of implicit subsumption
554 --implstrto arg (=200)
556 Timeout (in bogoprop Millions) of implicit strengthening
557 --cardfind arg (=0)
559 Find cardinality constraints
560 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 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 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
583 Please don't hesitate to file any and all issues at:
584 https://github.com/msoos/cryptominisat/issues
586
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
596 More documentation for the cryptominisat5 SAT solver can be found at
597 https://www.msoos.org/cryptominisat5/
598cryptominisat5 5.8.0 January 2022 CRYPTOMINISAT5(1)