z3 - Z3 中允许的 True/False 的边界数

Question

假设我在 Z3 中有一组逻辑断言，我想检查可满足性。有没有办法限制令人满意的模型中的真/假总数？

例如，我可能有一组涉及 100 个布尔变量的断言，但我只对至少有 90 个 True 的解决方案感兴趣。

标签： z3satisfiability

Answer 1

是的。有两种相对简单的方法可以实现这一点：

• 对于通用 SMT 求解器，只需断言：

  (assert (<= 90 (+ (ite v1 1 0) (ite v2 1 0) ...)))

  wherev1等v2是你的布尔值。这确保其中至少有 90 个是正确的。

• 如果您使用的是 z3，那么您可以使用伪布尔约束。在您的情况下，您想要PbGe. 有关详细信息，请参阅此答案：Z3Py 中的 K-out-of-N 约束

请注意，您甚至可以让 z3 “最大化”真实布尔值的数量。这将使用优化引擎，并通过最大化上面第一个选项中的和表达式来工作。您可以在 SO 中找到许多关于如何使用优化器的参考资料。