1MINISAT(1) General Commands Manual MINISAT(1)
2
6 minisat - fast and lightweight SAT solver
7
9 minisat [options] input-file result-output-file
10 minisat takes as input a plain or gzipped DIMACS formatted file. The
12 satisfiability of this input problem is indicated both via standard
13 output and the return value.
14
16 This manual page documents briefly the minisat command. MiniSat is a
17 minimalistic, open-source SAT solver, developed to help researchers and
18 developers alike to get started on SAT. Winning all the industrial cat‐
19 egories of the SAT 2005 competition, MiniSat is a good starting point
20 both for future research in SAT, and for applications using SAT.
21 Despite the NP completeness of the satisfiability problem of Boolean
23 formulas (SAT), SAT solvers are often able to decide this problem in a
24 reasonable time frame. As all other NP complete problems are reducible
25 to SAT, the solvers have become a general purpose tool for this class
26 of problems.
27
29 --help, --help-verb Show (verbose) summary of options.
30 -pre, -no-pre
32 Enable (default) or disable preprocessing.
33 -verb {0,1,2}
35 Set the verbosity of informational output (set to 0 for silent,
36 defaults to 1)
37 -cpu-lim <unsigned>
39 Set a limit on CPU time (seconds, defaults to 2147483647).
40 -mem-lim <unsigned>
42 Set a limit on memory usage (MB, defaults to 2147483647).
43 -dimacs <output-file>
45 Print (possibly preprocessed) input problem in DIMACS format and
46 stop.
47 -luby, -no-luby
49 Enable (default) or disable the Luby restart sequence.
50 -rnd-init, -no-rnd-init
52 Randomize the initial activity values (defaults to off).
53 -gc-frac <double>
55 The fraction of wasted memory allowed before a garbage collec‐
56 tion is triggered (non-negative, defaults to 0.2).
57 -rinc <double>
59 -var-decay <double>
61 Variable activity decay factor (0 <= value <= 1, defaults to
62 0.95).
63 -cla-decay <double>
65 Clause activity decay factor (0 <= value <= 1, defaults to
66 0.999).
67 -rnd-freq <double>
69 The frequency with which the decision heuristic tries to choose
70 a random variable (0 <= value <= 1, defaults to 0).
71 -rnd-seed <double>
73 Random seed for random variable selection (non-negative,
74 defaults to 9.16483e+07).
75 -phase-saving {0,1,2}
77 Controls the level of phase saving (0=none, 1=limited, 2=full,
78 defaults to 2).
79 -ccmin-mode {0,1,2}
81 Controls conflict clause minimization (0=none, 1=basic, 2=deep,
82 defaults to 2)
83 -rfirst <int>
85 The base restart interval (positive, defaults to 100).
86 -rcheck, -no-rcheck
88 Enable (costly) or disable (default) checking for redundant
89 clauses.
90 -asymm, -no-asymm
92 Shrink clauses by asymmetric branching (disabled by default).
93 -elim, -no-elim
95 Perform variable elimination (enabled by default).
96 -simp-gc-frac <double>
98 The fraction of wasted memory allowed before a garbage collec‐
99 tion is triggered during simplification (non-negative, defaults
100 to 0.5).
101 -sub-lim <int>
103 Do not check if subsumption against a clause larger than this
104 value (-1 <= value, defaults to 1000). -1 means no limit.
105 -cl-lim <int>
107 Variables are not eliminated if they produce a resolvent with a
108 length above this limit (-1 <= value, defaults to 20). -1 means
109 no limit.
110 -grow <int>
112 Number of additional clauses that may be introduced when elimi‐
113 nating a variable. Defaults to 0.
114
116 0 if parsing the command line options fails, usage information is
117 requested, or output of the input problem in DIMACS format succeeds. 1
118 if interrupted by SIGINT or if an input file cannot be read, 3 if pars‐
119 ing the input fails, 10 if found satisfiable, and 20 if found unsatis‐
120 fiable.
121
123 minisat was written by Niklas Een, Niklas Sorensson
124 This manual page was written by Michael Tautschnig <mt@debian.org>, for
126 the Debian project (but may be used by others).
127 September 3, 2011 MINISAT(1)