z3 - 简化 CNF 公式，同时保留某些变量的所有解决方案

Question

相关:CNF simplification (实际上，我认为该问题的提交者可能已经在寻找我想要的)

存在许多用于简化(或求解前“预处理”)DIMACS 格式 CNF 公式的工具，大多数 SAT 求解器都包含一些工具。然而，我所知道的一切都是将一个平凡可满足的公式简化为一个具有零个或一个变量的平凡可满足的 CNF，即它们只试图保持公式的可满足性。我至少尝试过 SatELite 和 cryptominisat 的预处理模式。

然而，对于构建一个大问题的 CNF，在我看来，一次简化问题的一个明确定义的子集是非常有用的，然后在最终的过程中可能会重复多次CNF 在这些子公式中的某些变量之间具有附加约束。

那么，是否存在任何工具，或者普通的 SAT 求解器(或其他求解器，如 Z3，我正在使用它来生成我想最小化的 CNF)是否可以以某种巧妙的方式使用，以简化 CNF 公式，同时保留一组给定变量的所有解决方案？

Answer 1

Coprocessor SAT 预处理器可以做你想做的事。它可以被赋予一个可选的变量范围，并且只会在该范围内应用等价保留简化。在该范围之外，它将应用更强的、可满足性保持的简化。至少在版本 2 中是这样。