xenial (1) minisat.1.gz

Provided by: minisat_2.2.1-5_amd64 bug

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)