SYNOPSIS

minisat2 [options] input-file result-output-file

DESCRIPTION

This manual page documents briefly the minisat2 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 satisfiabilty 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

-h, -help Show summary of options.

-pre {none,once}

Disable or enable preprocessing.

-asymm

Unknown.

-rcheck

Enable checking for redundant clauses.

-grow <num> [ >0 ]

Number of additional clauses that may be introduced when eliminating a variable. Defaults to 0.

-polarity-mode {true,false,rnd}

Set default polarity for decisions made (true, false, or random).

-decay <num> [ 0 - 1 ]

Inverse of the variable activity decay factor (defaults to 0.95).

-rnd-freq <num> [ 0 - 1 ]

The frequency with which the decision heuristic tries to choose a random variable (defaults to 0.02).

-freeze <freeze-file>

File containing a list of literals to be frozen at the given polarity.

-dimacs <output-file>

Print (possibly preprocessed) input problem in DIMACS format.

-verbosity {0,1,2}

Set the verbosity of informational output.

AUTHOR

minisat2 was written by Niklas Een, Niklas Sorensson

This manual page was written by Michael Tautschnig <[email protected]>, for the Debian project (but may be used by others).