对于任意k和任意数量的布尔变量，在Z3中编码“至少k个/最多k个布尔变量必须为真”约束的好方法是什么？
我正在考虑通过引入新的PB变量（使用此编码），通过双条件（例如）将它们与我的布尔变量相关联，并断言它们的总和大于或，将“至少k ”转换为伪布尔问题。等于k。这是一种合理的方法，还是我应该使用更简单/更有效的编码？x == true iff y == 1
最简单的方法是使用算术编码基数约束。因此，如果您想说a + b + c <= 2，其中a，b，c是布尔，那么您可以将其表示为（如果a 1 0）+（如果b 1 0）+（如果c 1 0） > =2。基础求解器Simplex通常使用此编码做非常合理的工作。
还有许多其他方法来处理基数约束。一种是将基数约束编译为“排序电路”，并且为此目的，已经开发了很多方法。Z3的未来版本将直接支持基数约束，更普遍的是伪布尔不等式。如果您有很多基数约束并且非常喜欢冒险，欢迎尝试在开发此代码的“ opt”分支中进行尝试。它对伪布尔不等式使用专用格式，并且还包括一种模式，该模式将“（如果a 1 0）+（如果b 1 0）+（如果c 1 0）> = 2”不等检测为PB不等式。也就是说，我将首先尝试非常简单的编码，然后看看基于单纯形的引擎如何在您的域中工作。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句