minisat - fast and lightweight SAT solver
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.
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.
--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.
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.
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).