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

【问题标题】：Is it possible to get the equisatisfiable boolean formula of a QF_UF formula using existing SMT solvers?是否可以使用现有的 SMT 求解器获得 QF_UF 公式的等值布尔公式？
【发布时间】：2017-07-13 07:07:58
【问题描述】：

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

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

【问题讨论】：

标签： z3 smt satisfiability

【解决方案1】：

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

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

【讨论】：

我稍后会尝试第一个解决方案。对于第二个，当我尝试将bit-blast 策略应用于 QF_UF 问题 (link) 时，输出仍然是 QF_UF 问题。是我做错了什么还是bit-blast策略只支持BV问题？
啊，是的。您需要首先摆脱 UF 符号。现在有一种阿克曼化策略。名称是 ackermannize_bv IIRC。
非常感谢。现在 UF 符号减少了。但我发现bit-blast 仍然无法将 QF_UF 问题转换为 SAT 公式（example）。那么是否有任何工作策略可以将没有未解释的非零元函数的 QF_UF 公式转换为 SAT 公式？谢谢！
SAT 公式是什么意思？如果你想要 DIMACS，你需要使用我提供的补丁；我不认为该功能已暴露。
如果你想要 CNF 或 NNF，也有相应的策略。