【发布时间】：2018-07-19 21:53:14
【问题描述】：
我刚刚了解了与 SMT 求解器相关的 DPLL(T) 和 DPLL algorithm。我在一些地方也看到过关于 SMT 求解器的引用 z3。
想知道 z3 在其算法中使用什么来实现 SMT 求解。如果是 DPLL 算法、变体、自定义的东西、一堆东西等等。希望了解现代 SMT 求解器使用的不同类型的算法。
【问题讨论】：
标签： algorithm z3 solver smt sat
【发布时间】：2018-07-19 21:53:14
【问题描述】：
SMT 求解器来自基于计算机的定理证明社区和传统数学逻辑中的自动推理的长期研究。在堆栈溢出答案中总结所有算法/研究是不可能的。但是，http://www.decision-procedures.org/ 这本书是一本极好的读物，并且有许多参考资料可以帮助您指导文献。 （第一版已经有 10 年的历史了，但我现在看到他们在 2016 年推出了第二版。）
【讨论】：
-
非常感谢，这就是我所需要的。 :)