非线性公式的可满足性问题不仅是理论研究的热点，也是程序验证中的一个核心问题。本报告专注于介绍无量词非线性公式的求解方法，包括利用多项式的弦结构优化圆柱代数分解（CAD）的投影序列，通过单胞腔投影操作符更有效地与冲突驱动的子句学习（CDCL）策略结合，以及使用局部搜索算法快速寻找解。报告最后还将介绍求解超越方程和混合三角多项式的方法。