.TH "MINISAT+" 1
.SH NAME
minisat+ \- A Solver for Pseudo-Boolean Constraints

.SH SYNOPSIS
.B minisat+
<input\-file> [<result\-file>] [<option> ...]

.SH DESCRIPTION
MiniSat+ is a solver for Pseudo-Boolean constraints, based on MiniSat.

Pseudo-Boolean constraints can be used to describe certain kinds of
combinatorial optimization problems. Variables are Boolean, that is
can take as values only 0 or 1. (In-)equations used in hard
constraints and objective functions, however, may use arbitrary
integer coefficients.

Minisat+ accepts problem specifications written in the OPB format.

.SH OPTIONS
.SS "Solver options:"
.TP
.BR \-M , \-minisat
Use MiniSat v1.13 as backend (default)
.TP
\.BR \-S , \-satelite
Use SatELite v1.0 as backend
.TP
.BR \-ca , \-adders
Convert PB\-constrs to clauses through adders.
.TP
.BR -cs , -sorters
Convert PB\-constrs to clauses through sorters.
.TP
.BR -cb , \-bdds
Convert PB\-constrs to clauses through bdds.
.TP
.BR \-cm , \-mixed
Convert PB\-constrs to clauses by a mix of the above. (default)
.TP
.BR -ga , -gs , -gb , -gm
Override conversion for goal function (long name: \fB\-goal\-xxx\fR).
.TP
.BR \-w , \-weak\-off
Clausify with equivalences instead of implications.
.TP
\fB\-bdd \fIn\fR, \fB\-thres=\fIn\fR
Set threshold for preferring BDDs in mixed mode to \fIn\fR (default: 3)
.TP
\fB\-sort\-thres=\fIn\fR
Set threshold for preferring sorters to \fIn\fR. Tried after BDDs (default: 20)
.TP
\fB\-goal \fIn\fR, \fB\-bias=\fIn\fR
Set bias goal function conversion towards sorters to \fIn\fR (default: 3).
.TP
\fB\-1\fR, \fB\-first\fR
Don't minimize, just give first solution found
.TP
\fB\-A\fR, \fB\-all\fR
Don't minimize, give all solutions
.TP
\fB\-goal=\fIn\fR
Set initial goal limit to \fIn\fR.
.TP
\fB\-p\fR, \fB\-pbvars\fR
Restrict decision heuristic of SAT to original PB variables.
.TP
\fB\-ps\fR{+,\-,0}
Polarity suggestion in SAT towards/away from goal (or neutral).

.SS "Input options:"
.TP
\fB\-of\fR, \fB\-old\-fmt\fR
Use old variant of OPB file format.

.SS "Output options:"
.TP
\fB\-s\fR, \fB\-satlive\fR
Turn off SAT competition output.
.TP
\fB\-a\fR, \fB\-ansi\fR
Turn off ANSI codes in output.
.TP
\fB\-v\fIn\fR Set verbosity level to \fIn\fR. Possible values for
\fIn\fR are 1,2,3 (default: 1).
.TP
\fB\-cnf=\fIfile\fR
Write SAT problem to a file \fIfile\fR. If the input problem is found to be
trivially unsatisfiable then no file is written.

.SH "EXIT CODES"
If parsing of the input fails then the program exits with exit code 5.

.SH AUTHORS
Minisat+ was written by Niklas Een and Niklas Sorensson.