利用逻辑演绎求解SAT问题的启发式完全算法

doi:10.3969/j.issn.0258-2724.2017.06.025

基金项目:

国家自然科学基金资助项目（61673320，11526171，61305074）

中央高校基本科研业务费专项资金资助项目（2682017ZT12）

详细信息

作者简介:
陈青山(1982-),男,助教,博士研究生,研究方向为智能信息处理、自动推理,E-mail:qschen@home.swjtu.edu.cn

计量
- 文章访问数:533
- HTML全文浏览量:133
- PDF下载量:85
- 被引次数:0
出版历程
- 收稿日期:2017-03-22
- 刊出日期:2017-12-25

Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction

摘要

摘要:为解决可满足性（satisfiability problem，SAT）问题求解过程中分支决策效率不高的问题，提出了一种基于逻辑演绎分组（logical deduction group，LDG）的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎，得到一组局部可满足赋值序列，并引导求解器优先搜索赋值序列所在解空间；对于可满足问题，可以通过迭代调用演绎过程，将局部可满足解成组地扩充为全局可满足解，对于不可满足问题，如果演绎结果出现空子句，则可以直接判定.采用SAT国际竞赛的实例，与具有代表性的指数级变元状态独立下降和（exponential variable state independent decaying sum，EVSIDS）变量决策算法进行了对比测试，结果表明：在求解总问题数方面，LDG比EVSIDS多出42个；在求解速度方面，LDG对可满足问题的求解时间相较EVSIDS平均减少了22.8%，对不可满足问题的求解时间平均减少了17.8%，总平均时间减少了20.1%.
- SAT问题/
- 启发式算法/
- 搜索算法/
- 变量决策/
- 演绎推理
Abstract:In order to address the issue of branch decision-making inefficiency in solving the satisfiability problem (SAT), a heuristic complete algorithm based on logical deduction group (LDG) is proposed. Specifically, the proposed algorithm chooses the remaining unsolved clauses to make the logical deduction such that an assignment sequence of partial satisfiability is obtained, further guiding the solver to first search its solution space. For the satisfiable problem, the partial assignment can be extended group by group to a complete assignment by iteratively utilizing the deductive process. For the unsatisfiable problem, it can be straightforward to judge whether there exists an empty clause. The international competition instance in SAT is adopted for comparison with the typical exponential variable state independent decaying sum (EVSIDS) decision heuristic. The experimental results demonstrate that LDG can solve 42 more problems than EVSIDS, and achieve 22.8% and 17.8% reductions in average solution time for the satisfiable and unsatisfiable problems, respectively, as well as a 20.1% reduction in total average time.
- satisfiability problem/
- heuristic algorithms/
- searching algorithms/
- decision making/
- deductive reasoning

HTML全文

参考文献 (22)

COOK S A. The complexity of theorem-proving procedures[C]//3rd Annual ACM Symposium on Theory of Computing. New York:ACM, 1971:151-158.

DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theoremproving[J]. Communications of the ACM, 1962, 5(7):394-397.

MOSKEWICZ M W, MADIGAN C F, ZHAO Y. Chaff:engineering an efficient SAT solver[C]//Proceedings of the 38th Annual Design Automation Conference. New York:ACM, 2001:530-535.

EÉN N, SÖENSSON N. An extensible SAT solver[C]//SAT 2003. Heidelberg:Springer, 2015:502-518.

GOMES C P, SELMAN B, KAUTZ H.Boosting combinatorial search through randomization[C]//Proceeding of the Fifteenth National Conference on Artificial Intelligence. Madison:AAAI Press, 1998:431-437.

GOLDBERG E, NOVIKOV Y.BerkMin:a fast and robust SATsolver[C]//Proceedings of Design, Automation and Test in Europe Conference. Los Alamitos:IEEE Computer Society Press, 2002:142-149.

LEWIS M D T,SCHUBERT T, BECKER B. Speedup techniques utilized in modern SAT solvers[C]//International Conference in Theory and Applications of Satisfiability Testing. Heidelberg:Springer, 2005:437-443.

RYAN L. Efficient algorithms for clause-learning SAT solvers[D]. Vancouver:Simon Fraser University, 2004.

MARQUES-SILVA J P, LYNCE I, MALIK S. Conflict-driven clause learning SAT solvers[M]//In Handbook of Satisfiability. Amsterdam:IOS Press, 2009:127-149.

MARQUES-SILVA J P, SAKALLAH K A. Grasp:a new search algorithm for satisfiability[C]//Proceedings of the 1996 IEEE/ACM International Conference onComputer-aided Design. Los Alamitos:IEEE Computer Society Press, 1996:220-227.

BIERE A. Pico SAT essentials[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4:75-97.

AUDEMARD G, SIMON L. Glucose 2.3 in the SAT 2013 Competition[C]//Theory and Applications of Satisfiability Testing-SAT 2008. Heidelberg:Springer, 2013:42-43.

BELOV A, DIEPOLD D, HEULE M J H, et al. SAT competition 2014 solver and benchmark descriptions. (2014-6-27)[2016-10-15]. https://helda.helsinki.fi/bitstream/handle/10138/135571/sc2014_proceedings.pdf?sequence=1.

JEROSLOW R E, WANG J. Solving propositional satisfiability problems[J]. Annals of Mathematics and Artificial Intelligence, 1990:167-187.

BURO M, KLEINE-BVING H.Report on a SAT competition[R]. Paderborn:University of Paderborn, 1992.

FREEMAN J W. Improvements to propositional satisfiability search algorithms[D]. Philadelphia:University of Pennsylvania, 1995.

LIANG J H, GANESH V,POUPART P, et al. Learning rate based branchingheuristic for SAT solvers[C]//In Theory and Applications of Satisfiability Testing-SAT 2016.[S.l.]:Springer, 2016:123-140.

BIERE A, FROHLICH A. Evaluating CDCL variable scoring schemes[C]//In Theory and Applications of Satisfiability Testing-SAT 2015.[S.l.]:Springer, 2015:405-422.

BIERE A. Adaptive restart strategies for conflict driven SAT solvers[C]//Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer, 2008:28-33.

CHANGC L, LEE R C T. Symbolic logic and mechanical theorem proving[M]. New York:Academic Press, 1973:130-162.

LOVELAND D W. A Linear Format for Resolution[M]. New York:Springer, 1970:147-162.

LUCKHAM D. Refinements in Resolution Theory[M]. New York:Springer, 1970:163-190.

施引文献

附加材料 (0)

访问统计