1MINISAT(1)                  General Commands Manual                 MINISAT(1)
2
3
4

NAME

6       minisat - fast and lightweight SAT solver
7

SYNOPSIS

9       minisat [options] input-file result-output-file
10
11       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

DESCRIPTION

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
22       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

OPTIONS

29       --help, --help-verb Show (verbose) summary of options.
30
31       -pre, -no-pre
32              Enable (default) or disable preprocessing.
33
34       -verb {0,1,2}
35              Set  the verbosity of informational output (set to 0 for silent,
36              defaults to 1)
37
38       -cpu-lim <unsigned>
39              Set a limit on CPU time (seconds, defaults to 2147483647).
40
41       -mem-lim <unsigned>
42              Set a limit on memory usage (MB, defaults to 2147483647).
43
44       -dimacs <output-file>
45              Print (possibly preprocessed) input problem in DIMACS format and
46              stop.
47
48       -luby, -no-luby
49              Enable (default) or disable the Luby restart sequence.
50
51       -rnd-init, -no-rnd-init
52              Randomize the initial activity values (defaults to off).
53
54       -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
58       -rinc <double>
59
60       -var-decay <double>
61              Variable activity decay factor (0 <= value  <=  1,  defaults  to
62              0.95).
63
64       -cla-decay <double>
65              Clause  activity  decay  factor  (0  <=  value <= 1, defaults to
66              0.999).
67
68       -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
72       -rnd-seed <double>
73              Random   seed   for  random  variable  selection  (non-negative,
74              defaults to 9.16483e+07).
75
76       -phase-saving {0,1,2}
77              Controls the level of phase saving (0=none,  1=limited,  2=full,
78              defaults to 2).
79
80       -ccmin-mode {0,1,2}
81              Controls  conflict clause minimization (0=none, 1=basic, 2=deep,
82              defaults to 2)
83
84       -rfirst <int>
85              The base restart interval (positive, defaults to 100).
86
87       -rcheck, -no-rcheck
88              Enable (costly) or  disable  (default)  checking  for  redundant
89              clauses.
90
91       -asymm, -no-asymm
92              Shrink clauses by asymmetric branching (disabled by default).
93
94       -elim, -no-elim
95              Perform variable elimination (enabled by default).
96
97       -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
102       -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
106       -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
111       -grow <int>
112              Number of additional clauses that may be introduced when  elimi‐
113              nating a variable.  Defaults to 0.
114

EXIT CODES

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

AUTHOR

123       minisat was written by Niklas Een, Niklas Sorensson
124
125       This manual page was written by Michael Tautschnig <mt@debian.org>, for
126       the Debian project (but may be used by others).
127
128
129
130                              September  3, 2011                    MINISAT(1)
Impressum