|
|
| FCS|前沿研究：一种基于公式结构信息的可满足性问题求解算法 |
|
论文标题：An algorithm for solving satisfiability problembased on the structural information of formulas
期刊：Frontiers of Computer Science
作者：Zaijun ZHANG, Daoyun XU, Jincheng ZHOU
DOI：10.1007/s11704-021-0318-8
微信链接：点击此处阅读微信文章
原文信息
• 标 题：
An algorithm for solving satisfiability problembased on the structural information of formulas
• 原文链接：
https://journal.hep.com.cn/fcs/EN/10.1007/s11704-021-0318-8
• 引用格式：
Zaijun ZHANG, Daoyun XU, Jincheng ZHOU. An algorithm for solving satisfiability problem based on the structural information of formulas. Front. Comput. Sci., 2021, 15(6): 156405
公众号推文链接：一种基于公式结构信息的可满足性问题求解算法
01导读
面向的问题
命题可满足性（SAT）问题是理论计算机科学中一个重要的NP-hard问题。为了高效地求解SAT问题，研究人员开展了大量的研究工作。现有SAT问题的求解算法主要分为两大类：完备求解算法和局部搜索求解算法。从实验上来看，SAT的完备求解算法在工业实例上表现出出色的性能，而SAT的局部搜索求解算法在随机实例上表现出较好的效果。目前性能出色的SAT局部搜索求解算法往往采用了随机游走技术，如CCASat和Sparrow2011。由于随机游走策略的不确定性是限制局部搜索求解算法的主要因素，所以这也很大程度地制约了SAT局部搜索求解算法的整体性能。
本文提出了一种基于命题公式的变量图结构信息的SAT局部搜索算法，进而有效地避免了随机游走技术所带来的不确定性。特别地，在给定命题公式的变量图中，所设计的求解算法使用节点的结构熵来生成初始赋值。当求解算法陷入局部最优时，不同于以往方法随机选择一个不可满足子句，本文将根据不可满足子句的权重或结构信息来选择最优或次优的不可满足子句。
02技术细节
给定一个命题公式
，变量集合
，V（c）表示子句c中的变量集合，C（x）表示包含变量x的子句C，V（F）表示命题公式F中出现的所有变量，N（x）表示变量x的所有邻居变量。其中，两个变量至少出现在同一个子句中，那么这两个变量互为邻居。
定义1：命题公式F的变量图定义为G=（V,E）,其中顶点集合V=V（F），E={（x，y）|x与y在F中互为邻居}。
定义2：节点i的结构熵定义为
，其中
。
定义3：给定一个命题公式F和相应的变量图G=（V,E）,对于任意一个子句c，我们定义子句c的一维结构信息为
，而变量图的一维结构信息维为
。
本文主要从两个方面改进SAT的局部搜索算法：生成初始解和选择最优的不可满足子句。
首先，利用命题公式F的变量图中节点的结构熵来生成初始赋值。算法1详细描述了具体的实现过程。在算法1中，set（c）是关于子句c的标记函数。set（c）>0表示c是可满足子句，否则c是不满足子句。函数pos（x）和neg（x）分别表示变量x出现的正文字个数和负文字个数。s是初始解，对于∀x∈V（F），有s（x）∈{0,1}。
当局部搜索算法陷入局部最优时，为了选择一个最优的不可满足子句，以前的局部搜索算法通常采用选取一个不可满足子句并进行随机扰动操作，而本文将根据子句的权值和结构信息来选择一个不可满足子句。本文使用Uc表示不可满足子句集合，Ucmax和Ucmin分别表示权重最大、结构信息最小的不满足子句的集合。为了跳出局部最优，本文倾向于选择权重最大的不可满足子句（即在Ucmax中的这些子句），然后在其中再选择最有希望的变量进行翻转。
然而，对于大规模SAT实例，当局部搜索算法第一次或者前几次陷入局部最优时，求解算法会产生大量的不可满足子句。在这些不可满足子句中，存在大量的子句具有相同的权值。在这种情况下，本文倾向选择一些结构信息最小的不可满足子句（即在Ucmin中的这些子句），然后在其中再选择最有希望的变量进行翻转。
当局部搜索算法遇到局部最优时，本文使用参数Oc来控制最优不可满足子句的选择。如果不满足的子句总数大于Oc（即|Uc|>Oc），则选择结构信息最小的子句作为最优子句。否则，选择权重最大的子句作为最优子句。
03主要贡献
本文的主要贡献如下：
1）一种生成初始候选解的策略，该策略是基于命题公式变量图中节点的结构熵，而不是使用传统的随机游走策略。
2）一种跳出局部最优的不可满足子句选择策略，该策略是基于子句的权重和结构信息。
3）所提出的策略融入到CCASat和Sparrow2011这两个求解算法中，表现出出色的性能。
04实验结果的简单总结
本文提出了一种基于命题公式结构信息的SAT局部搜索算法。实验结果表明了所提出的策略是有效的，并可以进一步提高基于随机游走策略的局部搜索求解算法的性能。
05与其他相关研究的对比
本文评估所提出策略在随机3-SAT实例上的性能。将所提出的策略融入到CCASat和Sparrow2011中，产生了两个新的求解算法SICCASat和SISparrow2011。实验在windows10系统上进行，运行内存为8.00g，处理器为Intel（R） Core（TM） i5-10210uCPU @1.60hz 2.11ghz。选取2009年和2011年SAT竞赛的实例来测试所提出策略的有效性。参数Oc设置为子句数的0.85倍。对于求解算法中其他的参数，本文保留其原始设置。本文使用ins_class来表示实例类，num表示每个实例类中实例的个数，avg_time和suc分别表示每个实例类的平均运行时间和成功率。
表1列出了所提出策略的实验结果。可以看出，融合所提出策略的求解算法整体性能明显优于原始求解算法。特别是，SISparrow2011求解算法与其他求解算法相比，表现出了强大的性能。此外，所提出的搜索策略也可以应用到其他基于随机游走技术的SAT局部搜索算法中。
解读：王艺源 东北师范大学
审核：张琨 合肥工业大学
Frontiers of Computer Science
Frontiers of Computer Science （FCS）是由教育部主管、高等教育出版社和北京航空航天大学共同主办、SpringerNature 公司海外发行的英文学术期刊。本刊于 2007 年创刊，双月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为周志华教授，共同主编为熊璋教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”；入选“中国科技期刊卓越行动计划项目”。
《前沿》系列英文学术期刊
由教育部主管、高等教育出版社主办的《前沿》（Frontiers）系列英文学术期刊，于2006年正式创刊，以网络版和印刷版向全球发行。系列期刊包括基础科学、 、工程技术和人文社会科学四个主题，是我国覆盖学科最广泛的英文学术期刊群，其中13种被SCI收录，其他也被A&HCI、Ei、MEDLINE或相应学科国际权威检索系统收录，具有一定的国际学术影响力。系列期刊采用在线优先出版方式，保证文章以最快速度发表。
中国学术前沿期刊网
http://journal.hep.com.cn
特别声明：本文转载仅仅是出于传播信息的需要，并不意味着代表本网站观点或证实其内容的真实性；如其他媒体、网站或个人从本网站转载使用，须保留本网站注明的“来源”，并自负版权等法律责任；作者如果不希望被转载或者联系转载稿费等事宜，请与我们接洽。
