Microsoft Z3 获得相关作业答案

【问题标题】：Microsoft Z3 get relevant assignmentsMicrosoft Z3 获得相关作业
【发布时间】：2020-06-18 03:23:51
【问题描述】：

如何仅获取 z3 可满足性检查后使用的变量的相关赋值？

例如：

我有多个断言作为 Z3 Sat Solver 的约束，而我需要检查一个布尔表达式是否满足。

Note: The assertion may contain variables which are not present/irrelevant in the Boolean Expression (Formula)

分配给模型的值也包含断言约束的分配，这对布尔表达式的可满足性没有影响。

我可以在模块 smt.relevance: 2 中看到 z3 配置中的默认值。
如何仅将其限制为对表达式可满足性有影响的变量？

【问题讨论】：

标签： java z3 smt sat

【解决方案1】：

一般来说，你不能这样做。 SAT 求解器将“启发式地”求解约束以找到令人满意的分配，通常，您无法控制搜索的进行方式。他们找不到任何类型的“最小的令人满意的任务”。

您可以将输出限制为仅包含公式中出现的变量，并查询末尾的变量值。如果你的公式中有一个变量的赋值与 SAT 无关，那么这种技术显然不会起作用，但它应该能让你走得更远。

【讨论】：

我同意@alias，只是忽略模型中的额外变量。 Z3 有时可以返回未为所有变量指定值的模型，但对此没有任何保证，显然它不会在您的用例中发生。如果您需要某种语义检查，您可以尝试翻转每个变量并询问 Z3 是否仍然满足公式，如果是，您知道该值是不相关的（但不能保证这会识别所有不相关的值） .
我曾想过尝试@Christoph 的建议，但是当我们翻转并放回变量时，变量的排列非常高，这似乎不是一种有效的方法。想知道是否有更好的方法来做到这一点？
这是一个不错的技巧，但不能避免指数搜索。考虑(p & q) -> r。如果将p 设置为False，则q 无关紧要。如果将q 设置为False，则p 无关紧要。这表明不仅没有任何“最小”的概念（p 和 q 可以是具有不可比较的元素集的任意公式），而且您也找不到引导搜索来引导您找到一些概念“最不相关的。” （在下一条评论中继续......）
（续）您始终可以使用每一步变量数量较少的公式，但也不能保证达到最小值。（但会是一个很好的启发式方法。）此外，这一切都假设 SAT 带有布尔值，如果您使用任意域上的变量进行常规 SMT，情况会更加复杂，