SAT求解器快速入门

Posted 2020-11-27 yuweng1689

从事组合优化或信息安全方向的研究人员，基于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互相结合的求解器）