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

Question

在 Z3 中，对于任意 k 和布尔变量的数量？

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

Answer 1

最简单的方法是使用算术编码基数约束。 所以如果你想说a + b + c = 2。 底层的求解器 Simplex 通常做得很合理 使用这种编码。

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