在急切的 SMT 求解器中，SMT 公式被编码为可均衡满足的布尔公式，该公式被馈送到 SAT 求解器。通常，对于QF_UF公式，未解释的函数通过阿克曼约简或布莱恩特约简来约简，然后通过等式图方法构造一个可均衡满足的布尔公式。
所以我想知道是否有可能调用现有的 SMT 求解器来获得给定QF_UF公式的均衡布尔公式，而无需破解求解器的低级实现。例如，Z3 有一些转换输入问题的策略(例如tseitin-cnf和elim-term-ite(，有没有这种翻译的策略？
在 z3 中，您可以使用类似 https://gist.github.com/nunoplopes/8cd9fb433b2663c99cb34c8a95ae812f 的补丁转储 DIMACS
您还可以使用位爆炸策略来获取 SAT 公式，该公式将超过布尔 Z3 变量。我不认为这保证是CNF或NNF或任何形式。