摘要: Most CSP algorithms are based on refinements and extensions of backtracking, employ one two simple "branching schemes": 2-way branching or d-way branching, for domain size d. The schemes not equivalent, but little is known about their relative power. Here we compare them in terms how efficiently they can refute an unsatisfiable instance with optimal choices, by studying variants the resolution proof system, denoted C-RES NG-RES, which model reasoning algorithms. tree-like restrictions, tree-C-RES tree-NG-RES, exactly capture power backtracking respectively. We give a family instances require exponential sized search trees have O(d2n) branching. also natural strategy finds refutations these time O(d2n2). unrestricted NG-RES simulate incorporate learning k-consistency enforcement. show separations between as well versions each system. All given nearly optimal.
springer.com
core.ac.uk
sci-hub.st 参考文章(15)
Avi Wigderson, Russell Impagliazzo, Eli Ben-Sasson, Near-Optimal Separation of Treelike and General Resolution Electronic Colloquium on Computational Complexity. ,vol. 7, ,(2000)
David Geoffrey Mitchell, Hector Levesque, The resolution complexity of constraint satisfaction University of Toronto. ,(2002)
Andrew B. Baker, Intelligent backtracking on constraint satisfaction problems: experimental and theoretical results University of Oregon. ,(1995)
Cho Yee Joey Hwang, A Theoretical Comparison of Resolution Proof Systems for CSP Algorithms ,(2004)
David G. Mitchell, Resolution Complexity of Random Constraints principles and practice of constraint programming. pp. 295- 309 ,(2002) , 10.1007/3-540-46135-3_20
M.L. Bonet, J.L. Esteban, N. Galesi, J. Johannsen, Exponential separations between restricted resolution and cutting planes proof systems foundations of computer science. pp. 638- 647 ,(1998) , 10.1109/SFCS.1998.743514
Balakrishnan Krishnamurthy, Short proofs for tricky formulas Acta Informatica. ,vol. 22, pp. 253- 275 ,(1985) , 10.1007/BF00265682
Wolfgang J. Paul, Robert Endre Tarjan, James R. Celoni, Space bounds for a game on graphs Proceedings of the eighth annual ACM symposium on Theory of computing - STOC '76. pp. 149- 160 ,(1976) , 10.1145/800113.803643
Toniann Pitassi, Josh Buresh-Oppenheim, David G. Mitchell, Linear and Negative Resolution are weaker than Resolution Electronic Colloquium on Computational Complexity. ,vol. 8, ,(2001)
Vincent Se-jin Park, AN EMPIRICAL STUDY OF DIFFERENT BRANCHING STRATEGIES FOR CONSTRAINT SATISFACTION PROBLEMS University of Waterloo. ,(2004)