我不是计算机科学专业的学生，对算法或命题逻辑没有很好的了解。但是，我确实在项目中使用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的整个样本空间吗？
您可以将SMT视为一种光荣的搜索算法，但这极为误导：它比这更聪明，更复杂。特别是，正如您所说的那样，它肯定确实搜索整个样本空间。（想象一下：SMT求解器可以处理无限的整数和真实：不可能详尽地搜索它们。）
不幸的是，这是一个在堆栈跨流的背景下要回答的问题，但是幸运的是，有许多出色的参考文献值得花时间和阅读。这是我最喜欢的两个：
-
"决策过程"书http://www.decision-procedures.org/是一本很棒的阅读，并且有许多参考可以帮助您指导文献。这本书告诉您有关SMT-Solvers中用于不同逻辑的算法的所有信息，甚至如果您有兴趣建造一个逻辑。
-
http://citeseerx.ist.psu.edu.edu/viewdoc/download?doi=10.1.1.1.367.9961＆amp;rep=rep=rep=rep=rep = rep; type = pdf是Leonardo and Nikolaj（Z3的主要开发者））。它提供了一个很好的概述，如果您只对应用程序感兴趣，就可以轻松阅读。
我建议从后者开始，然后使用其中的参考文献以您的利益进一步研究领域。有许多出色的文章，教程和一个友好的堆栈跨流社区，可以帮助您！