NAME¶
minisat - fast and lightweight SAT solver
SYNOPSIS¶
minisat [
options]
input-file result-output-file
minisat takes as input a plain or gzipped DIMACS formatted file. The
satisfiability of this input problem is indicated both via standard output and
the return value.
DESCRIPTION¶
This manual page documents briefly the
minisat command. MiniSat is a
minimalistic, open-source SAT solver, developed to help researchers and
developers alike to get started on SAT. Winning all the industrial categories
of the SAT 2005 competition, MiniSat is a good starting point both for future
research in SAT, and for applications using SAT.
Despite the NP completeness of the satisfiability problem of Boolean formulas
(SAT), SAT solvers are often able to decide this problem in a reasonable time
frame. As all other NP complete problems are reducible to SAT, the solvers
have become a general purpose tool for this class of problems.
OPTIONS¶
--help, --help-verb Show (verbose) summary of options.
- -pre, -no-pre
- Enable (default) or disable preprocessing.
- -verb {0,1,2}
- Set the verbosity of informational output (set to 0 for
silent, defaults to 1)
- -cpu-lim <unsigned>
- Set a limit on CPU time (seconds, defaults to
2147483647).
- -mem-lim <unsigned>
- Set a limit on memory usage (MB, defaults to
2147483647).
- -dimacs <output-file>
- Print (possibly preprocessed) input problem in DIMACS
format and stop.
- -luby, -no-luby
- Enable (default) or disable the Luby restart sequence.
- -rnd-init, -no-rnd-init
- Randomize the initial activity values (defaults to
off).
- -gc-frac <double>
- The fraction of wasted memory allowed before a garbage
collection is triggered (non-negative, defaults to 0.2).
- -rinc <double>
- -var-decay <double>
- Variable activity decay factor (0 <= value <= 1,
defaults to 0.95).
- -cla-decay <double>
- Clause activity decay factor (0 <= value <= 1,
defaults to 0.999).
- -rnd-freq <double>
- The frequency with which the decision heuristic tries to
choose a random variable (0 <= value <= 1, defaults to 0).
- -rnd-seed <double>
- Random seed for random variable selection (non-negative,
defaults to 9.16483e+07).
- -phase-saving {0,1,2}
- Controls the level of phase saving (0=none, 1=limited,
2=full, defaults to 2).
- -ccmin-mode {0,1,2}
- Controls conflict clause minimization (0=none, 1=basic,
2=deep, defaults to 2)
- -rfirst <int>
- The base restart interval (positive, defaults to 100).
- -rcheck, -no-rcheck
- Enable (costly) or disable (default) checking for redundant
clauses.
- -asymm, -no-asymm
- Shrink clauses by asymmetric branching (disabled by
default).
- -elim, -no-elim
- Perform variable elimination (enabled by default).
- -simp-gc-frac <double>
- The fraction of wasted memory allowed before a garbage
collection is triggered during simplification (non-negative, defaults to
0.5).
- -sub-lim <int>
- Do not check if subsumption against a clause larger than
this value (-1 <= value, defaults to 1000). -1 means no limit.
- -cl-lim <int>
- Variables are not eliminated if they produce a resolvent
with a length above this limit (-1 <= value, defaults to 20). -1 means
no limit.
- -grow <int>
- Number of additional clauses that may be introduced when
eliminating a variable. Defaults to 0.
EXIT CODES¶
0 if parsing the command line options fails, usage information is
requested, or output of the input problem in DIMACS format succeeds.
1
if interrupted by SIGINT or if an input file cannot be read,
3 if
parsing the input fails,
10 if found satisfiable, and
20 if
found unsatisfiable.
AUTHOR¶
minisat was written by Niklas Een, Niklas Sorensson
This manual page was written by Michael Tautschnig <mt@debian.org>, for
the Debian project (but may be used by others).