|
|
- 2017
利用逻辑演绎求解SAT问题的启发式完全算法
|
Abstract:
为解决可满足性（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%.
：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
| [1] | BIERE A. Adaptive restart strategies for conflict driven SAT solvers[C]//Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer, 2008:28-33. |
| [2] | BURO M, KLEINE-BVING H.Report on a SAT competition[R]. Paderborn:University of Paderborn, 1992. |
| [3] | JEROSLOW R E, WANG J. Solving propositional satisfiability problems[J]. Annals of Mathematics and Artificial Intelligence, 1990:167-187. |
| [4] | FREEMAN J W. Improvements to propositional satisfiability search algorithms[D]. Philadelphia:University of Pennsylvania, 1995. |
| [5] | 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. |
| [6] | 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. |
| [7] | 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. |
| [8] | CHANGC L, LEE R C T. Symbolic logic and mechanical theorem proving[M]. New York:Academic Press, 1973:130-162. |
| [9] | LOVELAND D W. A Linear Format for Resolution[M]. New York:Springer, 1970:147-162. |
| [10] | DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theoremproving[J]. Communications of the ACM, 1962, 5(7):394-397. |
| [11] | 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. |
| [12] | EéN N, S？ENSSON N. An extensible SAT solver[C]//SAT 2003. Heidelberg:Springer, 2015:502-518. |
| [13] | 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. |
| [14] | 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. |
| [15] | 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. |
| [16] | RYAN L. Efficient algorithms for clause-learning SAT solvers[D]. Vancouver:Simon Fraser University, 2004. |
| [17] | 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. |
| [18] | 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. |
| [19] | 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. |
| [20] | BIERE A. Pico SAT essentials[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4:75-97. |
| [21] | COOK S A. The complexity of theorem-proving procedures[C]//3rd Annual ACM Symposium on Theory of Computing. New York:ACM, 1971:151-158. |
| [22] | LUCKHAM D. Refinements in Resolution Theory[M]. New York:Springer, 1970:163-190. |
