SMT算法基础

Question

我不是计算机科学专业的学生，对算法和命题逻辑没有很好的理解。但是，我在一个项目中确实使用了SMT求解器，我想了解算法是如何工作的？

我基本上有一个功能

f(x)=(p_0)x+(p_1)x^2+(p_2)x^3+...(p_n)^x^n

和一组方程，例如

f(x)>0

f(x)<1

f(x)+f'(x)f(x)<0.5

SMT求解器z3通过检验给定约束在一组数据样本上的可满足性来计算系数p_0,p_1...,p_n。

你能用非常简单的术语帮助我理解这到底是怎么发生的吗？它会搜索p的整个样本空间吗？

Answer 1

你可以认为SMT是一个光荣的搜索算法，但这将是极具误导性的:它要聪明得多，而且要复杂得多。特别是，它肯定不会像您所说的那样搜索整个示例空间。(想象一下: SMT求解器可以处理无界整数和reals:不可能穷尽地搜索这些整数和reals。)

不幸的是，这是一个过于宽泛的问题，无法在堆栈溢出的上下文中回答，但幸运的是，有许多优秀的参考资料值得您花时间阅读。以下是我最喜欢的两个：

• “决策过程”一书“http://www.decision-procedures.org/”是一本很好的读物，有许多参考资料可以帮助您进入文献。这本书告诉你所有的SMT算法-为不同的逻辑求解，甚至指导你，如果你有兴趣建立一个。
• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf是Leonardo和Nikolaj (z3的主要开发人员)的一篇优秀文章。它提供了一个很好的概述，如果您只对应用程序感兴趣，那么阅读起来就容易多了。

我建议从后者开始，并使用其中的参考资料来进一步研究您感兴趣的领域。有许多优秀的文章，教程，和一个友好的堆栈溢出社区，以帮助解决如果你被困！