Backdoor Sets for DLL Subsolvers
Tóm tắt
We study the parameterized complexity of detecting small backdoor sets for instances of the propositional satisfiability problem (SAT). The notion of backdoor sets has been recently introduced by Williams, Gomes, and Selman for explaining the ‘heavy-tailed’ behavior of backtracking algorithms. If a small backdoor set is found, then the instance can be solved efficiently by the propagation and simplification mechanisms of a SAT solver. Empirical studies indicate that structured SAT instances coming from practical applications have small backdoor sets. We study the worst-case complexity of detecting backdoor sets with respect to the simplification and propagation mechanisms of the classic Davis–Logemann–Loveland (DLL) procedure. We show that the detection of backdoor sets of size bounded by a fixed integer k is of high parameterized complexity. In particular, we determine that this detection problem (and some of its variants) is complete for the parameterized complexity class W[P]. We achieve this result by means of a generalization of a reduction due to Abrahamson, Downey, and Fellows.
Tài liệu tham khảo
Abrahamson, K. A., Downey, R. G. and Fellows, M. R. (1995) Fixed-parameter tractability and completeness. IV. On completeness for W[P] and PSPACE analogues, Ann. Pure Appl. Logic 73(3), 235–276.
Cook, S. A. and Mitchell, D. G. (1997) Finding hard instances of the satisfiability problem: A survey, in Satisfiability problem: theory and applications (Piscataway, NJ, 1996), American Mathematical Society, pp. 1–17.
Davis, M., Logemann, G. and Loveland, D. A (1962) machine program for theorem-proving, Commun. ACM 5, 394–397.
Davis, M. and Putnam, H. (1960) A computing procedure for quantification theory, J. ACM 7(3), 201–215.
Downey, R. G. and Fellows, M. R. (1999) Parameterized Complexity, Monographs in Computer Science. Springer.
Flum, J. and Grohe, M. (2004) Parameterized complexity and subexponential time, Bull. Eur. Assoc. Theor. Comput. Sci. 84, 71–100.
Interian, Y. (2003) Backdoor sets for random 3-SAT, in Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure, Portofino, Italy, May 5–8, 2003, (SAT 2003), informal proceedings, pp. 231–238.
Malik, S. (1994) Analysis of Cyclic Combinatorial Circuits, IEEE Trans. Comput.-Aided Des. 13(7), 950–956.
Nishimura, N., Ragde, P. and Szeider, S. (2004) Detecting backdoor sets with respect to Horn and binary clauses, in H. Hoos and D. G. Mitchell (eds.), Seventh International Conference on Theory and Applications of Satisfiability Testing, 10–13 May, 2004, Vancouver, BC, Canada (SAT 2004), informal proceedings, pp. 96–103.
Ruan, Y., Kautz, H. A. and Horvitz, E. (2004) The backdoor key: A path to understanding problem hardness, in D. L. McGuinness and G. Ferguson (eds.), Proceedings of the 19th National Conference on Artificial Intelligence, 16th Conference on Innovative Applications of Artificial Intelligence, pp. 124–130.
Williams, R., Gomes, C. and Selman, B. (2003a) Backdoors to typical case complexity, in G. Gottlob and T. Walsh (eds.), Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI 2003, pp. 1173–1178.
Williams, R., Gomes, C. and Selman, B. (2003b) On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search, in Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure, Portofino, Italy, May 5–8, 2003 (SAT 2003), informal proceedings, pp. 222–230.