minisat+ - A Solver for Pseudo-Boolean Constraints
minisat+ <input-file> [<result-file>]
[<option> ...]
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.
- -M,-minisat
- Use MiniSat v1.13 as backend (default)
- -S,-satelite
- Use SatELite v1.0 as backend
- -ca,-adders
- Convert PB-constrs to clauses through adders.
- -cs,-sorters
- Convert PB-constrs to clauses through sorters.
- -cb,-bdds
- Convert PB-constrs to clauses through bdds.
- -cm,-mixed
- Convert PB-constrs to clauses by a mix of the above. (default)
- -ga,-gs,-gb,-gm
- Override conversion for goal function (long name: -goal-xxx).
- -w,-weak-off
- Clausify with equivalences instead of implications.
- -bdd n,
-thres=n
- Set threshold for preferring BDDs in mixed mode to n (default:
3)
- -sort-thres=n
- Set threshold for preferring sorters to n. Tried after BDDs
(default: 20)
- -goal n,
-bias=n
- Set bias goal function conversion towards sorters to n (default:
3).
- -1, -first
- Don't minimize, just give first solution found
- -A, -all
- Don't minimize, give all solutions
- -goal=n
- Set initial goal limit to n.
- -p, -pbvars
- Restrict decision heuristic of SAT to original PB variables.
- -ps{+,-,0}
- Polarity suggestion in SAT towards/away from goal (or neutral).
If parsing of the input fails then the program exits with exit
code 5.
Minisat+ was written by Niklas Een and Niklas Sorensson.