在 Z3 求解器中使用封闭世界假设求解约束

Question

我正在使用 Python 中的 Z3 Solver 来解决约束满足问题，我需要解决以下形式的约束：

ForAll([x, y], Implies(And(situation(x), situation(y)), And(actions(x), actions(y))))

给定一组事实，例如：

situation(x) == True

我想应用封闭世界假设，这意味着如果不知道某件事是真的，那么它应该被认为是假的，以找到满足给定事实和约束的唯一可能的解决方案。我的目标是在不引入超出严格规定的额外信息或假设的情况下做到这一点。

我目前不确定如何在Z3中有效地实现封闭世界假设以相应地限制解决方案空间。有没有办法直接指示 Z3 在封闭世界假设下运行，或者我需要在约束中显式地对该假设进行建模？任何有关如何使用 Z3 实现此目的的指示或示例将不胜感激。

最初，我尝试手动将所有未声明为 True 的内容指定为 False，但事实证明这种方法对于我的目的而言过于详尽且不切实际。它显着增加了问题的复杂性和规模，而没有有效利用 Z3 的功能。

Answer 1

SMT 求解器不会做出封闭世界假设。只要他们找到满足您提出的约束条件的模型，他们就会做出回应

sat

。对于任何未明确说明的内容，求解器可以自由选择对真值进行任意分配的解释。

没有自动“开关”来告诉 z3（或任何其他 SMT 求解器）合并封闭世界假设。由于其基于 DPLL 的架构，添加一个也不是一件容易的事。 （但也许这不是重点。）

您说从建模角度来看“手动添加”封闭世界假设的成本太高。我想知道是否可能存在一种不同的建模方式，使得不需要封闭世界假设。请记住，虽然类似 Prolog 的系统本质上是原子和谓词，但 SMT 求解器提供了更丰富的世界：您可以拥有未解释的类型、枚举类型等，这可以让您无需封闭世界即可解决问题假设。

但是不可能以您所提出的一般性来回答您的问题。如果您能提出一个更简单的具体示例来说明您正在尝试执行的操作，甚至可能展示您将如何在 Prolog 中执行此操作，我们也许能够为您提供有关如何在 SMT 世界中对其进行建模的指导。

但是，长话短说，SMT 世界中不存在封闭世界假设。如果您想利用 SMT 求解器，则必须对问题进行建模，而无需这样做。