Abstract
There has been considerable interest in the identification of structural properties of combinatorial problems that lead to efficient algorithms for solving them. Some of these properties are “easily” identifiable, while others are of interest because they capture key aspects of state-of-the-art constraint solvers. In particular, it was recently shown that the problem of identifying a strong Horn- or 2CNF-backdoor can be solved by exploiting equivalence with deletion backdoors, and is NP-complete. We prove that strong backdoor identification becomes harder than NP (unless NP=coNP) as soon as the inconsequential sounding feature of empty clause detection (present in all modern SAT solvers) is added. More interestingly, in practice such a feature as well as polynomial time constraint propagation mechanisms often lead to much smaller backdoor sets. In fact, despite the worst-case complexity results for strong backdoor detection, we show that Satz-Rand is remarkably good at finding small strong backdoors on a range of experimental domains. Our results suggest that structural notions explored for designing efficient algorithms for combinatorial problems should capture both statically and dynamically identifiable properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brockington, M., Culberson, J.C.: Camouflaging independent sets in quasi-random graphs. In: Johnson, D.S., Trick, M.A. (eds.) Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, American Mathematical Society, vol. 26, pp. 75–88 (1996)
Chandru, V., Hooker, J.N.: Detecting embedded Horn structure in propositional logic. Information Processing Letters 42(2), 109–111 (1992)
Chen, H., Dalmau, V.: Beyond hypertree width: Decomposition methods without decompositions. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 167–181. Springer, Heidelberg (2005)
Chen, H., Gomes, C., Selman, B.: Formal models of heavy-tailed behavior in combinatorial search. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, Springer, Heidelberg (2001)
Dechter, R.: Constraint Processing. Morgan Kaufmann Publishers Inc., San Francisco (2003)
Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artif. Intell. 34(1), 1–38 (1987)
Deville, Y., Van Hentenryck, P.: An efficient arc consistency algorithm for a class of csp problems. In: IJCAI 1991, pp. 325–330 (1991)
Freuder, E.C.: A sufficient condition for backtrack-free search. J. ACM 29(1), 24–32 (1982)
Freuder, E.C.: A sufficient condition for backtrack-bounded search. J. ACM 32(4), 755–761 (1985)
Freuder, E.C.: Complexity of k-tree structured constraint satisfaction problems. In: AAAI 1990, Boston, MA, pp. 4–9 (1990)
Gomes, C., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: AAAI 1998, New Providence, RI, pp. 431–438 (1998)
Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. Autom. Reason. 24(1-2), 67–100 (2000)
Hoffmann, J., Gomes, C., Selman, B.: Structure and problem hardness: Goal asymmetry and DPLL proofs in SAT-based planning. Logical Methods in Computer Science 3(1:6) (2007)
ILOG, SA: CPLEX 10.1 Reference Manual (2006)
Kilby, P., Slaney, J.K., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: AAAI 2005, pp. 1368–1373 (2005)
Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: IJCAI 1997, pp. 366–371 (1997)
Lynce, I., Marques-Silva, J.: Hidden structure in unsatisfiable random 3-SAT: An empirical study. In: ICTAI 2004 (2004)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001, pp. 530–535 (2001) ISBN 1-58113-297-2.
Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542. Springer, Heidelberg (2005)
Paris, L., Ostrowski, R., Siegel, P., Sais, L.: Computing Horn strong backdoor sets thanks to local search. In: ICTAI 2006, pp. 139–143 (2006), http://doi.ieeecomputersociety.org/10.1109/ICTAI.2006.43 ISSN 1082-3409
Samer, M., Szeider, S.: Constraint satisfaction with bounded treewidth revisited. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 499–513. Springer, Heidelberg (2006)
Sinz, C., Kaiser, A., Küchlin, W.: Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engr. Design, Analysis and Manufacturing 17(1), 75–97 (2003)
Szeider, S.: Backdoor sets for DLL subsolvers. J. of Automated Reasoning (2005)
van Beek, P., Dechter, R.: On the minimality and global consistency of row-convex constraint networks. J. ACM 42(3), 543–561 (1995)
Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: IJCAI 2003, pp. 1173–1178 (2003)
Williams, R., Gomes, C., Selman, B.: On the connections between heavy-tails, backdoors, and restarts in combinatorial search. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 222–230. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dilkina, B., Gomes, C.P., Sabharwal, A. (2007). Tradeoffs in the Complexity of Backdoor Detection. In: Bessière, C. (eds) Principles and Practice of Constraint Programming – CP 2007. CP 2007. Lecture Notes in Computer Science, vol 4741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74970-7_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-74970-7_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74969-1
Online ISBN: 978-3-540-74970-7
eBook Packages: Computer ScienceComputer Science (R0)