如何用Z3约束求解器让两个Int变量匹配二维数组任意数对

现有两个Z3 Int类型变量x1和x2，以及二维数组list = [[1,2],[12,13],[45,7]]，需要编写约束让x1和x2取数组中的任意一组数对（比如x1=1且x2=2，或x1=12且x2=13等）。但用循环添加And约束的方式会导致求解器永远返回unsat，需解决该问题且适配任意数量的数组数对。

用户尝试的错误代码：

solver = Solver()
for i in range(0,len(list)):
      solver.add(And((x1==list[i][0]),(x2==list[i][1])))

错误原因 #

这段代码每次循环都向求解器添加一组与约束，相当于要求x1同时等于数组中所有数对的第一个元素，x2同时等于所有数对的第二个元素——这种矛盾的约束必然导致求解器返回unsat。

正确实现 #

需要用或约束（Or）让求解器选择数组中任意一组数对满足即可，代码如下：

from z3 import *

x1 = Int('x1')
x2 = Int('x2')
list_pairs = [[1,2],[12,13],[45,7]]

solver = Solver()
# 生成所有数对对应的约束，用Or包裹实现多选一
pair_constraints = []
for pair in list_pairs:
    pair_constraints.append(And(x1 == pair[0], x2 == pair[1]))
solver.add(Or(*pair_constraints))

# 检查并输出单个解
if solver.check() == sat:
    model = solver.model()
    print(f"x1 = {model[x1]}, x2 = {model[x2]}")
else:
    print("unsat")

扩展：遍历所有可行解 #

如果需要输出数组中所有符合条件的数对解，可以循环排除已找到的解，直到求解器返回unsat：

# 遍历所有可行解
while solver.check() == sat:
    model = solver.model()
    x1_val = model[x1].as_long()
    x2_val = model[x2].as_long()
    print(f"x1 = {x1_val}, x2 = {x2_val}")
    # 添加约束排除当前解，触发下一轮求解
    solver.add(Not(And(x1 == x1_val, x2 == x2_val)))

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