# Enumeration of Minimal Unsatisfiable Cores and Maximal Satisfying Subsets

This tutorial illustrates how to use Z3 for extracting all minimal unsatisfiable cores together with all maximal satisfying subsets.

## Origin

The algorithm that we describe next represents the essence of the core extraction procedure by Liffiton and Malik and independently by Previti and Marques-Silva:

Enumerating Infeasibility: Finding Multiple MUSes Quickly
Mark H. Liffiton and Ammar Malik
in *Proc. 10 ^{th} International Conference on Integration of Artificial
Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming* (CPAIOR-2013), 160-175, May 2013.

Partial MUS Enumeration
Alessandro Previti, Joao Marques-Silva
in *Proc. AAAI-2013* July 2013

## Z3py Features

This implementation contains no tuning. It was contributed by Mark Liffiton and it is a simplification of one of the versions available from his Marco Polo Web site. Code for eMUS is also [available. The example illustrates the following features of Z3's Python-based API:

- Using assumptions to track unsatisfiable cores.
- Using multiple solvers and passing constraints between them.
- Calling the C-based API from Python. Not all API functions are supported over the Python wrappers. This example shows how to get a unique integer identifier of an AST, which can be used as a key in a hash-table.

## Idea of the Algorithm

The main idea of the algorithm is to maintain two logical contexts and exchange information between them:

The

*MapSolver*is used to enumerate sets of clauses that are not already supersets of an existing unsatisfiable core and not already a subset of a maximal satisfying assignment. The*MapSolver*uses one unique atomic predicate per*soft*clause, so it enumerates sets of atomic predicates. For each minimal unsatisfiable core, say, represented by predicates*p*, the_{1}, p_{2}, p_{5}*MapSolver*contains the clause*¬ p*. For each maximal satisfiable subset, say, represented by predicats_{1}∨ ¬ p_{2}∨ ¬ p_{5}*p*, the_{2}, p_{3}, p_{5}*MapSolver*contains a clause corresponding to the disjunction of all literals not in the maximal satisfiable subset,*p*._{1}∨ p_{4}∨ p_{6}The

*SubsetSolver*contains a set of soft clauses (clauses with the unique indicator atom occurring negated). The*MapSolver*feeds it a set of clauses (the indicator atoms). Recall that these are not already a superset of an existing minimal unsatisfiable core, or a subset of a maximal satisfying assignment. If asserting these atoms makes the*SubsetSolver*context infeasible, then it finds a minimal unsatisfiable subset corresponding to these atoms. If asserting the atoms is consistent with the*SubsetSolver*, then it extends this set of atoms maximally to a satisfying set.