Hello! This page presents the MARCO algorithm for efficiently analyzing infeasible constraint systems. Interactive visualizations are included throughout to help explain key points. You can control the execution of algorithms with the provided buttons and interact with the visualizations for additional details.

MARCO is an algorithm for analyzing infeasible constraint systems with the goal of enumerating all minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes). Typically, MUSes are of more interest, as they have found broader application, and we will focus on them here.

MARCO is short for **Ma**pping **R**egions of **Co**nstraints, and that roughly describes how it operates.
This mapping can be represented visually on the *power set lattice* of a constraint system.
The power set of a set of constraints is the set of all constraint subsets.
Power sets can be represented visually in *Hasse diagrams*, which provide a useful way to visualize all of the subsets and their relation to each other.
In a Hasse diagram, every subset in the power set is represented by a node, and edges connect immediate supersets and subsets.

Given some set of constraints, MARCO's goal of enumerating MUSes and MSSes is equivalent to fully "mapping" the power set's *feasibility*.
Every subset of constraints is either SAT or UNSAT, and the set of MUSes and MSSes provide complete information on the satisfiability of every subset.
Any node that is a superset of an MUS must be unsatisfiable, and any subset of an MSS is satisfiable.
On the map, then, this means that every MUS is a "low point" in the unsatisfiable region, while MSSes are "high points" in the satisfiable nodes.

MARCO operates, at a high level, by repeatedly identifying one of these high or low points (an MSS or an MUS), marking a region of the map as "explored" based on what it finds, and continuing from a new, unexplored point.
Two important functions for finding MSSes and MUSes are `grow()`

and `shrink()`

.
Each operates on a *seed*, some subset of a constraint system that is known to be either SAT (for `grow()`

) or UNSAT (for `shrink()`

).
MARCO uses these as subroutines such that each can be implemented using whatever techniques are known to be most efficient at the time; the below algorithms are very basic versions for illustrating the concept.
The visualizations below illustrate the operation of `grow()`

and `shrink`

on seeds in the constraint set `C = {a, ¬a, b, ¬b, a ∨ b}`

.

The purpose of `grow()`

is to find an MSS.
It takes a satisfiable constraint subset `seed`

as input and iteratively adds constraints to `seed`

as long as those constraints do not make `seed`

unsatisfiable.
The last subset found is therefore maximal.

Inputs: Constraint system

`C`

, SAT constraint subset `seed`

for`c`

in`C`

\`seed`

:

if`seed`

∪ {`c`

} is satisfiable:

`seed`

←`seed`

∪ {`c`

}

return`seed`

Click on a node to select a new initial `seed`

subset.

`seed`

=`c`

=

The purpose of `shrink()`

is to find an MUS.
It takes an unsatisfiable constraint subset `seed`

as input and iteratively removes constraints from `seed`

as long as those constraints do not make `seed`

satisfiable.
The last subset found is therefore minimal.

Inputs: Constraint system

`C`

, UNSAT constraint subset `seed`

for`c`

in`seed`

:

if`seed`

\ {`c`

} is unsatisfiable:

`seed`

←`seed`

\ {`c`

}

return`seed`

Click on a node to select a new initial `seed`

subset.

`seed`

=`c`

=

MARCO works by iteratively finding MSSes and MUSes. It takes the constraint set `C`

as input. Additionally, it takes `Map`

, initially an empty boolean formula over `|C|`

variables. Each constraint `C`

is represented by a variable _{i}`x`

in _{i}`Map`

. `getUnexplored()`

finds a variable assignment `m`

that satisfies `Map`

. `getUnexplored()`

is biased towards assignments with more variables set to `true`

. Since `Map`

is initially empty, each variable will be set to `true`

in the initial model.

Next, `seed`

is set to the subset of all constraints `C`

whose variable representations are _{i}`true`

in the model `m`

. Then, MARCO checks if the subset `seed`

is satisfiable. If `seed`

is satisfiable, then it is a subset of an MSS. MARCO finds the MSS by "growing" `seed`

. Alternatively, if `seed`

is unsatisfiable, then it contains an MUS. MARCO finds this MUS by "shrinking" `seed`

.

Notice that once an MSS is found, MARCO is no longer concerned with the subsets of that MSS. `blockDown()`

returns a clause that is added to `Map`

. This clause ensures that neither the MSS or any of its subsets will be viable models of `Map`

.

Similarly, once an MUS is found, MARCO is no longer concerned with all sets of constraints that contain the MUS. Thus, `blockUp()`

returns a clause that is added to `Map`

. This clause ensures that neither the MUS or any sets that contain the MUS will be viable models of `Map`

.

MARCO continues until there no longer exists a satisfying assignment for `Map`

. Below is a visual example of MARCO.

Input: Constraint system

`C`

`Map`

← ⊤

while`Map`

is satisfiable:

`seed`

← getUnexplored(`Map`

)

if`seed`

is satisfiable:

`MSS`

← grow(`seed`

,`C`

)

output`MSS`

`Map`

←`Map`

∧ blockDown(`MSS`

)

else:

`MUS`

← shrink(`seed`

,`C`

)

output`MUS`

`Map`

←`Map`

∧ blockUp(`MUS`

)

Example input: `C`

= {a, ¬a, b, ¬b, a ∨ b}

`seed` : | |

`Map` : | |

`MUSes` : | |

`MSSes` : |