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

问题描述

一个例子：

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,p3>0))，设置较少的变量）是有价值的。

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

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

解决方法

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

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

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