4.2.8.1. Assumptions

An assumption interface for solvers that support solving under assumptions. The Boolean variables passed to \({\bf assume}\) are assumed to be true; a solver that supports assumptions may, when the model is unsatisfiable under these assumptions, report a subset of them as an unsatisfiable core. MiniZinc maps such a core back to the original expressions and prints it for inspection (look for the Unsatisfiable core comment in the solver output).

In this section: assume.

assume

predicate assume(array [int] of var bool: b)

Assume that the Boolean variables in b hold.

A solver supporting assumptions treats these as assumptions rather than hard constraints, and may report a subset of them as an unsatisfiable core when the model is unsatisfiable under the assumptions. Fixed-true elements are dropped; a fixed-false element makes the model trivially unsatisfiable (and is reported to the user). If the selected solver has no native support, the assumptions are posted as hard constraints and a warning is issued.