Ограничение K-out-of-N в Z3Py

Question

Я использую привязки Python для доказательства теоремы Z3 (Z3Py). У меня есть N булевых переменных, x1,..,xN. Я хочу выразить ограничение, что именно K из N должно быть истинным. Как я могу это сделать в Z3Py? Есть ли встроенная поддержка для этого? Я проверил онлайн-документацию, но в документации Z3Py не упоминается ни об одном API для этого.

Для ограничений "один из N" я знаю, что могу отдельно выразить, что по крайней мере одно из них является истинным (утверждать Or(x1,..,xN)), и что самое большее одно из них является истинным (утверждать Not(And(xi,xj))) для всех я,j). Я также знаю о других способах ручного выражения ограничений 1-из-N и K-из-N. Однако у меня сложилось впечатление, что, когда решатель имеет встроенную поддержку этого ограничения, иногда это может быть более эффективным, чем выражение его вручную.

Answer 1

Да, Z3Py имеет встроенную поддержку для этого. Для этого есть недокументированный API, который не упоминается в документации по Z3Py: PbEq, В частности, выражение

PbEq(((x1,1),(x2,1),..,(xN,1)),K)

будет истинным, если точно K из N булевых переменных установлены в true. Есть некоторые сообщения, что эта кодировка будет быстрее, чем наивные способы ручного выражения ограничения.

Чтобы выразить ограничение 1 из N, просто установите K=1 и используйте PbEq, Чтобы выразить ограничение не более K-out-of-N, используйте PbLe, Чтобы выразить ограничение по крайней мере K-out-of-N, используйте PbGe,