MARCO

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.

Mapping Infeasibility

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.

Our running example will be the constraint system (with Boolean variables a and b):

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

C is infeasible, containing three MUSes:

{a, ¬a}, {b, ¬b}, and {¬a, ¬b, a ∨ b}

MARCO is short for Mapping Regions of Constraints, 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.

This is the lattice for three constraints, {a, ¬a, b}:

In the larger examples below, most node labels will be hidden until you hover over them. Here is the lattice for the example constraint set C = {a, ¬a, b, ¬b, a ∨ b}:

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.

Satisfiability of individual subsets can be mapped on a lattice with color. For the three constraints, {a, ¬a, b}, all but two subsets are satisfiable:

This is the map for the running example. The MUSes are the three red/UNSAT nodes with only green/SAT children.


Helper Functions

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

grow()

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.

Grow Algorithm
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 =

shrink()

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.

Shrink Algorithm
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

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 Ci is represented by a variable xi in 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 Ci whose variable representations are 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.

MARCO Algorithm
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 :