从事组合优化或信息安全方向的研究人员，基于SMT研究，需要快速学习SAT求解器的基本原理和方法。以下是快速入门的几点体会：
1.理清需要——是完备求解器还是不完备求解器
完备求解器 能给出SAT、UNSAT、unknow三种确定的答案，尤其是UNSAT结论能给出证明推导过程，指出导致矛盾的关键路径。
不完备求解器能给出SAT、unknow两种结论。SAT结论给出一组可满足解即完成求解任务。可能会存在其他一组或多组可满足解。如果问题本身不知一组解，那么不同的求解器得出的可满足解可能不同。
2.先进的完备求解器中以CDCL框架为主流。
基本算法框架：
最新比较经典的全面介绍minisat系列完备求解器的文献，本人推荐下面这篇文章作为掌握基本概念之后快速进阶。
Audemard, Simon - 2018 - On the Glucose SAT Solver
结合glucose4.0版本，认真解读代码，不断补充知识点，这样学习进步会很快。
3.不完备算法——随机局部搜索（SLS）
原理很简单：
入门求解器：probSAT, wailSAT, Score2SAT,YalSAT等
综合性较强的求解器：dimetheus，Sparrow2Riss-2018等
建议查阅文献：
中文文献——硕士论文：命题逻辑中随机3_SAT问题算法研究_安世勇；基于概率推理的SAT局部搜索算法_梅方元；
外文文献：Adrian Balint and Uwe Schoning，Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break。
4.两种求解器结合使用：CDCL+SLS
截止2019年11月，从2019年SAT竞赛发布的总结和求解器介绍，可以看出CDCL+SLS发挥各自优势是许多科研工作者研究的内容。简要列出来如下：
（截止2020-4-6本人了解到的SLS与CDCL互相结合的求解器）
原文地址：https://www.cnblogs.com/yuweng1689/p/12652346.html