基于子句的动态检查强制文字的SAT求解器

计算机工程与科学

基于子句的动态检查强制文字的SAT求解器

常文静1,2，徐扬2

（1.西南交通大学信息科学与技术学院，四川成都 610036;

2.西南交通大学系统可信性自动验证国家地方联合工程实验室,四川成都 610036）

收稿日期:2017-12-25 修回日期:2018-04-11 出版日期:2019-02-25 发布日期:2019-02-25
基金资助:
国家自然科学基金（61673320）；中央高校基本科研业务费（2682017ZT12）

A clause-based dynamical necessary

literal checking SAT solver

CHANG Wenjing1,2，XU Yang2

(1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610036;

2.NationalLocal Joint Engineering Laboratory of System Credibility Automatic Verification,

Southwest Jiaotong University,Chengdu 610036,China）

Received:2017-12-25 Revised:2018-04-11 Online:2019-02-25 Published:2019-02-25

摘要/Abstract

摘要：

检查强制文字是一种重要的预处理方法。结合学习子句，提出一种在求解过程中使用的策略—基于子句的动态检查强制文字（CNL），并且设计了一种易实现低成本的数据结构。分别实现了两个不同版本的求解器：Glucose_PRE和Glucose_CNL，前者在求解初始时将检查强制文字作为预处理，后者实现了基于子句的动态检查强制文字策略。实验测试结果表明，与Glucose_PRE和Glucose3.0求解器相比，求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时，求解实例个数更多，耗时更少，说明所提策略和所设计的数据结构均可提高求解器的求解性能。

关键词: 可满足问题, 预处理技术, 强制文字, 数据结构

Abstract:

Necessary literal checking is an important preprocessing technique. by learning clauses, this paper proposes a clausebased dynamical necessary literal checking strategy (CNL) used in the solving process, and designs a lowcost data structure. We implement two solvers, Glucose_PRE and Glucose_CNL. The former adopts the necessary literal checking as the preprocessing technique at the beginning of the solving process, and the latter implements the proposed clausebased dynamical necessary literal checking strategy. Experimental results show that the Glucose_CNL solves more instances with less time than the Glucose_PRE and Glucose 3.0 when solving the applicationtype instances in 2015 and 2016 SAT competitions, demonstrating the significance of the proposed strategy and data structure.

Key words: satisfiability problem, preprocessing technique, necessary literal, data structure

常文静1,2，徐扬2. 基于子句的动态检查强制文字的SAT求解器[J]. 计算机工程与科学.

CHANG Wenjing1,2，XU Yang2.

A clause-based dynamical necessary

literal checking SAT solver

[J]. Computer Engineering & Science.

[1]	牛鹏飞, 王晓峰, 芦磊, 张九龙. 随机约束满足问题相变研究综述[J]. 计算机工程与科学, 2022, 44(07): 1321-1330.
[2]	张志祥，赵皑，崔良中. “小抄进考场”课程考核模式初探[J]. 计算机工程与科学, 2016, 38(增刊): 90-92.
[3]	李颖颖，韩林. 数据结构翻转课堂教学实践[J]. 计算机工程与科学, 2016, 38(增刊): 195-199.
[4]	唐艳琴，陈卫卫，施蕾. “数据结构”小班化教学探讨[J]. J4, 2014, 36(A1): 244-247.
[5]	王伟嘉，张洪萍，宁亚辉，陈勤，李余. 关于《数据结构》课程与ACMICPC竞赛结合的探讨[J]. J4, 2014, 36(A1): 257-260.
[6]	杨灿,桑波. 大整数乘法运算的实现及优化[J]. J4, 2013, 35(3): 183-190.
[7]	孟礼，武小悦. 带有互补边的共享OBDDs及数据结构[J]. J4, 2013, 35(1): 180-184.
[8]	赵伟波,刘青凯,秦桂明. 基于层次化数据结构的并行有限元计算[J]. J4, 2012, 34(8): 114-118.
[9]	张琨，杨会菊，宋继红，赵学龙. 基于遗传算法的自动组卷系统的设计与实现[J]. J4, 2012, 34(5): 178-183.
[10]	程聂，黄昆，苏欣，张大方. 一种基于树形结构的布鲁姆过滤器[J]. J4, 2012, 34(2): 19-24.
[11]	左正康, 游珍, 薛锦云. 后序遍历二叉树非递归算法的推导及形式化证明[J]. J4, 2010, 32(3): 119-123.
[12]	骆志刚,仲妍,吴枫. 稀疏线性方程组求解中的预处理技术综述[J]. J4, 2010, 32(12): 89-93.
[13]	张建民, 沈胜宇, 李思昆. 可满足性求解技术研究[J]. J4, 2010, 32(1): 50-54.
[14]	田李李爱平邹鹏贾焰. 更新数据流上的连续Skyline计算[J]. J4, 2008, 30(5): 59-64.
[15]	朱雅莉李肯立. DNA计算机中堆栈数据结构的设计[J]. J4, 2008, 30(4): 121-123.