table of contents
MINISAT+(1) | General Commands Manual | MINISAT+(1) |
NAME¶
minisat+ - A Solver for Pseudo-Boolean ConstraintsSYNOPSIS¶
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:¶
- -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).
Input options:¶
- -of, -old-fmt
- Use old variant of OPB file format.
Output options:¶
- -s, -satlive
- Turn off SAT competition output.
- -a, -ansi
- Turn off ANSI codes in output.
- -vn Set verbosity level to n. Possible values for
- n are 1,2,3 (default: 1).
- -cnf=file
- Write SAT problem to a file file. If the input problem is found to be trivially unsatisfiable then no file is written.