| 标题 | 布尔可满足性问题研究综述 |
| 范文 | 郭莹 摘要摘要：布尔可满足性（简称SAT）问题是研究最广泛的NP-完全（简称NPC）问题之一。编码、预处理和求解算法是SAT问题求解的3个关键技术，近年来涌现了大量成果。SAT问题广泛应用在生产和生活中， SAT求解技术的健壮性和综合性能迫切需要进一步提升。从SAT问题分类、SAT问题应用领域、研究现状及面临的挑战等方面对相关研究成果进行梳理。 关键词关键词：SAT问题；NP完全问题；编码；预处理；求解算法 DOIDOI：10.11907/rjdk.162699 中图分类号：TP301 文献标识码：A文章编号文章编号：16727800（2017）005020403 0引言 布尔可满足性问题（Boolean Satisfiability Problem，简称SAT问题）是一个著名的判定问题[1]，不仅在数理逻辑和计算理论等方面有着举足轻重的研究地位，而且在实际生产领域具有很高的应用价值。本文从SAT问题求解的研究背景、意义和基本概念出发，在分析国内外研究现状基础上，介绍了SAT问题3大求解关键技术：编码、预处理和求解算法；对SAT问题求解面临的挑战进行了论述。 1SAT问题 SAT问题的基本形式指给定一个命题变量集合X和一个X上的合取范式φ（X），判断是否存在一个真值赋值t（X），使得φ（X）为真。如果能找到，则称φ（X）是可满足的（satisfiable），否则称φ（X）是不可满足的（unsatisfiable）。SAT问题的模型发现形式指当φ（X）可满足时，给出使公式φ（X）可满足的一组赋值。 本文参照SAT国际竞赛组别[2]，按照问题产生来源将SAT问题实例划分为应用类（Application）、组合类（Hard combination）和随机类（Random）。 2SAT问题应用领域 SAT问题是世界上第一个被证明的NPC问题[3]。SAT问题在计算机科学、复杂性理论、密码系统、人工智能等领域发挥着至关重要的作用。然而，促使SAT问题成为持续研究热点的主要原因在于其在现实应用中的重要性。许多包含数以万计变量和数百万约束的组合问题都可运用SAT求解技术处理。SAT求解器作为核心搜索引擎应用广泛，文献[4]对此进行了介绍，下面列出一部分应用。 （1）数学领域：数学密码、判定图和子图同构、寻找图生成树、自动机同态、欧拉回路、布尔函数的函数依赖识别、旅行商、图着色等问题。 （2）人工智能领域：知识编译、规划问题、机器识别、弹道轨迹、任务计划、神经网络计算、自动推理、DNA智能可编程片段生成等问题。SAT求解技术是人工智能的核心技术。 （3）计算机科学领域：约束满足问题、难组合类问题、N皇后问题、工作流可满足性问题、护理调度问题、扩展推理、真值维护、定理证明、数据库检索与维护、数据挖掘、AES密钥调度、语义信息处理等。 （4）计算机辅助设计与制造领域：软件模型检查、硬件模型检测、计算机系统结构设计、VLSI集成电路设计与验证、错误诊断、有限状态系统的模型检测、FGPA路由、逻辑合成的技术映射、图像解释、寄存器分配、时序问题等。 （5）生物信息领域：单模标本推理、系谱一致性检查等。 SAT问题越来越多地应用到生产和生活中，迫切需要提升当前SAT求解技术的健壮性和综合性能[5]。 3SAT问题研究成果 自1960年Davis和Putnam提出DP算法[6]以来，SAT求解研究逐步受到关注。然而1971年Cook证明SAT问题是NPC之后，人们对SAT的重视程度减弱。后来人们对SAT问题有了新的认识。自1991年起，世界各国研究机构纷纷举办SAT竞赛，众多学者的研究热情空前高涨，SAT算法及其实现程序的求解效率大幅提高，SAT问题逐渐在许多实际应用中显现出强大的作用。SAT协会是目前推动SAT问题理论和应用进展的主要驱动力量，其Satlive网站[7]随时更新SAT研究动态，发布了一系列有关会议、竞赛、技术报告、论文、图书等信息；每年举办一次SAT理论和应用国际学术会议，目前已召开16届； SAT国际竞赛始于2002年，每隔两年或一年举办，2016年成功举行了第10届，汇聚了大批优秀的SAT求解器，影响力很大。 3.1SAT问题编码方法 实际生产中的NP难题可以转化为SAT问题进行求解，因此，首先要进行规约和编码，目前SAT问题编码多采用CNF形式。DIMACS [8]作为标准格式广泛用于CNF布尔公式，也被历届SAT国际竞赛采用。DIMACS文件用字符“c”引导的注释文字行开始。紧接注释之后的一行“p cnf 实际上，對于同一个实例，即使使用同一个求解器，不同编码方法转换成的SAT问题求解效率是不一样的，SAT编码方法是研究热点之一。 3.2SAT问题预处理技术 最近几年的SAT国际竞赛结果证明，预处理技术对SAT求解器性能至关重要。早期的预处理技术使用原始DPLL[9]（DavisPutnamLogemannLoveland，简称DPLL）提出的单元传播和纯文字规则，后来发展了一些更复杂的技术如超二元解析、单元子句和探针等。近年来预处理技术出现了大量优秀成果，如Eén 等人首次解决了化简问题的规模性和复杂性，Marijn Heule等人提出和分析了子句消除化简规则，Tomas Balyo等人扩展了阻塞子句消除化简规则，Manthey提出CP3以模块化的方式将诸多预处理技术集成到SAT求解器中，等等。 3.3SAT问题求解算法 目前典型的SAT求解算法包括确定性算法和随机搜索算法两大类。确定性算法采取穷举和回溯思想，从理论上保证给定命题公式的可满足性，并在实例无解的情况下给出完备证明，但不适用于求解大规模的SAT问题。随机搜索算法主要基于局部搜索思想，绝大多数随机搜索算法不能判断SAT问题的不可满足性，但由于采用了启发式策略来指导搜索，在处理可满足的大规模随机类问题时，往往能比确定性算法更快得到一个解。 3.3.1确定性SAT求解算法 当前流行的确定性SAT求解算法几乎都是由基于深度优先搜索的DPLL[9]算法衍生而来的，冲突驱动子句学习（Conflict Driven Clause Learning，简称CDCL）[10]算法主要框架基于DPLL，是目前最重要的SAT求解算法，在冲突分析与子句学习、非时序回溯、重启、数据结构等方面作了一系列改进。 冲突分析和子句学习方面，GRASP算法在DPLL基础上引入冲突学习策略CDCL，Holldobler[11]进一步扩展并提出了通用的CDCL形式化描述；非时序回溯方面，一些新的智能启发式被先后引入到求解算法中，进一步减小了问题规模和搜索空间；重启策略方面，Wu研究了随机化问题和重启策略，Huang分析了基于子句学习效率的重启效果， Haim等人则认为相比一组相对固定的回溯间隔，应更加频繁进行重启；数据结构方面，出现了双观察文字、改进存储访问模式等新技术。 当前代表性的CDCL求解器包括Chaff、MiniSAT[12]、Lingeling[13]、Glucose[14]、Sparrow[15]等。其中Moskewicz等人提出的Chaff算法集合了laziness、线性学习和一系列启发式策略，强调“快速和低廉”的低负荷决策方法，是SAT求解算法的重要突破，形成流行求解器的相关思想。Lingeling、Glucose、Sparrow等近年来在SAT国际竞赛中屡获佳绩。 3.3.2随机搜索SAT求解算法 随机搜索SAT求解算法主要基于局部搜索思想。随机局部搜索（Stochastic Local Search，简称SLS）算法是最早提出的随机搜索SAT求解算法。Selman等人提出了基于SLS思想的贪心局部搜索法GSAT，之后又针对局部最优提出了框架性的WalkSAT。近年来，SLS算法研究取得了新进展，如避免重复翻转的方法[16]、工程随机搜索算法[17]、双重配置检查方法等。 研究人员开辟了利用进化算法（Evolutionary Algorithms，简称EA）求解SAT问题的新途径。例如早期用于求解SAT问题的EA算法包括遗传算法、拟物拟人算法Solar、禁忌搜索算法、量子免疫克隆算法、粒子群算法、量子算法、组织进化算法等，近年来一些新的SAT求解算法如人工蜂群算法[18]、模拟DNA算法[19]等。 4SAT求解面临的挑战 求解SAT问题的目标是作出正确有效的判定，这可能需要指数级运行时间。在追求越来越快且有效执行的求解方法时，不可避免会遇到一些错误[20]。一些SAT求解技术过于复杂，且需要大量的专业知识去理解概念的正确性，以及如何有效运行。尽管现有的SAT求解方法已经取得巨大成功，但仍有一些问题没有得到高效解决，已经解决的问题可能还存在更好求解方法。一些高效求解器忽視了算法的正确性和完备性，因此研究并实现高效率的求解方法仍是当前要解决的中心问题[21]。未来研究主要包括编码、预处理、确定性算法、随机类算法、求解器实现、并行求解等问题。 参考文献参考文献： [1]BALINT A， BELOV A， JARVISALO M， et al. Overview and analysis of the SAT challenge 2012 solver competition[J]. Artificial Intelligence， 2015（223）： 120155. [2]KUMAR T K S， NGUYEN D T， YEOH W， et al. A simple polynomialtime randomized distributed algorithm for connected row convex constraints[C].TwentyEighth AAAI Conference on Artificial Intelligence，2014. [3]COOK S A. The complexity of theorem proving procedures[C].Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing， New York， 1971：151158. [4]VARDI M Y. Boolean satisfiability：theory and engineering[J].Commun.ACM，2014，57（3）： 56. [5]SAT COMPETITION.Description of the Tracks[EB/OL].http：//satcompetition.org/2014 /description.shtml， 2014. [6]DAVIS M， PUTNAM H. A computing procedure for quantification theory[J]. Journal of the ACM （JACM）， 1960， 7（3）： 201215. [7]SAT ASSOCIATION. SAT live [EB/OL].http：//www.satlive.org/， 2015. [8]CHALLENGE D I M A C S. Satisfiability：suggested format[J].DIMACS Challenge， DIMACS， 1993（6）：2529. [9]DAVIS M， LOGEMANN G， LOVELAND D. A machine program for theoremproving[J].Communications of the ACM，1962，5（7）：394397. [10]EEN N， SORENSSON N. An extensible SATsolver[C]. Theory and applications of satisfiability testing，Springer Berlin Heidelberg， 2004：502518. [11]HOLLDOBLER S， MANTHEY N， PHILIPP T， et al. Generic CDCLA formalization of modern propositional satisfiability solvers[C].Young Scientists' International Workshop on Trends in Information Processing， 2014： 2534. [12]CHEN J. MiniSAT blbd[C].Proceedings of SAT Competition 2014： Solver and Benchmark Descriptions， 2014： 45. [13]BIERE A. Yet another local search solver and Lingeling and friends entering the SAT Competition 2014[C]. SAT Competition， 2014： 3940. [14]BELOV A， DIEPOLD D， HEULE M J H， et al. Glucose in the SAT 2014 Competition[C].SAT competition，2014：3132. [15]BALINT A， MANTHEY N. SparrowToRiss[C].SAT Competition，2014： 7778. [16]DUONG T T， PHAM D N， SATTAR A. A method to avoid duplicative flipping in local search for SAT[M].Advances in Artificial Intelligence， Springer Berlin Heidelberg， 2012：218229. [17]BALINT A. Engineering stochastic local search for the satisfiability problem[C].Universitat Ulm：Fakultat für Ingenieurwissenschaften und Informatik， 2014. [18]郭瑩， 张长胜，张斌.一种求解 SAT 问题的人工蜂群算法[J].东北大学学报：自然科学版， 2014， 35（1）：2932. [19]DAI P， ZHOU K， WEI Z， et al. Simulation DNA algorithm[M].BioInspired ComputingTheories and Applications， Springer Berlin Heidelberg， 2014： 8387. [20]WETZLER N D. Efficient， mechanicallyverified validation of satisfiability solvers[D]. Wichita St Austin：the University of Texas At Austin， 2015. [21]BALINT A， BELOV A， JARVISALO M， et al. Overview and analysis of the SAT challenge 2012 solver competition[J]. Artificial Intelligence， 2015（223）： 120155. 责任编辑（责任编辑：杜能钢） |
| 随便看 |
|
科学优质学术资源、百科知识分享平台，免费提供知识科普、生活经验分享、中外学术论文、各类范文、学术文献、教学资料、学术期刊、会议、报纸、杂志、工具书等各类资源检索、在线阅读和软件app下载服务。