Scroll to navigation

MINISAT+(1) General Commands Manual MINISAT+(1)

NAME

minisat+ - A Solver for Pseudo-Boolean Constraints

SYNOPSIS

minisat+ <input-file> [<result-file>] [<option> ...]

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.

OPTIONS

Solver options:

Use MiniSat v1.13 as backend (default)
Use SatELite v1.0 as backend
Convert PB-constrs to clauses through adders.
Convert PB-constrs to clauses through sorters.
Convert PB-constrs to clauses through bdds.
Convert PB-constrs to clauses by a mix of the above. (default)
Override conversion for goal function (long name: -goal-xxx).
Clausify with equivalences instead of implications.
Set threshold for preferring BDDs in mixed mode to n (default: 3)
Set threshold for preferring sorters to n. Tried after BDDs (default: 20)
Set bias goal function conversion towards sorters to n (default: 3).
-1, -first
Don't minimize, just give first solution found
Don't minimize, give all solutions
Set initial goal limit to n.
Restrict decision heuristic of SAT to original PB variables.
Polarity suggestion in SAT towards/away from goal (or neutral).

Input options:

Use old variant of OPB file format.

Output options:

Turn off SAT competition output.
Turn off ANSI codes in output.
n are 1,2,3 (default: 1).
Write SAT problem to a file file. If the input problem is found to be trivially unsatisfiable then no file is written.

EXIT CODES

If parsing of the input fails then the program exits with exit code 5.

AUTHORS

Minisat+ was written by Niklas Een and Niklas Sorensson.