Z3中允许正误的限界数

Question

假设我在Z3中有一组逻辑断言，并且我想检查可满足性。在满意的模型中，是否有一种方法可以确定真/假的总数？

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

Answer 1

是。要做到这一点，有两种相对简单的方法：

• 用于一般的SMT解决程序，只需断言：

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

v1，v2等是你的布尔人。这将确保其中至少有90个是正确的。

如果使用的是

• ，则可以使用伪布尔约束。在你的情况下，你想要PbGe。有关详细信息，请参阅此答案：K-out-of-N constraint in Z3Py

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