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).

                                               September  3, 2011                                     MINISAT(1)