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 (=MAX)
40 Stop solving after this much time (s)
41 --maxconfl arg (=MAX)
43 Stop solving after this many conflicts
44 -m [ --mult ] arg (=4)
46 Time multiplier for all simplification cutoffs
47 --memoutmult arg (=1)
49 Multiplier for memory-out checks on variables and
50 clause-link-in, etc. Useful when you have limited memory.
51 -p [ --preproc ] arg (=0)
53 0 = normal run, 1 = preprocess and dump, 2 = read back dump and
54 solution to produce final solution
55 --polar arg (=auto)
57 {true,false,rnd,auto} Selects polarity mode. 'true' -> selects
58 only positive polarity when branching. 'false' -> selects only
59 negative polarity when branching. 'auto' -> selects last polar‐
60 ity used (also called 'caching')
61 Restart options:
63 --restart arg
64 {geom, glue, luby} Restart strategy to follow.
65 --gluehist arg (=50)
67 The size of the moving window for short-term glue history of
68 redundant clauses. If higher, the minimal number of conflicts
69 between restarts is longer
70 --blkrest arg (=1)
72 Perform blocking restarts as per Glucose 3.0
73 --blkrestlen arg (=5000)
75 Length of the long term trail size for blocking restart
76 --blkrestmultip arg (=1.4)
78 Multiplier used for blocking restart cut-off (called 'R' in Glu‐
79 cose 3.0)
80 --lwrbndblkrest arg (=10000)
82 Lower bound on blocking restart -- don't block before this many
83 conflicts
84 --locgmult arg (=0.80000000000000004) The multiplier used to determine
86 if we
87 should restart during glue-based restart
88 --brokengluerest arg (=1)
90 Should glue restart be broken as before 8e74cb5010bb4
91 --ratiogluegeom arg (=5)
93 Ratio of glue vs geometric restarts -- more is more glue
94 Printing options:
96 --verbstat arg (=1)
97 Change verbosity of statistics at the end of the solving [0..2]
98 --verbrestart arg (=0)
100 Print more thorough, but different stats
101 --verballrestarts arg (=0)
103 Print a line for every restart
104 -s [ --printsol ] arg (=1)
106 Print assignment if solution is SAT
107 --restartprint arg (=8192)
109 Print restart status lines at least every N conflicts
110 Propagation options:
112 --updateglueonanalysis arg (=1)
113 Update glues while analyzing
114 --otfhyper arg (=1)
116 Perform hyper-binary resolution at dec. level 1 after every
117 restart and during probing
118 Redundant clause options:
120 --gluecut0 arg (=3)
121 Glue value for lev 0 ('keep') cut
122 --gluecut1 arg (=6)
124 Glue value for lev 1 cut ('give another shot'
125 --adjustglue arg (=0.7)
127 If more than this % of clauses is LOW glue (level 0) then lower
128 the glue cutoff by 1 -- once and never again
129 --everylev1 arg (=10000)
131 Reduce lev1 clauses every N
132 --everylev2 arg (=15000)
134 Reduce lev2 clauses every N
135 --lev1usewithin arg (=30000)
137 Learnt clause must be used in lev1 within this timeframe or be
138 dropped to lev2
139 --dumpred arg
141 Dump redundant clauses of gluecut0&1 to this filename
142 --dumpredmaxlen arg (=10000)
144 When dumping redundant clauses, only dump clauses at most this
145 long
146 --dumpredmaxglue arg (=1000)
148 When dumping redundant clauses, only dump clauses with at most
149 this large glue
150 Clause dumping after problem finishing:
152 Variable branching options:
154 --vardecaystart arg (=0.8)
155 variable activity increase divider (MUST be smaller than multi‐
156 plier)
157 --vardecaymax arg (=0.95)
159 variable activity increase divider (MUST be smaller than multi‐
160 plier)
161 --vincstart arg (=1)
163 variable activity increase starts with this value. Make sure
164 that this multiplied by multiplier and divided by divider is
165 larger than itself
166 --freq arg (=0)
168 [0 - 1] freq. of picking var at random
169 --maple arg (=1)
171 Use maple-type variable picking sometimes
172 --maplemod arg (=3)
174 Use maple N-1 of N rounds. Normally, N is 2, so used every other
175 round. Set to 3 so it will use maple 2/3rds of the time.
176 --maplemorebump arg (=0)
178 Bump variable usefulness more when glue is HIGH
179 Conflict options:
181 --recur arg (=1)
182 Perform recursive minimisation
183 --moreminim arg (=1)
185 Perform strong minimisation at conflict gen.
186 --moremoreminim arg (=0)
188 Perform even stronger minimisation at conflict gen.
189 --moremorecachelimit arg (=400)
191 Time-out in microsteps for each more minimisation with cache.
192 Only active if 'moreminim' is on
193 --moremorestamp arg (=0)
195 Use cache for otf more minim of learnt clauses
196 --moremorealways arg (=0)
198 Always strong-minimise clause
199 --otfsubsume arg (=0)
201 Perform on-the-fly subsumption
202 --decbased arg (=1)
204 Create decision-based conflict clauses when the UIP clause is
205 too large
206 --decbasemaxlev arg (=9)
208 Create decision-based conflict if the maximum level is below or
209 equal to this
210 --decbaseminsz arg (=50)
212 Create decision-based conflict if the learnt clause is larger
213 than this
214 Iterative solve options:
216 --maxsol arg (=1)
217 Search for given amount of solutions. Thanks to Jannis Harder
218 for the decision-based banning idea
219 --debuglib arg
221 MainSolver at specific 'solve()' points in CNF file
222 --dumpresult arg
224 Write solution(s) to this file
225 Probing options:
227 --bothprop arg (=1)
228 Do propagations solely to propagate the same value twice
229 --probe arg (=0)
231 Carry out probing
232 --probemaxm arg (=800)
234 Time in mega-bogoprops to perform probing
235 --transred arg (=1)
237 Remove useless binary clauses (transitive reduction)
238 --intree arg (=1)
240 Carry out intree-based probing
241 --intreemaxm arg (=1200)
243 Time in mega-bogoprops to perform intree probing
244 Stamping options:
246 --stamp arg (=0)
247 Use time stamping as per Heule&Jarvisalo&Biere paper
248 --cache arg (=0)
250 Use implication cache -- may use a lot of memory
251 --cachesize arg (=2048)
253 Maximum size of the implication cache in MB. It may temporarily
254 reach higher usage, but will be deleted&disabled if this limit
255 is reached.
256 --cachecutoff arg (=2000)
258 If the number of literals propagated by a literal is more than
259 this, it's not included into the implication cache
260 Simplification schedules:
262 --schedsimp arg (=1)
263 Perform simplification rounds. If 0, we never perform any.
264 --presimp arg (=0)
266 Perform simplification at the very start
267 --allpresimp arg (=0)
269 Perform simplification at EVERY start -- only matters in library
270 mode
271 -n [ --nonstop ] arg (=0)
273 Never stop the search() process in class SATSolver
274 --schedule arg
276 Schedule for simplification during run
277 --preschedule arg
279 Schedule for simplification at startup
280 --occsimp arg (=1)
282 Perform occurrence-list-based optimisations (variable elimina‐
283 tion, subsumption, bounded variable addition...)
284 --confbtwsimp arg (=50000)
286 Start first simplification after this many conflicts
287 --confbtwsimpinc arg (=1.3999999999999999)
289 Simp rounds increment by this power of N
290 Occ-based simplification memory limits:
292 --occredmax arg (=200)
293 Don't add to occur list any redundant clause larger than this
294 --occredmaxmb arg (=600)
296 Don't allow redundant occur size to be beyond this many MB
297 --occirredmaxmb arg (=2500)
299 Don't allow irredundant occur size to be beyond this many MB
300 Ternary resolution:
302 --tern arg (=0)
303 Perform Ternary resolution'
304 --terntimelim arg (=100)
306 Time-out in bogoprops M of ternary resolution as per paper
307 'Look-Ahead Versus Look-Back for Satisfiability Problems'
308 Occ-based subsumption and strengthening time limits:
310 --strengthen arg (=1)
311 Perform clause contraction through self-subsuming resolution as
312 part of the occurrence-subsumption system
313 --substimelim arg (=300)
315 Time-out in bogoprops M of subsumption of long clauses with long
316 clauses, after computing occur
317 --strstimelim arg (=300)
319 Time-out in bogoprops M of strengthening of long clauses with
320 long clauses, after computing occur
321 BVE options:
323 --varelim arg (=1)
324 Perform variable elimination as per Een and Biere
325 --varelimto arg (=350)
327 Var elimination bogoprops M time limit
328 --varelimover arg (=32)
330 Do BVE until the resulting no. of clause increase is less than
331 X. Only power of 2 makes sense, i.e. 2,4,8...
332 --emptyelim arg (=1)
334 Perform empty resolvent elimination using bit-map trick
335 --varelimmaxmb arg (=1000)
337 Maximum extra MB of memory to use for new clauses during varelim
338 --eratio arg (=norm: 1.6 preproc: 1)
340 Eliminate this ratio of free variables at most per variable
341 elimination iteration
342 --skipresol arg (=1)
344 Skip BVE resolvents in case they belong to a gate
345 --agrelimtimelim arg (=300)
347 Time-out in bogoprops M of aggressive(=uses reverse distilla‐
348 tion) var-elimination
349 BVA options:
351 --bva arg (=0)
352 Perform bounded variable addition
353 --bvalim arg (=150000)
355 Maximum number of variables to add by BVA per call
356 --bva2lit arg (=1)
358 BVA with 2-lit difference hack, too. Beware, this reduces the
359 effectiveness of 1-lit diff
360 --bvato arg (=100)
362 BVA time limit in bogoprops M
363 Equivalent literal options:
365 --scc arg (=1)
366 Find equivalent literals through SCC and replace them
367 --extscc arg (=1)
369 Perform SCC using cache
370 Component options:
372 --comps arg (=0)
373 Perform component-finding and separate handling
374 --compsfrom arg (=0)
376 Component finding only after this many simplification rounds
377 --compsvar arg (=1000000)
379 Only use components in case the number of variables is below
380 this limit
381 --compslimit arg (=500)
383 Limit how much time is spent in component-finding
384 XOR-related options:
386 --xor arg (=1)
387 Discover long XORs
388 --maxxorsize arg (=7)
390 Maximum XOR size to find
391 --xorcache arg (=0)
393 Use cache when finding XORs. Finds a LOT more XORs, but takes a
394 lot more time
395 --varsperxorcut arg (=2)
397 Number of _real_ variables per XOR when cutting them. So 2 will
398 have XORs of size 4 because 1 = connecting to previous, 1 = con‐
399 necting to next, 2 in the midde. If the XOR is 4 long, it will
400 be just one 4-long XOR, no connectors
401 --maxxormat arg (=400)
403 Maximum matrix size (=num elements) that we should try to echel‐
404 onize
405 Gate-related options:
407 --gates arg (=0)
408 Find gates. Disables all sub-options below
409 --gorshort arg (=1)
411 Shorten clauses with OR gates
412 --gandrem arg (=1)
414 Remove clauses with AND gates
415 --gateeqlit arg (=1)
417 Find equivalent literals using gates
418 --printgatedot arg (=0)
420 Print gate structure regularly to file 'gatesX.dot'
421 --gatefindto arg (=200)
423 Max time in bogoprops M to find gates
424 --shortwithgatesto arg (=200)
426 Max time to shorten with gates, bogoprops M
427 --remwithgatesto arg (=100)
429 Max time to remove with gates, bogoprops M
430 Misc options:
432 --distill arg (=1)
433 Regularly execute clause distillation
434 --distillmaxm arg (=20)
436 Maximum number of Mega-bogoprops(~time) to spend on vivify‐
437 ing/distilling long cls by enqueueing and propagating
438 --distillto arg (=120)
440 Maximum time in bogoprops M for distillation
441 Reconf options:
443 --reconfat arg (=2)
444 Reconfigure after this many simplifications
445 --reconf arg (=0)
447 Reconfigure after some time to this solver configuration [0..15]
448 Misc options:
450 --strcachemaxm arg (=30)
451 Maximum number of Mega-bogoprops(~time) to spend on vivifying
452 long irred cls through watches, cache and stamps
453 --renumber arg (=1)
455 Renumber variables to increase CPU cache efficiency
456 --savemem arg (=1)
458 Save memory by deallocating variable space after renumbering.
459 Only works if renumbering is active.
460 --fullwatchconseveryn arg (=4000000)
462 Consolidate watchlists fully once every N conflicts. Scheduled
463 during simplification rounds.
464 --implicitmanip arg (=1)
466 Subsume and strengthen implicit clauses with each other
467 --implsubsto arg (=100)
469 Timeout (in bogoprop Millions) of implicit subsumption
470 --implstrto arg (=200)
472 Timeout (in bogoprop Millions) of implicit strengthening
473 Normal run schedules:
475 Default schedule: handle-comps,scc-vrepl, cache-clean,
476 cache-tryboth,sub-impl, intree-probe,
477 probe,sub-str-cls-with-bin, distill-cls,scc-vrepl, sub-impl,
478 str-impl, sub-impl,occ-backw-sub-str, occ-clean-implicit,
479 occ-bve, occ-bva,occ-ternary-res, occ-xor,cl-consoli‐
480 date,str-impl, cache-clean, sub-str-cls-with-bin, dis‐
481 till-cls,scc-vrepl, check-cache-size, renumber
482 Schedule at startup: sub-impl,occ-backw-sub-str,
484 occ-clean-implicit, occ-bve,occ-ternary-res, occ-backw-sub-str,
485 occ-xor, cl-consolidate,scc-vrepl,sub-cls-with-bin
486 Preproc run schedule:
488 handle-comps,scc-vrepl, cache-clean, cache-try‐
489 both,sub-impl,sub-str-cls-with-bin, distill-cls, scc-vrepl,
490 sub-impl,occ-backw-sub-str, occ-clean-implicit, occ-bve,
491 occ-bva,occ-ternary-res, occ-xor,cl-consolidate,str-impl,
492 cache-clean, sub-str-cls-with-bin, distill-cls, scc-vrepl,
493 sub-impl,str-impl, sub-impl, sub-str-cls-with-bin,intree-probe,
494 probe,must-renumber
495
497 Please don't hesitate to file any and all issues at:
498 https://github.com/msoos/cryptominisat/issues
500
502 cryptominisat5 is written and maintained by Mate Soos
503 soos.mate@gmail.com
504
506 cryptominisat5 is under the MIT license. Please see https://open‐
507 source.org/licenses/MIT for the full text
508
510 More documentation for the cryptominisat5 SAT solver can be found at
511 https://www.msoos.org/cryptominisat5/
512cryptominisat5 5.6.8 February 2019 CRYPTOMINISAT5(1)