上海交通大学严骏驰教授团队回顾了借助机器学习(ML)技术解决布尔可满足性问题(SAT)这一典型的NP 完全问题的最新文献。近十年来，机器学习社区发展迅速，在多项任务中的表现都超过了人类。这一趋势也启发了大量应用机器学习方法解决SAT问题的研究。本综述将研究借助机器学习技术解决SAT问题的(ML-SAT)求解器及其发展历程，从带有手工特征的朴素分类器到新兴的端到端SAT问题求解器，以及将较为成熟的冲突驱动子句学习(CDCL)求解器和局部搜索求解器与机器学习方法相结合的最新进展。总之，利用机器学习求解布尔可满足性问题是一个前景广阔但又充满挑战的研究课题。本文总结了现有工作的局限性，并提出了未来可能的发展方向。

相关文献列表请见：

https://github.com/Thinklab-SJTU

全文下载：

Machine Learning Methods in Solving the Boolean Satisfiability Problem

Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, Junchi Yan

https://www.mi-research.net/en/article/doi/10.1007/s11633-022-1396-2

https://link.springer.com/article/10.1007/s11633-022-1396-2

 全文导读

布尔可满足性问题(常被称为 SAT)是计算复杂性领域第一个被证明的 NP 完全问题。由于它的应用广泛，且可以规约为 SAT 的问题种类繁多，这个困难的组合问题一直吸引着研究人员的关注。就理论研究而言，许多组合问题都可以用命题公式表示，并通过运行 SAT 求解器来解决，例如图着色、顶点覆盖和团检测等问题。它还是自动定理证明的有用工具，其中一个典型案例就是凯勒猜想的解决。此外 SAT 求解还有很多工业应用，如电路设计中的有界模型检查、配置管理和等效性检查。它也是逻辑综合中的一个重要组成部分，许多 SAT 求解器都是专门为此任务而设计的。因此，SAT 求解不仅有重要的研究意义，还能帮助工业界实现更经济的工作流程。

由于P/NP问题仍未解决，研究人员对SAT问题的难度心怀敬畏，并努力设计高效的 SAT 求解器。与此同时，机器学习，尤其是方兴未艾的深度学习技术，已经被应用于组合优化领域，并催发了许多前景广阔的新研究方向。近年来，图匹配和混合整数规划等领域都得到了深入研究，SAT 领域也不例外。作为 SAT 求解器最前沿的赛事之一，在过去的 SAT 竞赛中，也出现了多个采用机器学习技术获奖的求解器，包括 Kissat_MAB(2021 年 SAT 竞赛排名第一)和 MapleCOMSPS(2016年SAT竞赛排名第一)。除了用机器学习技术辅助传统求解器外，NeuroSAT 等端到端框架也实现了机器学习与SAT求解的融合，从而实现自动推导，并节省人力。

此前有一些关于机器学习技术解决SAT和其他难题的研究。具体来说，Popescu等人关注的是范围更广的约束求解问题。在另一篇与本文相关的综述中，作者Holden回顾了解决 SAT 和带量词的 SAT(QSAT)的机器学习方法，尤其是用于自动定理证明的方法。作者根据机器学习与 SAT 求解的结合方式对所评述的方法进行了分类。基于这种分类方法，本综述报告讨论了机器学习与 SAT 求解结合的三种主要模式：1) 使用纯机器学习方法的独立 SAT 求解器；2)使用机器学习导向启发式方法替换现有冲突驱动子句学习(CDCL)求解器的某些关键组件；3)使用机器学习辅助模块修改局部搜索求解器。除了用机器学习方法解决 SAT 问题本身之外，本文还总结了用机器学习生成 SAT 实例的方法，这是该领域一个新兴且前景广阔的课题。与前述相关综述相比，本研究侧重于最新进展，并以更紧凑、更简洁的方式展开，以便读者能快速了解这一新兴领域。

本文包括借助机器学习技术，如多层感知器(MLP)、朴素贝叶斯和神经网络，以上述三种方式直接优化 SAT 求解。本文不涉及组合求解器和算法运行时间预测，因为它是一种适用于其他问题的通用技术(参见原文 Hutter 等人的综述)。SAT 的扩展问题，如最大可满足性问题(MAX-SAT)、可满足性模理论(SMT)和带量词的布尔表达式(QBF)也不在本文研究范围之内。

本文接下来的内容结构如下。第 2 节是前言部分，第 3 节讨论了基于机器学习的 SAT 求解的三种模式：第 3.1 节讨论了纯机器学习方法的独立 SAT 求解器，第 3.2 节讨论了使用机器学习组件增强的冲突驱动子句学习求解器，第 3.3 节讨论了机器学习辅助的局部搜索 SAT 求解器。第 4 节讨论了 SAT 实例生成的机器学习方法。最后第 5 节进行总结。图 1 是本研究的概览。

 图1 使用机器学习技术的 SAT 求解器概览

全文下载：

Machine Learning Methods in Solving the Boolean Satisfiability Problem

Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, Junchi Yan

https://www.mi-research.net/en/article/doi/10.1007/s11633-022-1396-2

https://link.springer.com/article/10.1007/s11633-022-1396-2

BibTex:

@Article{MIR-2022-07-212,
author = {Wenxuan Guo and Hui-Ling Zhen and Xijun Li and Wanqian Luo and Mingxuan Yuan and Yaohui Jin and Junchi Yan},
journal = {Machine Intelligence Research},
title = {Machine Learning Methods in Solving the Boolean Satisfiability Problem},
year = {2023},
volume = {20},
number = {5},
pages = {640-655},
doi = {10.1007/s11633-022-1396-2}
}

纸刊免费寄送

Machine Intelligence Research

MIR为所有读者提供免费寄送纸刊服务，如您对本篇文章感兴趣，请点击下方链接填写收件地址，编辑部将尽快为您免费寄送纸版全文！

说明：如遇特殊原因无法寄达的，将推迟邮寄时间，咨询电话010-82544737

收件信息登记：

https://www.wjx.cn‍/vm/eIyIAAI.aspx#  

∨关于Machine Intelligence Research

Machine Intelligence Research（简称MIR，原刊名International Journal of Automation and Computing）由中国科学院自动化研究所主办，于2022年正式出版。MIR立足国内、面向全球，着眼于服务国家战略需求，刊发机器智能领域最新原创研究性论文、综述、评论等，全面报道国际机器智能领域的基础理论和前沿创新研究成果，促进国际学术交流与学科发展，服务国家人工智能科技进步。期刊入选"中国科技期刊卓越行动计划"，已被ESCI、EI、Scopus、中国科技核心期刊、CSCD等数据库收录。