---
name: "minisat+"
section: "1"
platform: "linux"
package: "minisat+"
version: "1.0-5"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/minisat+"
---

# minisat+(1)

A Solver for Pseudo-Boolean Constraints

## 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:

- **-M**,**-minisat**

  Use MiniSat v1.13 as backend (default)

- .BR -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.

- **-v***n* 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.

## 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.