如何使用 Z3 获得具有最小变量的模型以满足断言答案

【问题标题】：How to get the model with minimum variables to satisfy the assertion using Z3如何使用 Z3 获得具有最小变量的模型以满足断言
【发布时间】：2021-04-08 22:18:40
【问题描述】：

一个例子：

from z3 import *
p1,p2, p3 = Reals('p1 p2 p3')
s = Optimize()
s.add(And(Or(p1>=0, p2>0),Or(p1<=10,p3>0)))
print(s.check())
print(s.model())

运行代码，得到输出：

sat
[p3 = 1, p1 = 11, p2 = 1]

没错。但是，获得预期结果很有价值（满足约束And(Or(p1>=0, p2>0),Or(p1<=10,p3>0))，设置较少的变量。

例如，只设置 p1=0（或 range([0,10]) 中的任何值），则满足约束。只需设置一个变量。

所以我的问题是，有没有一种通用的方法来获得最少数量的必要变量？

【问题讨论】：

这能回答你的问题吗？ Do you know how to set "weak" initial values to each of z3 Array element?
谢谢。有帮助。我知道 Z3 Optimize 对象中有“add_soft”功能。但实际上约束逻辑由数百个变量组成，它们耦合在不同的子句中，例如： (p1>100) || ((p1
是的。也许我可以添加软原因并检查已解决的模型以获取哪些变量是冗余的。但是当涉及到耦合变量时，例如：p1,p2 = Reals('p1 p2') s = Optimize() s.add(And((p1>=100),Or(p1<=150,p2<0)))，如何设置软子句？
我已尝试编辑问题。希望我说清楚。谢谢。
哦，我看到变量不再是booleans，而是变成了Reals。这是一个与原始问题完全不同的问题。 AFAIK，这对于像 Z3 这样的普通 SMT/OMT 求解器来说是不可能的。

标签： z3 smt z3py

【解决方案1】：

您正在寻找的是所谓的“符号”模型，即，其中一些变量设置为常量，而其他变量可以设置为表达式。例如，如果您有类似x > y 的约束，那么符号模型可能是y = 0, x > y。不幸的是，SMT 求解器不提供这种“符号”模型。通常的 DPLL 样式约束传播不允许这种简单的符号模型构造。

这个领域的一个困难是，对于这样的最小模型可能是什么，没有“规范”的概念。（这个问题一般是不可判定的。）

如果您对此类模型感兴趣，最好的办法是使用更高级的工具（例如数学）或一般的定理证明器来提出此类模型。（当然，这些充其量是半自动化的。）基于 BDD 的求解器也可以提供符号模型，尽管大多数现代求解器使用 SAT 引擎和/或没有公开足够的 API 来查看其 BDD 引擎生成的模型。

【讨论】：

感谢别名。问题仅来自符号执行。对于某些特定的应用程序，我通过编程得到了解决方案。现在，我想找到一种处理更常见约束的通用方法，将约束赋予 Z3 并找到答案。所以这是我正在研究的问题。感谢@Patrick Trentin 和 Malte Schwerhoff 的所有讨论。到目前为止，我已经了解了这个问题的条件，我应该通过一些洞察力来解决它。似乎应该先尝试软约束。