Z3Py中的K出N约束 [英] K-out-of-N constraint in Z3Py

问题描述

我正在为 Z3定理证明器(Z3Py)使用Python绑定.我有N个布尔变量x1，.. xN.我想表达一个约束，即其中N个中的K个应该正确.如何在Z3Py中做到这一点?有内置的支持吗?我检查了在线文档，但是 Z3Py文档没有提及为此的任何API.

I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,..,xN. I want to express the constraint that exactly K out of N of them should be true. How can I do that, in Z3Py? Is there any built-in support for that? I checked the online documentation, but the Z3Py docs don't have any mention of any API for that.

对于N分之一的约束，我知道我可以分别表示至少一个为真(断言Or(x1，..，xN))，至多一个为真(断言Not(And( xi，xj))对于所有i，j).我还知道其他方式，用于手动表示N中的1-out和K中的k-out- N个约束.但是，我的印象是，当求解器对这种约束有内置支持时，有时比手动表达它会更有效.

For one-out-of-N constraints, I know I can separately express that at least one is true (assert Or(x1,..,xN)) and that at most one is true (assert Not(And(xi,xj)) for all i,j). I also know of other ways to manually express the 1-out-of-N and K-out-of-N constraints. However I have the impression that when the solver has built-in support for this constraint, it can sometimes be more efficient than expressing it manually.

推荐答案

是的，Z3Py对此具有内置支持.有一个未记录的API，Z3Py文档中未提及:请使用PbEq.特别是表达式

Yes, Z3Py has built-in support for this. There is an undocumented API for this, that isn't mentioned in the Z3Py docs: use PbEq. In particular, the expression

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

如果N个布尔变量中的K个正好设置为true，则

将为true.有一些报告，该编码比手动表达约束的简单方法要快.

will be true if exactly K out of the N boolean variables are set to true. There are some reports that this encoding will be faster than naive ways of manually expressing the constraint.

要表达N分之一约束，只需设置K = 1并使用PbEq.要表示最多N个K约束，请使用PbLe.要表达至少N个K约束，请使用PbGe.

To express a 1-out-of-N constraint, just set K=1 and use PbEq. To express an at-most-K-out-of-N constraint, use PbLe. To express an at-least-K-out-of-N constraint, use PbGe.

您可以像这样在Python中表达这一点:

You can express this in Python like this:

import z3

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#Exactly 3 of the variables should be true
s.add( z3.PbEq([(x,1) for x in bvars], 3) )
s.check()
m = s.model()

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#<=3 of the variables should be true
s.add( z3.PbLe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#>=3 of the variables should be true
s.add( z3.PbGe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()

这篇关于Z3Py中的K出N约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！