unsatisfiable core

An unsatisfiable core is a set of formulas for which no satisfying instance exists. The Alloy Analyzer has a built-in ability to produce an unsat core when it fails to find an instance for a given command. An unsat core can be used to detect potential inconsistencies in a specification (for run command), or check whether an assertion holds vacuously true (for check).

To enable the unsat core generation, select "Minisat with Unsat Core" option for the choice of the SAT solver:

When the analyzer fails to find an instance/counterexample for a run/check command, the unsat core can be highlighted by clicking on ''Core'' in the message panel:

Each Alloy constraint that belongs to the unsat core is highlighted red. A constraint highlighted with a bold shade of red is guaranteed to be a member of the core. A constraint highlighted with a lighter shade of red is potentially, but not necessarily, part of the core.

The analyzer allows the user to control two characteristics of an unsat core: core size and granularity.

Core size: The analyzer provides three minimization strategies that determine the size of a resulting core:

A core computed using the "Slow" strategy is guaranteed to a local minimum; that is, if any constraint is removed from this core, the resulting set of constraints is satisfiable. The "Fast" strategy takes the least amount of computation, but the resulting core is also the least accurate, and may contain a number of false positives (i.e., constraints that are highlighted light red but not actually part of the core).

Core granularity: By default, each constraint in an unsat core is a top-level conjunct Ci in a given Alloy specification S (where 1 <= i <= n):

S = C1 /\ C2 /\ ... /\Cn

However, a top-level conjunct might be too coarse-grained for effectively locating the source of an inconsistency in the specification. For example, consider the following top-level conjunct:

!(A \/ !B)

Let us assume that the formula B is inconsistent, and the analyze fails to find a satisfying instance for the specification. A resulting unsat core with the default top-level granularity highlights the entire conjunct !(A \/ !B). Now, consider the following equivalent formula, obtained by pushing the negation inside the disjunction:

!A /\ B

Given this formula, the analyzer is able to generate a core that highlights only B.

The analyzer provides four different types of logical transformations for controlling the granularity of an unsat core (listed in the order of increasing granularity and the amount of required computation):