对于任意k和布尔变量的数量,在Z3中编码"至少k /最多k个这些布尔变量必须为真"的约束是什么？
我想通过引入新的PB变量(使用这种编码)将"至少k "作为伪布尔问题,通过双条件(例如)将它们与我的布尔变量相关联,并声明它们的总和大于或者等于k.这是一种合理的方法,还是我应该使用更简单/更有效的编码？x == true iff y == 1
最简单的方法是使用算术编码基数约束.因此,如果你想说a + b + c <= 2,其中a,b,c是Bool,那么你可以将其表示为(如果是1 0)+(如果b 1 0)+(如果c 1 0) > = 2.底层求解器Simplex通常使用此编码做一个非常合理的工作.
还有许多其他方法可以处理基数约束.一种是将基数约束编译成"排序电路",并且在这方面有相当发达的方法.未来版本的Z3将直接支持基数约束,更普遍的是伪布尔不等式.如果您有许多基数限制并且非常喜欢冒险,欢迎您试用正在开发的"opt"分支.它使用伪布尔不等式的专用格式,它还包括一种模式,它检测"(如果a 1 0)+(如果b 1 0)+(如果c 1 0)> = 2"不等式作为PB不等式.也就是说,我首先尝试非常简单的编码,看看基于Simplex的引擎如何适用于您的域.