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 (=4096)
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 --ml arg (=0)
131 Use ML model to guess clause effectiveness
132 --everylev1 arg (=10000)
134 Reduce lev1 clauses every N
135 --everylev2 arg (=15000)
137 Reduce lev2 clauses every N
138 --lev1usewithin arg (=30000)
140 Learnt clause must be used in lev1 within this timeframe or be
141 dropped to lev2
142 --dumpred arg
144 Dump redundant clauses of gluecut0&1 to this filename
145 --dumpredmaxlen arg (=10000)
147 When dumping redundant clauses, only dump clauses at most this
148 long
149 --dumpredmaxglue arg (=1000)
151 When dumping redundant clauses, only dump clauses with at most
152 this large glue
153 Variable branching options:
155 --vardecaystart arg (=0.8)
156 variable activity increase divider (MUST be smaller than multi‐
157 plier)
158 --vardecaymax arg (=0.95)
160 variable activity increase divider (MUST be smaller than multi‐
161 plier)
162 --vincstart arg (=1)
164 variable activity increase stars with this value. Make sure that
165 this multiplied by multiplier and divided by divider is larger
166 than itself
167 --freq arg (=0)
169 [0 - 1] freq. of picking var at random
170 --maple arg (=1)
172 Use maple-type variable picking sometimes
173 --maplemod arg (=3)
175 Use maple N-1 of N rounds. Normally, N is 2, so used every other
176 round. Set to 3 so it will use maple 2/3rds of the time.
177 --maplemorebump arg (=0)
179 Bump variable usefulness more when glue is HIGH
180 Conflict options:
182 --recur arg (=1)
183 Perform recursive minimisation
184 --moreminim arg (=1)
186 Perform strong minimisation at conflict gen.
187 --moremoreminim arg (=0)
189 Perform even stronger minimisation at conflict gen.
190 --moremorecachelimit arg (=400)
192 Time-out in microsteps for each more minimisation with cache.
193 Only active if 'moreminim' is on
194 --moremorestamp arg (=0)
196 Use cache for otf more minim of learnt clauses
197 --moremorealways arg (=0)
199 Always strong-minimise clause
200 --otfsubsume arg (=0)
202 Perform on-the-fly subsumption
203 Iterative solve options:
205 --maxsol arg (=1)
206 Search for given amount of solutions
207 --debuglib arg
209 MainSolver at specific 'solve()' points in CNF file
210 --dumpresult arg
212 Write solution(s) to this file
213 Probing options:
215 --bothprop arg (=1)
216 Do propagations solely to propagate the same value twice
217 --probe arg (=0)
219 Carry out probing
220 --probemaxm arg (=800)
222 Time in mega-bogoprops to perform probing
223 --transred arg (=1)
225 Remove useless binary clauses (transitive reduction)
226 --intree arg (=1)
228 Carry out intree-based probing
229 --intreemaxm arg (=1200)
231 Time in mega-bogoprops to perform intree probing
232 Stamping options:
234 --stamp arg (=0)
235 Use time stamping as per Heule&Jarvisalo&Biere paper
236 --cache arg (=0)
238 Use implication cache -- may use a lot of memory
239 --cachesize arg (=2048)
241 Maximum size of the implication cache in MB. It may temporarily
242 reach higher usage, but will be deleted&disabled if this limit
243 is reached.
244 --cachecutoff arg (=2000)
246 If the number of literals propagated by a literal is more than
247 this, it's not included into the implication cache
248 Simplification options:
250 --schedsimp arg (=1)
251 Perform simplification rounds. If 0, we never perform any.
252 --presimp arg (=0)
254 Perform simplification at the very start
255 --allpresimp arg (=0)
257 Perform simplification at EVERY start -- only matters in library
258 mode
259 -n [ --nonstop ] arg (=0)
261 Never stop the search() process in class SATSolver
262 --schedule arg
264 Schedule for simplification during run
265 --preschedule arg
267 Schedule for simplification at startup
268 --occsimp arg (=1)
270 Perform occurrence-list-based optimisations (variable elimina‐
271 tion, subsumption, bounded variable addition...)
272 --confbtwsimp arg (=50000)
274 Start first simplification after this many conflicts
275 --confbtwsimpinc arg (=1.3999999999999999)
277 Simp rounds increment by this power of N
278 --varelim arg (=1)
280 Perform variable elimination as per Een and Biere
281 --varelimto arg (=350)
283 Var elimination bogoprops M time limit
284 --varelimover arg (=32)
286 Do BVE until the resulting no. of clause increase is less than
287 X. Only power of 2 makes sense, i.e. 2,4,8...
288 --emptyelim arg (=1)
290 Perform empty resolvent elimination using bit-map trick
291 --strengthen arg (=1)
293 Perform clause contraction through self-subsuming resolution as
294 part of the occurrence-subsumption system
295 --bva arg (=0)
297 Perform bounded variable addition
298 --bvalim arg (=150000)
300 Maximum number of variables to add by BVA per call
301 --bva2lit arg (=1)
303 BVA with 2-lit difference hack, too. Beware, this reduces the
304 effectiveness of 1-lit diff
305 --bvato arg (=100)
307 BVA time limit in bogoprops M
308 --eratio arg (=norm: 1.6 preproc: 1)
310 Eliminate this ratio of free variables at most per variable
311 elimination iteration
312 --skipresol arg (=1)
314 Skip BVE resolvents in case they belong to a gate
315 --occredmax arg (=200)
317 Don't add to occur list any redundant clause larger than this
318 --occirredmaxmb arg (=2500)
320 Don't allow irredundant occur size to be beyond this many MB
321 --occredmaxmb arg (=600)
323 Don't allow redundant occur size to be beyond this many MB
324 --substimelim arg (=300)
326 Time-out in bogoprops M of subsumption of long clauses with long
327 clauses, after computing occur
328 --strstimelim arg (=300)
330 Time-out in bogoprops M of strengthening of long clauses with
331 long clauses, after computing occur
332 --agrelimtimelim arg (=300)
334 Time-out in bogoprops M of aggressive(=uses reverse distilla‐
335 tion) var-elimination
336 Equivalent literal options:
338 --scc arg (=1)
339 Find equivalent literals through SCC and replace them
340 --extscc arg (=1)
342 Perform SCC using cache
343 Component options:
345 --comps arg (=0)
346 Perform component-finding and separate handling
347 --compsfrom arg (=0)
349 Component finding only after this many simplification rounds
350 --compsvar arg (=1000000)
352 Only use components in case the number of variables is below
353 this limit
354 --compslimit arg (=500)
356 Limit how much time is spent in component-finding
357 XOR-related options:
359 --xor arg (=1)
360 Discover long XORs
361 --xorcache arg (=0)
363 Use cache when finding XORs. Finds a LOT more XORs, but takes a
364 lot more time
365 --varsperxorcut arg (=2)
367 Number of _real_ variables per XOR when cutting them. So 2 will
368 have XORs of size 4 because 1 = connecting to previous, 1 = con‐
369 necting to next, 2 in the midde. If the XOR is 4 long, it will
370 be just one 4-long XOR, no connectors
371 --echelonxor arg (=1)
373 Extract data from XORs through echelonization (TOP LEVEL ONLY)
374 --maxxormat arg (=400)
376 Maximum matrix size (=num elements) that we should try to echel‐
377 onize
378 Gate-related options:
380 --gates arg (=0)
381 Find gates. Disables all sub-options below
382 --gorshort arg (=1)
384 Shorten clauses with OR gates
385 --gandrem arg (=1)
387 Remove clauses with AND gates
388 --gateeqlit arg (=1)
390 Find equivalent literals using gates
391 --printgatedot arg (=0)
393 Print gate structure regularly to file 'gatesX.dot'
394 --gatefindto arg (=200)
396 Max time in bogoprops M to find gates
397 --shortwithgatesto arg (=200)
399 Max time to shorten with gates, bogoprops M
400 --remwithgatesto arg (=100)
402 Max time to remove with gates, bogoprops M
403 Misc options:
405 --distill arg (=1)
406 Regularly execute clause distillation
407 --distillmaxm arg (=20)
409 Maximum number of Mega-bogoprops(~time) to spend on vivify‐
410 ing/distilling long cls by enqueueing and propagating
411 --distillto arg (=120)
413 Maximum time in bogoprops M for distillation
414 Reconf options:
416 --reconfat arg (=2)
417 Reconfigure after this many simplifications
418 --reconf arg (=0)
420 Reconfigure after some time to this solver configuration [0..15]
421 Misc options:
423 --strcachemaxm arg (=30)
424 Maximum number of Mega-bogoprops(~time) to spend on vivifying
425 long irred cls through watches, cache and stamps
426 --renumber arg (=1)
428 Renumber variables to increase CPU cache efficiency
429 --savemem arg (=1)
431 Save memory by deallocating variable space after renumbering.
432 Only works if renumbering is active.
433 --implicitmanip arg (=1)
435 Subsume and strengthen implicit clauses with each other
436 --implsubsto arg (=100)
438 Timeout (in bogoprop Millions) of implicit subsumption
439 --implstrto arg (=200)
441 Timeout (in bogoprop Millions) of implicit strengthening
442 Normal run schedules:
444 Default schedule: handle-comps,scc-vrepl, cache-clean,
445 cache-tryboth,sub-impl, intree-probe,
446 probe,sub-str-cls-with-bin, distill-cls,scc-vrepl, sub-impl,
447 str-impl, sub-impl,occ-backw-sub-str, occ-clean-implicit,
448 occ-bve, occ-bva, occ-xor,str-impl, cache-clean,
449 sub-str-cls-with-bin, distill-cls,scc-vrepl, check-cache-size,
450 renumber
451 Schedule at startup: sub-impl,occ-backw-sub-str,
453 occ-clean-implicit, occ-bve,occ-backw-sub-str,
454 occ-xor,scc-vrepl,sub-cls-with-bin
455 Preproc run schedule:
457 handle-comps,scc-vrepl, cache-clean, cache-try‐
458 both,sub-impl,sub-str-cls-with-bin, distill-cls, scc-vrepl,
459 sub-impl,occ-backw-sub-str, occ-xor, occ-clean-implicit,
460 occ-bve, occ-bva,str-impl, cache-clean, sub-str-cls-with-bin,
461 distill-cls, scc-vrepl, sub-impl,str-impl, sub-impl,
462 sub-str-cls-with-bin,intree-probe, probe,must-renumber
463
465 Please don't hesitate to file any and all issues at:
466 https://github.com/msoos/cryptominisat/issues
468
470 cryptominisat5 is written and maintained by Mate Soos
471 soos.mate@gmail.com
472
474 cryptominisat5 is under the MIT license. Please see https://open‐
475 source.org/licenses/MIT for the full text
476
478 More documentation for the cryptominisat5 SAT solver can be found at
479 https://www.msoos.org/cryptominisat5/
480cryptominisat5 5.6.4 August 2018 CRYPTOMINISAT5(1)