如何提取公式的多个不同模型？Z3重复输出同一模型求助

Great question! Let's tackle your two questions and fix that duplicate model issue you're seeing.

Question 1: Can we output at most 2 solutions if multiple exist? #

Absolutely! You can easily limit your output to 2 distinct models—you just need to stop the enumeration process once you've retrieved the second one. We'll cover how to do this alongside solving your core problem below.

Question 2: How to output multiple distinct models (and why your current approach repeats the same one) #

The reason your (check-sat) (get-model) (check-sat) (get-model) sequence returns the same model twice is simple: Z3 doesn't automatically track or exclude models it's already found. By default, it just returns the first satisfying assignment it finds each time you call check-sat.

To get different models, you need to block the model you just found by adding a new constraint that explicitly rules out that exact assignment. Here's how to do it, both in raw SMT-LIB and using Z3's programmatic APIs like z3py:

Method 1: Manual blocking in SMT-LIB #

Let's use a simple example where we want models for x + y = 5 (integer variables):

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 5))

; Get first model
(check-sat)
(get-model) ; Might return x=0, y=5

; Block this model so Z3 finds a different one
(assert (not (and (= x 0) (= y 5))))

; Get second model
(check-sat)
(get-model) ; Now returns something like x=1, y=4

; Stop here if you only want 2 models!

After retrieving each model, add a negation of the exact assignment from that model. This forces Z3 to look for a new solution that doesn't match the ones you've already seen.

Method 2: Automated enumeration with z3py (Python) #

If you're using Z3's Python API, you can automate the blocking process to avoid manually writing constraints—perfect for cases with many variables:

from z3 import *

# Define variables and constraints
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 5)

# Retrieve up to 2 distinct models
max_models = 2
for i in range(max_models):
    if solver.check() == sat:
        model = solver.model()
        print(f"Model {i+1}:")
        print(model)
        
        # Create a constraint to block this model
        block_clause = []
        for var in model:
            # var is a FuncDecl; var() gives the actual variable
            block_clause.append(var() != model[var])
        solver.add(Or(block_clause))
    else:
        print(f"No more models found after {i} iterations.")
        break

This script will automatically find and block each model, stopping once it has 2 distinct ones or runs out of solutions.

Key Notes #

• Z3 doesn't have a built-in command to return multiple models directly—you have to explicitly block each one you retrieve.
• If your formula has a finite number of models, this method will eventually exhaust all of them. For infinite models (like real numbers with infinitely many solutions), you can still get distinct ones, but you'll never run out.
• To limit to exactly 2 models, just stop the process after the second successful check-sat call.

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