## 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 `C`

in a given Alloy
specification _{i}`S`

(where `1 <= i <= n`

):

S = C_{1}/\ C_{2}/\ ... /\C_{n}

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

**Top-level conjuncts only**: No logical transformation is applied, and constraints in the core correspond to the top-level conjuncts in the given Alloy specification.**Flatten the formula once at the beginning**: The original formulas are transformed into logically equivalent ones by pushing negation in as much as possible (without expanding quantifiers).**Flatten the formula at the beginning and after skolemnizing**: After skolemnization is applied to eliminate existential quantifiers, negation is further pushed into the formulas.**In addition to flattening the formula twice, expand the quantifiers**: Each universal quantifier is fully expanded given the bounds on the signatures, increasing the granularity of a core to parts of the quantified expressions.