我不是计算机科学专业的学生，对算法或命题逻辑没有很好的理解。但是，我确实在项目中使用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求解器可以处理无界的整数和实数：无法彻底搜索这些整数。）
不幸的是，在堆栈溢出的情况下，这个问题太过宽泛，但你很幸运，有许多优秀的参考资料非常值得花时间和阅读。这是我最喜欢的两个：
我建议从后者开始，并使用其中的参考资料根据您的兴趣进一步研究该领域。有许多优秀的文章，教程和友好的堆栈溢出社区可以帮助您解决问题！