计算机科学 ›› 2023, Vol. 50 ›› Issue (6A): 220600013-5.doi: 10.11896/jsjkx.220600013
刘凌荣, 陈树伟, 姜世攀
LIU Lingrong, CHEN Shuwei, JIANG Shipan
摘要： 在命题逻辑SAT求解过程中,子句集简化技术是重要的一个环节。冗余性质所对应的子句消去方法可以准确识别并删除冗余子句。无论是在预处理阶段还是SAT求解过程中,子句消去方法嵌入到SAT求解器均可加快求解器的求解效率。现有的高效子句消去方法大多基于封锁子句冗余性质和蕴涵模归结子句冗余性质扩展而来,为检查子句C是否冗余,只需要考虑子句C是否满足冗余条件。提出一种L-型冗余性质,它是封锁冗余性质、包含冗余性质、蕴涵模归结冗余性质的推广,将冗余子句判断条件由单个文字的归结式拓展到文字集合的组合。然后,针对L-型冗余性质,分析L-型冗余子句具有的性质,并将L-型冗余子句与已有的冗余子句的高效性进行比较,说明所提出的L-型冗余性质的高效性。
中图分类号:
| [1]LIU X H.Automatic Reasoning Based on Reduction Method[M].Beijing:Science Press,1994. [2]EEN N,BIERE A.Effective preprocessing in SAT through variable and clause elimination[C]//International Conference on Theory and Applications of Satisfiability Testing(SAT 2005).Berlin:Springer-Verlag,2005,3569:61-75. [3]JARVISALO M,BIERE A.Blocked Clause Elimination[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2010:129-144. [4]CHEN J C.Fast blocked clause decomposition with high quality[EB/OL].[2015-12-09][2022-05-28].https://arxiv.org/abs/1507.00459v2,2015. [5]HEULE M,JARVISALO M,BIERE A.Clause Elimination Procedures for CNF Formulas[C]//Logic for Programming,Artificial Intelligence,Reasoning International Conference.DBLP,2010:357-371. [6]HEULE M,JARVISALO M,BIERE A.Covered Clause Elimination[M]//Logic for Programming.Aritficial Intelligence and Reasoning-LPAR17,2010:41-46. [7]JARVISALO M,HEULE M,BIERE A.Inprocessing Rules[C]//International Joint Conference on Automated Reasoning.Berlin:Springer,2012:355-370. [8]KIESL B,SEIDL M,TOMPITS H,et al.Super-Blocked Clauses[C]//International Joint Conference on Automated Reasoning,IJCAR 2016.Springer International Publishing,2016:45-61. [9]HEULE M,KIESL B, BIERE A.Short Proofs Without NewVariables[C]//International Conference on Automated Deduction.Berlin,Springer-Verlag,2017:130-147. [10]HEULE M,KIESL B,BIERE A.Encoding Redundancy for Satisfaction-Driven Clause Learning[M]//Tools and Algorithms for the Construction and Analysis of Systems(ACAS 2019).2019:41-58. [11]NING X R,XU Y,CHEN Z S.Novel preprocessing clauseelimination methods for propositional SAT solvers[J].ComputerIntegrated Manufacturing Systems,2020,26(8):131-140. [12]NING X R,XU Y,CAO F,et al.Clause elimination methods in first-order logic lifted from proposition logic[J].Computer Engineering and Applications,2019,55(5):18-25. [13]NING X R.The study of redundancy property of propositional logic and first-order logic[D].Chengdu:Southwest Jiaotong University,2019. [14]LIU L R,CHEN S W,WU G F.A class of extended clause elimination methods in propositional logic[J].Journal of Sichuan Normal University,2023,46(1):117-124. |
|
||
首页