z3 - 在 Z3 中编码 "at-most-k/at-least-k booleans are true"约束

Question

对于任意 k 和 bool 变量的数量，在 Z3 中对“这些 bool 变量中的至少 k/至多 k 必须为真”约束进行编码的好方法是什么？

我正在考虑通过引入新的 PB 变量(使用 this encoding )，通过双条件(例如 x == true iff y == 1 )将它们与我的 bool 变量相关联，并断言它们的总和来将“至少 k”转换为伪 bool 问题大于或等于 k。这是一种合理的方法，还是我应该使用更简单/更有效的编码？

Answer 1

最简单的方法是使用算术对基数约束进行编码。
所以如果你想说a + b + c <= 2，其中a、b、c都是Bool，那么你可以
将其公式化为 (if a 1 0) + (if b 1 0) + (if c 1 0) >= 2。
底层求解器 Simplex 通常做得非常合理
用这种编码。

还有许多其他方法可以处理基数约束。
一种是将基数约束编译成“排序电路”，有
在这方面相当发达的方法。 Z3 的 future 版本将具有直接
支持基数约束，以及更普遍的伪 bool 不等式。
如果你有很多基数限制并且觉得很冒险
欢迎您尝试“选择”分支
这是正在开发中。它对伪 bool 不等式使用专用格式，并且
还包括一种模式，它将“(if a 1 0) + (if b 1 0) + (if c 1 0) >= 2”不等式检测为 PB 不等式。也就是说，我将首先尝试非常简单的编码，看看基于单工的引擎如何为您的域工作。