z3 - 是否可以使用现有的 SMT 求解器获得 QF_UF 公式的等值布尔公式？

Question

在急切的 SMT 求解器中，SMT 公式被编码为可等满足的布尔公式，该公式被馈送到 SAT 求解器。通常，对于 QF_UF 公式，未解释的函数通过 Ackermann 归约或 Bryant 归约进行归约，然后通过等式图方法构造一个等值的布尔公式。

所以我想知道是否可以调用现有的 SMT 求解器来获得给定 QF_UF 公式的等值布尔公式，而无需破解求解器的低级实现。比如 Z3 有一些转换输入问题的策略（比如tseitin-cnfand elim-term-ite），有没有这样的转换策略？

Answer 1

在 z3 中，您可以使用https://gist.github.com/nunoplopes/8cd9fb433b2663c99cb34c8a95ae812f之类的补丁转储 DIMACS

您还可以使用 bit-blast 策略来获得 SAT 公式，该公式将超过布尔 Z3 变量。我认为这不能保证是 CNF 或 NNF 或任何形式。