Measuring the hardness of SAT instances
作者： Felip Manyà , Jordi Levy , Carlos Ansótegui , María Luisa Bonet
DOI:
关键词:
摘要: The search of a precise measure what hardness SAT instances means for state-of-the-art solvers is relevant research question. Among others, the space complexity treelike resolution (also called hardness), minimal size strong backdoors and cycle-cutsets, treewidth can be used this purpose. We propose use tree-like as solid candidate to best based on DPLL. To support thesis we provide comparison with other mentioned measures. We also conduct an experimental investigation show how proposed characterizes random industrial instances.
参考文章(21)
Sylvie Thiébaux, Philip Kilby, John Slaney, Toby Walsh, Backbones and backdoors in satisfiability national conference on artificial intelligence. pp. 1368- 1373 ,(2005)
Carla Gomes, César Fernàndez, Carles Mateu, Ramón Béjar, Carlos Ansótegui, The impact of balancing on problem hardness in a highly structured domain national conference on artificial intelligence. pp. 10- 15 ,(2006)
Bistra Dilkina, Carla P. Gomes, Ashish Sabharwal, Tradeoffs in the complexity of backdoor detection principles and practice of constraint programming. pp. 256- 270 ,(2007) , 10.1007/978-3-540-74970-7_20
Oliver Kullmann, Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs Electronic Colloquium on Computational Complexity. ,(1999)
Chu Min Li, Anbulagan, Look-ahead versus look-back for satisfiability problems principles and practice of constraint programming. pp. 341- 355 ,(1997) , 10.1007/BFB0017450
Jacobo Torán, Lower Bounds for Space in Resolution computer science logic. pp. 362- 373 ,(1999) , 10.1007/3-540-48168-0_26
Jon William Freeman, Improvements to propositional satisfiability search algorithms University of Pennsylvania. ,(1995)
Bart Selman, Carla P. Gomes, Ryan Williams, Backdoors to typical case complexity international joint conference on artificial intelligence. pp. 1173- 1178 ,(2003)
Eli Ben-Sasson, Nicola Galesi, Space complexity of random formulae in resolution Random Structures and Algorithms. ,vol. 23, pp. 92- 109 ,(2003) , 10.1002/RSA.10089
Jakob Nordström, Narrow proofs may be spacious Proceedings of the thirty-eighth annual ACM symposium on Theory of computing - STOC '06. ,vol. 2006, pp. 507- 516 ,(2006) , 10.1145/1132516.1132590