Z3能否基于抽象函数公式求解对应的未知布尔函数？

可行性结论 #

可以实现，Z3原生支持该需求，核心通过未知函数声明、相似性约束绑定、增量枚举三个步骤完成。

具体实现步骤 #

• 抽象布尔函数：将原公式中需要设为未知的布尔函数声明为Z3的Function对象，定义域、值域均设为BoolSort()，替换原公式中的固定函数实现。
• 添加相似性约束：按照你定义的「与原公式相似」规则添加约束，常见规则包括：未知函数在原公式的所有可满足输入上输出与原函数一致、两个公式的语义等价输入占比达到指定阈值、未知函数的真值表汉明距离与原函数小于指定值等。
• 全量模型枚举：每次求解得到可行模型后，生成对应阻塞子句加入求解器，排除当前模型后再次求解，循环直到求解器返回unsat，即可遍历所有符合要求的模型。

代码示例 #

from z3 import *

# 示例场景：原公式为 (a & b) | c，将二元与运算替换为未知布尔函数f
a, b, c = Bools('a b c')
# 声明二元布尔函数f：输入两个布尔值，输出一个布尔值
f = Function('f', BoolSort(), BoolSort(), BoolSort())
# 生成抽象后的公式
abstract_formula = f(a, b) | c
# 相似性约束示例：要求f与原与函数的真值表汉明距离不超过1
similarity_constraint = AtMost(
    f(True, True) == True,
    f(True, False) == False,
    f(False, True) == False,
    f(False, False) == False,
    3 # 4个输入中最多3个和原函数一致，即汉明距离≤1
)

s = Solver()
s.add(abstract_formula, similarity_constraint)

model_idx = 0
while s.check() == sat:
    model = s.model()
    model_idx += 1
    print(f"第{model_idx}个模型对应的f函数真值表：")
    for va in [True, False]:
        for vb in [True, False]:
            print(f"f({va}, {vb}) = {model.eval(f(BoolVal(va), BoolVal(vb)))}")
    print("---")
    # 添加阻塞子句，排除当前模型
    block_conds = []
    for d in model.decls():
        if d.name() == 'f':
            # 函数类型需要覆盖所有输入组合生成阻塞条件
            for va in [True, False]:
                for vb in [True, False]:
                    block_conds.append(f(BoolVal(va), BoolVal(vb)) == model.eval(f(BoolVal(va), BoolVal(vb))))
        else:
            block_conds.append(d() == model[d])
    s.add(Not(And(block_conds)))

注意事项 #

• 未知布尔函数的输入变量数决定了函数实现的总数量，输入数超过4个后总实现量会指数级上升，枚举全量模型的耗时会快速增长，可按需添加额外约束缩小求解空间。
• 对函数类型生成阻塞子句时，必须覆盖所有可能的输入取值组合，才能保证不会重复返回相同的函数实现。

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