Abstract
Theoretical studies show that in some combinatorial problems, there is a close relationship between classes of tractable instances and the treewidth (tw) of graphs describing their structure. In the case of satisfiability for quantified Boolean formulas (QBFs), tractable classes can be related to a generalization of treewidth, that we call quantified treewidth (tw p ). In this paper we investigate the practical relevance of computing tw p for problem domains encoded as QBFs. We show that an approximation of tw p is a predictor of empirical hardness, and that it is the only parameter among several other candidates which succeeds consistently in being so. We also provide evidence that QBF solvers benefit from a preprocessing phase geared towards reducing tw p , and that such phase is a potential enabler for the solution of hard QBF encodings.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bodlaender, H.L.: Treewidth: Characterizations, applications, and computations. Technical report, Utrecht University (2006)
Freuder, E.: Complexity of k-tree structured constraint satisfation problem. In: Proc. of AAAI 1990 (1990)
Dechter, R., Pearl, J.: Tree Clustering for constraint networks. Artificial Intelligence, 61–95 (1989)
Chen, H., Dalmau, V.: From pebble games to tractability: An ambidextrous consistency algorithm for quantified constraint satisfaction. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634. Springer, Heidelberg (2005)
Gottlob, G., Greco, G., Scarcello, F.: The Complexity of Quantified Constraint Satisfaction Problems under Structural Restrictions. In: IJCAI 2005, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pp. 150–155. Professional Book Center (2005)
Pan, G., Vardi, M.Y.: Fixed-Parameter Hierarchies inside PSPACE. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 27–36. IEEE Computer Society, Los Alamitos (2006)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: 5th Annual ACM Symposium on the Theory of Computation, pp. 1–9 (1973)
Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), www.qbflib.org
Narizzano, M., Pulina, L., Taccchella, A.: QBF solvers competitive evaluation (QBFEVAL) (2006), http://www.qbflib.org/qbfeval
Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM Journal on Algebraic and Discrete Methods, 277–284 (1987)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Artificial Intelligence Research 26, 371–416 (2006), http://www.jair.org/vol/vol26.html
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design (ICCAD 2002) (2002)
Benedetti, M.: sKizzo: A suite to evaluate and certify QBFS. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 369–376. Springer, Heidelberg (2005)
Biere, A.: Resolve and expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Pan, G., Y. Vardi, M.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 453–467. Springer, Heidelberg (2004)
Rish, I., Dechter, R.: Resolution versus search: Two strategies for sat. Journal of Automated Reasoning 24(1/2), 225–275 (2000)
Tarjan, R.E., Yannakakis, M.: Addendum: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. Comput. 14(1), 254–255 (1985)
Gogate, V., Dechter, R.: A Complete Anytime Algorithm for Treewidth. In: UAI 2004, Proceedings of the 20th Conference in Uncertainty in Artificial Intelligence, pp. 201–208. AUAI Press (2004)
Subbarayan, S., Andersen, H.R.: Backtracking Procedures for Hypertree, HyperSpread and Connected Hypertree Decomposition of CSPs. In: IJCAI, pp. 180–185 (2007)
Benedetti, M.: Quantifier trees for QBFS. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569. Springer, Heidelberg (2005)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantifier Structure in search based procedures for QBFs. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 26(3) (2007)
Pulina, L., Taccchella, A.: MIND-Lab projects and related information (2008), http://www.mind-lab.it/projects
Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 574–589. Springer, Heidelberg (2007)
Witten, I.H., Frank, E.: Data Mining, 2nd edn. Morgan Kaufmann, San Francisco (2005)
Kleine-Büning, H., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995)
Larrosa, J., Dechter, R.: Boosting Search with Variable Elimination in Constraint Optimization and Constraint Satisfaction Problems. Constraints 8(3), 303–326 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pulina, L., Tacchella, A. (2008). Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings . In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)