编码“at-most-k/at-least-k 布尔值为真"；Z3 中的约束 [英] Encoding "at-most-k / at-least-k booleans are true" constraints in Z3

问题描述

在 Z3 中对任意 k 和布尔变量的数量?

What's a good way to encode "at least k / at most k of these boolean variables must be true" constraints in Z3, for arbitrary k and number of boolean variables?

我正在考虑通过引入新的 PB 变量(使用 此编码)，通过双条件将它们与我的布尔变量相关联(例如 x == true iff y == 1)，并断言它们的总和大于或等于 k.这是一种合理的方法，还是我应该使用更简单/更有效的编码?

I'm thinking of casting "at least k" as a pseudo-boolean problem by introducing new PB variables (using this encoding), relating them to my boolean variables through a biconditional (e.g. x == true iff y == 1), and asserting that their sum is greater than or equal to k. Is this a reasonable approach, or is there a simpler / more efficient encoding that I should use instead?

推荐答案

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

The easiest is to encode cardinality constraints using arithmetic. So if you want to say a + b + c <= 2, where a, b, c are Bool, then you can formulate it as (if a 1 0) + (if b 1 0) + (if c 1 0) >= 2. The underlying solver, Simplex, often does a very reasonable job with this encoding.

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

There are many other way to deal with cardinality constraints. One is to compile cardinality constraints into "sorting circuits", and there is quite developed methods in this end. A future version of Z3 will have direct support for cardinality constraints, and more generally pseudo-Boolean inequalities. If you have many cardinality constraints and feel very adventurous you are welcome to try out the "opt" branch where this is being developed. It uses dedicated format for pseudo-Boolean inequalities and it also include a mode where it detects "(if a 1 0) + (if b 1 0) + (if c 1 0) >= 2" inequalities as PB inequalities. That said, I would first try the very simple encoding and see how the simplex-based engine works for your domain.

这篇关于编码“at-most-k/at-least-k 布尔值为真"；Z3 中的约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！