基于CDCL结构的SAT问题优化策略的研究

发布时间：2020-09-04 18:17

　　 可满足性问题(即SAT问题)是当代理论计算机科学的重要研究方向之一,也是第一个被证明的NP完全问题,SAT问题的求解有助于解决其他NP问题。其快速求解算法不仅具有重要的理论意义,也具有重要的实际价值。SAT问题广泛应用于社会生产和人类生活中的各个领域,如人工智能、自动推理、软件自动验证等。因此,设计并实现求解SAT问题的高效算法具有重要研究意义。目前,求解SAT问题的算法主要分为完备算法和不完备算法两类。不完备算法主要是基于随机搜索策略的局部搜索算法。完备算法主要基于1962年由Martin Davis,Hilary Putnam,George Logemann和Donald W.Loveland提出的DPLL算法,现在大多数完备算法都是基于DPLL算法发展而来,包括现在主流的CDCL算法。随着社会科学的进步,许多基于CDCL算法的求解器应运而生,用于解决日益复杂的大规模SAT问题,如z Chaff、Mini SAT、Glucose、Lingeling、PicoSAT等。本文基于CDCL算法结构,做了如下几个方面的研究工作:1.根据变量决策层和冲突次数,引入了分支决策阶段变量得分的增量函数,用于动态衡量不同搜索阶段下变量的得分,在此基础上,提出了基于变量决策层的分支策略(DLBH),为分支决策提供依据,引导求解器搜索过程;2.根据学习子句中不同变量的决策层,引入了子句深度,用于评估求解过程中所产生学习子句的质量,以删除低质量学习子句而保证高效率求解为目的,提出了基于子句深度的学习子句删除策略(DBCD);3.分别将所提出的DLBH策略和DBCD策略形成相应算法,嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh和glucose3.0+dbcd;将DLBH策略和DBCD策略对应的算法同时嵌入到著名求解器Glucose3.0中,得到新的求解器glucose3.0+dlbh+dbcd。选择2015年和2017年SAT国际竞赛中的问题进行测试,从测试结果在成功求解个数、平均决策次数、平均冲突次数、平均重启次数、平均用时等多项指标进行对比分析,显现出了新的求解器的有效性及优势。
【学位单位】：西南交通大学
【学位级别】：硕士
【学位年份】：2018
【中图分类】：TP301.6
【部分图文】：

图中的每一个点代表一个测试例，位于右下方的点代表求解器的性能高于位于左上方的点。从图5.1 可以看出，求解器 glucose3.0+dlbh、glucose3.0+dbcd 及 glucose3.0+dlbh+dbcd 在性

【参考文献】

相关期刊论文 前2条

1 郭莹;张长胜;张斌;;一种求解SAT问题的人工蜂群算法[J];东北大学学报(自然科学版);2014年01期

2 刘歆;颜萍;;用布尔可满足性验证逻辑电路的等价性[J];湖北工业大学学报;2007年02期

相关硕士学位论文 前1条

1 丁志宇;应用线性代数求解可满足性问题的研究与实现[D];中山大学;2014年

本文编号：2812429