在Z3中使用(get-unsat-core)后，如何遍历多组unsat core？

Great question! When working with Z3, the default (get-unsat-core) command only spits out one unsatisfiable core—but if you need to iterate through all possible (or at least a full set of) cores, there are reliable strategies to make that happen. Let’s break down the best approaches:

The core idea here is: every time you get an unsat core, add a constraint that prevents that exact core from being found again, then re-solve. Repeat until the problem becomes satisfiable (meaning no more unsat cores exist). Here’s how to implement it:

• First, assign a unique boolean flag variable to each of your original constraints. For a constraint C_i, define b_i and assert (=> b_i C_i). This lets you toggle whether each constraint is active.
• Run your first (check-sat); if it returns unsat, use (get-unsat-core) to get the set of flags corresponding to the core.
• Add a new constraint: (not (and b_{i1} b_{i2} ... b_{ik}))—this forbids the solver from selecting that exact combination of constraints again.
• Repeat the solve-and-block cycle until (check-sat) returns sat.

Here’s a quick SMT-LIB example to demonstrate:

(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const b3 Bool)
(declare-const x Int)

; Bind constraints to their flag variables
(assert (=> b1 (< x 0)))
(assert (=> b2 (> x 5)))
(assert (=> b3 (= x 3)))

; First solve
(check-sat)
(get-unsat-core) ; Might return (b1 b2)

; Block this core from being found again
(assert (not (and b1 b2)))

; Second solve
(check-sat)
(get-unsat-core) ; Might return (b1 b3)

; Block this core too
(assert (not (and b1 b3)))

; Final solve
(check-sat) ; Now returns sat—no more unsat cores left

If you’re using Z3’s Python bindings, you can automate this entire process with a loop, avoiding manual SMT-LIB writing. The logic stays the same, but the code handles iteration and core tracking for you:

from z3 import *

# Define variables and constraints with flags
x = Int('x')
b1 = Bool('b1')
b2 = Bool('b2')
b3 = Bool('b3')

solver = Solver()
solver.add(Implies(b1, x < 0))
solver.add(Implies(b2, x > 5))
solver.add(Implies(b3, x == 3))

all_unsat_cores = []

while True:
    result = solver.check()
    if result != unsat:
        break  # No more cores to find
    
    current_core = solver.unsat_core()
    core_set = set(current_core)
    
    # Avoid duplicate cores (in case Z3 returns the same one unexpectedly)
    if core_set not in all_unsat_cores:
        all_unsat_cores.append(core_set)
        # Add constraint to block this core
        solver.add(Not(And(*current_core)))

print("All found unsat cores:")
for core in all_unsat_cores:
    print(core)

• Core Explosion Risk: If your constraint set is large, there could be an exponential number of unsat cores. In such cases, you might want to focus only on minimal cores (cores where removing any single constraint makes the problem satisfiable). Z3’s default (get-unsat-core) returns a minimal core, and blocking these will help you collect only minimal ones.
• Performance Tuning: Set the parameter smt.core.minimize=true to make Z3 prioritize returning minimal cores, which speeds up the iteration process.
• Verify Minimality: If you need to ensure you’re only collecting minimal cores, after retrieving a core, you can test each constraint in the core by removing it and checking if the problem becomes sat. If it does, the core is minimal.

内容的提问来源于stack exchange，提问作者Amin