UNSAT Core Extraction

Introduction to UNSAT Core Extraction

An unsatisfiable core (UNSAT core) is a subset of constraints in an unsatisfiable formula that is still unsatisfiable. A minimal unsatisfiable subset (MUS) is an UNSAT core that becomes satisfiable if any constraint is removed.

UNSAT core extraction is crucial in many applications:

  • Debugging: Identifying the source of unsatisfiability in complex constraint systems

  • Verification: Pinpointing the exact cause of property violations

  • Optimization: Guiding search algorithms by identifying conflicting constraints

  • Explanation: Providing human-readable explanations for why a system has no solution

UNSAT Core Extraction in Arlib

Arlib provides a comprehensive suite of algorithms for UNSAT core extraction:

  1. MARCO (marco.py): A highly efficient algorithm for MUS enumeration that can find multiple MUSes quickly.

  2. MUSX (musx.py): An algorithm focused on finding a single MUS with good performance characteristics.

  3. OPTUX (optux.py): An optimized algorithm for finding minimal UNSAT cores.

  4. MSS (mss.py): Algorithms for finding maximal satisfiable subsets, which are complementary to MUSes.

The module provides a unified interface through the UnsatCoreComputer class, which allows users to select the appropriate algorithm for their needs.

Usage Example

```python import z3 from arlib.unsat_core.unsat_core import get_unsat_core, Algorithm

# Define an unsatisfiable formula x, y = z3.Ints(‘x y’) constraints = [

x > 0, x < 0, y > 10, y < 5

]

# Create a solver factory function def solver_factory():

return z3.Solver()

# Extract an UNSAT core using the MARCO algorithm result = get_unsat_core(

constraints=constraints, solver_factory=solver_factory, algorithm=Algorithm.MARCO, timeout=10000 # 10 seconds

)

# Print the UNSAT core print(“UNSAT core:”) for core in result.cores:

for idx in core:

print(f” {constraints[idx]}”)

# Enumerate all MUSes from arlib.unsat_core.unsat_core import enumerate_all_mus

all_muses = enumerate_all_mus(

constraints=constraints, solver_factory=solver_factory, timeout=10000

)

print(f”Found {len(all_muses.cores)} MUSes”) ```

Algorithm Selection

The choice of algorithm depends on your specific needs:

  • MARCO: Best for enumerating multiple MUSes, especially when you need to find as many as possible

  • MUSX: Efficient for finding a single MUS quickly

  • OPTUX: Optimized for finding minimal cores with specific characteristics

For most applications, the default MARCO algorithm provides a good balance of performance and quality.

Advanced Features

The UNSAT core extraction module provides several advanced features:

  • Timeout control: Set maximum execution time for algorithms

  • Statistics collection: Gather performance metrics during execution

  • Custom solvers: Use any SMT solver that provides a compatible interface

  • Incremental solving: Reuse solver state for improved performance

References

      1. Liffiton and K. A. Sakallah. “Algorithms for computing minimal unsatisfiable subsets of constraints.” Journal of Automated Reasoning, 2008.

    1. Marques-Silva, F. Heras, M. Janota, A. Previti, and A. Belov. “On computing minimal correction subsets.” IJCAI, 2013.

    1. Belov and J. Marques-Silva. “MUSer2: An efficient MUS extractor.” Journal on Satisfiability, Boolean Modeling and Computation, 2012.