PySMT结合Z3求解器：如何均匀随机抽取公式的n个解？

问题描述 #

我需要从给定的SMT公式中抽取n个解，采用PySMT结合Z3求解器实现。当前做法是每次调用get_model得到一个解后，将该解的否定加入公式迭代求解，但最终变量的取值分布很差，而均匀分布对我的项目至关重要。有没有办法让抽取的n个样本中，所有变量的取值在其值域内近似均匀分布？

当前代码如下：

solutions = []

for s in range(n_samples):
        solution = []
        model = get_model(formula)

       if model is None:
            print("Not enough solutions")
            break

        sample = []
        for o in self.objects:
            attributes = {
                attr: [
                    x
                    for x in self.values[attr]
                    if model[self.get_attribute(attr, o, x)].is_true()
                ][0]
                for attr in self.values
            }
            sample.append(attributes)

        solutions.append(sample)

        # Exclude the current model by adding a negation of its assertions
        # to the problem, so the next iteration finds a different solution.
        negation = Not(And(EqualsOrIff(x, y) for (x, y) in model))
        formula = And(formula, negation)

核心问题分析 #

你当前的方法本质是增量排除已得解，Z3的默认搜索策略会优先探索相邻的解空间，导致后续解和已得解高度相似，自然出现分布不均的问题。要实现均匀采样，需要主动引导求解器遍历不同的取值区域，而不是被动排除。

可行的解决方法 #

1. 随机偏好约束引导 #

每次求解前，给每个变量添加临时随机偏好约束，引导Z3优先选择当前采样较少的取值。具体步骤：

• 维护每个变量各取值的采样计数
• 每次迭代时，对每个变量，计算取值的采样频率，给频率低的取值赋予更高的“偏好权重”
• 将这些偏好作为约束加入公式，迭代后再基于原始公式重新构建约束，避免公式过度膨胀

示例修改代码：

from pysmt.shortcuts import get_model, And, Not, EqualsOrIff
import random

# 初始化采样计数：{变量: {取值: 计数}}
sample_counts = {attr: {v: 0 for v in self.values[attr]} for attr in self.values}
solutions = []
original_formula = formula  # 保存原始公式，避免叠加否定导致公式膨胀

for s in range(n_samples):
    # 构建偏好约束：优先选采样少的取值
    preference_constraints = []
    for attr in self.values:
        # 按采样计数升序排序取值，随机选低采样值作为偏好
        sorted_vals = sorted(self.values[attr], key=lambda v: sample_counts[attr][v])
        preferred_vals = random.sample(sorted_vals[:len(sorted_vals)//2], 1)
        for o in self.objects:
            attr_sym = self.get_attribute(attr, o, preferred_vals[0])
            preference_constraints.append(attr_sym)
    
    # 组合原始公式+偏好约束+排除已得解的约束
    current_formula = And(original_formula, *preference_constraints)
    if solutions:
        exclude_clauses = []
        for sample in solutions:
            clause = []
            for o_attrs in sample:
                for attr, val in o_attrs.items():
                    sym = self.get_attribute(attr, o, val)
                    clause.append(sym)
            exclude_clauses.append(Not(And(*clause)))
        current_formula = And(current_formula, *exclude_clauses)
    
    model = get_model(current_formula)
    if model is None:
        print("Not enough solutions")
        break
    
    # 解析样本并更新采样计数
    sample = []
    for o in self.objects:
        attributes = {}
        for attr in self.values:
            val = [x for x in self.values[attr] if model[self.get_attribute(attr, o, x)].is_true()][0]
            attributes[attr] = val
            sample_counts[attr][val] += 1
        sample.append(attributes)
    solutions.append(sample)

2. 分层预采样 #

如果变量值域不大，可以先按变量取值拆分公式，再按比例从每个子公式中抽取解：

• 对每个变量的每个取值，生成公式 ∧ (变量=取值)的子公式
• 统计每个子公式的解数量，按均匀分布的目标分配每个子公式的采样数
• 从每个子公式中抽取对应数量的解（可复用你原来的迭代排除法）

这种方法能保证每个变量的取值被覆盖到，适合值域规模较小的场景。

3. 调整Z3求解器的随机策略 #

Z3支持随机化搜索策略，通过设置参数让求解器每次选择不同的分支，避免陷入局部解空间：

• 在调用get_model前，配置Z3的随机种子、随机决策等参数

示例代码：

from pysmt.solvers.z3 import Z3Solver

def get_random_model(formula):
    with Z3Solver() as solver:
        solver.add_assertion(formula)
        # 设置Z3随机化参数
        solver.z3.set("random_seed", random.randint(0, 100000))
        solver.z3.set("smt.random_seed", random.randint(0, 100000))
        solver.z3.set("sat.random_initial_value", True)
        solver.z3.set("sat.random_polarity", True)
        if solver.solve():
            return solver.get_model()
        else:
            return None

# 循环中用get_random_model替代原get_model

注意事项 #

• 避免公式过度膨胀：直接叠加所有已得解的否定会让公式越来越大，求解速度骤降，建议基于原始公式重新构建约束，或定期清理旧的排除条件。
• 提前检测解空间大小：如果总解数远小于需要的采样数，均匀分布无从谈起，需提前判断并调整采样目标。

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