Z3最大满足子集查找文档示例存在Bug

问题根源 #

核心问题在于Z3的MSSSolver返回MSS结果时，默认给出的是约束的别名变量（格式类似|constraint_name|），而非原约束公式本身。直接将这些别名变量的交集添加到求解器，仅强制了"该约束被选中"的元信息，并没有真正引入原约束的逻辑规则，这必然会导致模型矛盾或结果与预期不符——比如你遇到的p、q同真但Not(And(p,q))被标记为True，本质就是只添加了该约束的别名变量为真，却没添加约束本身的逻辑限制。

解决方案 #

关键是将MSS返回的别名变量映射回原约束公式，再添加到求解器中，具体步骤如下：

1. 建立原约束与别名变量的映射关系
   使用solver.assert_and_track()方法添加约束时，显式记录每个原约束对应的别名变量：

   from z3 import *
   
   p, q = Bools('p q')
   constraints = [p, q, Not(And(p, q))]
   
   mss_solver = MSSSolver()
   constraint_map = {}
   for c in constraints:
       alias = FreshBool()
       mss_solver.assert_and_track(c, alias)
       constraint_map[alias] = c
   

2. 将MSS别名变量转换为原约束
   获取MSS的别名集合后，通过预存的映射表替换为原约束，再添加到普通求解器：

   # 获取单个MSS并转换
   mss_aliases = mss_solver.get_mss()
   mss_constraints = [constraint_map[alias] for alias in mss_aliases]
   
   solver = Solver()
   solver.add(mss_constraints)
   if solver.check() == sat:
       print(solver.model())
   else:
       print("unsat")
   

3. 处理所有MSS的交集
   若要取所有MSS的公共约束，先收集所有MSS的别名集合，找出公共别名后再映射回原约束：

   # 假设已获取所有MSS的别名列表all_mss_aliases
   common_aliases = set.intersection(*[set(mss) for mss in all_mss_aliases])
   common_constraints = [constraint_map[alias] for alias in common_aliases]
   
   solver.add(common_constraints)
   # 执行后续求解逻辑
   

关键说明 #

• assert_and_track(c, alias)的作用是将约束c与别名变量alias绑定，Z3内部通过别名跟踪约束是否被纳入MSS；
• 别名变量仅代表"约束被选中"的状态，不包含约束本身的逻辑，必须映射回原约束才能保证求解逻辑的正确性。

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