是否有办法要求z3-Python中至少有k个满足的软约束？

Question

我知道您可以在z3py中添加软约束，然后请z3通过运行以下命令找到满足最大软约束数的模型：

s = Optimize()
s.add_soft(...)
...
s.add_soft(...)
s.check()

我的问题是，如果您希望z3返回至少满足k个软约束的任何模型，您可以做什么。我希望如果z3能够满足k约束，它将停止搜索并返回当前模型。

Answer 1

是。这些被称为k-out-N约束，也称为伪布尔约束.详情请参见K-out-of-N constraint in Z3Py。