Heuristics based on unit propagation for satisfiability problems
作者： Chu Min Li , Anbulagan Anbulagan
DOI:
关键词:
摘要: The paper studies new unit propagation based heuristics for Davis-Putnam-Loveland (DPL) procedure. These are the novel combinations of and usual "Maximum Occurrences in clauses Minimum Size" heuristics. Based on experimental evaluations different alternatives a simple heuristic is put forward. This compares favorably with employed current state-of-the-art DPL implementations (C-SAT, Tableau, POSIT).
ijcai.org 
acm.org 参考文章(8)
Bart Selman, David Mitchell, Hector Levesque, Hard and easy distributions of SAT problems national conference on artificial intelligence. pp. 459- 465 ,(1992)
Jon William Freeman, Improvements to propositional satisfiability search algorithms University of Pennsylvania. ,(1995)
Stephen A. Cook, The complexity of theorem-proving procedures symposium on the theory of computing. pp. 151- 158 ,(1971) , 10.1145/800157.805047
Donald Loveland, George Logemann, Martin Davis, A machine program for theorem-proving ,(2011)
Robert G. Jeroslow, Jinchang Wang, Solving propositional satisfiability problems Annals of Mathematics and Artificial Intelligence. ,vol. 1, pp. 167- 187 ,(1990) , 10.1007/BF01531077
Vašek Chvátal, Endre Szemerédi, Many hard examples for resolution Journal of the ACM. ,vol. 35, pp. 759- 768 ,(1988) , 10.1145/48014.48016
James M. Crawford, Larry D. Auton, Experimental results on the crossover point in random 3-SAT Artificial Intelligence. ,vol. 81, pp. 31- 57 ,(1996) , 10.1016/0004-3702(95)00046-1
J. N. Hooker, V. Vinay, Branching rules for satisfiability Journal of Automated Reasoning. ,vol. 15, pp. 359- 383 ,(1995) , 10.1007/BF00881805