An Empirical Study of QBF Encodings: from Treewidth Estimation to Useful Preprocessing

• Autorzy: Pulina L. , Tacchella A.
• Języki publikacji: EN

Abstrakty

EN

From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings.

Słowa kluczowe

EN

automated reasoning; Structural Decompositions; QBF preprocessing

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 3/4
• Strony: 391--427
• Opis fizyczny: Bibliogr. 48 poz., tab., wykr.

Twórcy

autor

Pulina L.

autor

Tacchella A.

• DIST, Universita di Genova, Viale Causa, 13 - 16145 Genova, Italy,

Bibliografia

• [1] L. Stockmeyer, A. Meyer, Word roblems requiring exponential time (Preliminary Report), in: 5th Annual ACM Symposium on the Theory of computing, 1973, pp. 1-9.
• [2] L. Pulina, A. Tacchella, A self-adaptive multi-engine solver for quantified Boolean formulas, Constraints 14 (1) (2009) 80-116.
• [3] N. Robertson, P. D. Seymour, Graph Minors. II: Algorithmic aspects of tree-width, Journal of Algorithms 7 (3) (1986) 309-322.
• [4] H. Bodlaender, Treewidth: Characterizations, Applications, and Computations, Tech. rep., Utrecht University (2006).
• [5] E. Freuder, Complexity of k-tree Structured Constraint Satisfation Problems, in: In proc. of 8th Nat.l Conf.on Artificial Intelligence, 1990, pp. 4-9.
• [6] R. Dechter, J. Pearl, Tree Clustering for Constraint Networks, Artificial Intelligence 38 (3) (1989) 353-266.
• [7] H. Chen, V. Dalmau, From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction, in: 19th Int.l workshop on Computer Science Logic, Vol. 3634 of LNCS, 2005, pp. 232-247.
• [8] G. Gottlob, G. Greco, F. Scarcello, The Complexity of Quantified Constraint Satisfaction Problems under Structural Restrictions, in: 19th Int.l Joint Conf. on Artificial Intelligence, 2005, pp. 150-155.
• [9] G. Pan, M. Vardi, Fixed-Parameter Hierarchies inside PSPACE, in: 21th IEEE Symposium on Logic in Computer Science, 2006, pp. 27-36.
• [10] M. Narizzano, L. Pulina, A. Taccchella, 4th QBF solvers evaluation, http://www.qbfeval.org/2006 (2006).
• [11] M. Narizzano, L. Pulina, A. Taccchella, 5th QBF solvers evaluation, http://www.qbfeval.org/2008 (2007).
• [12] C. Peschiera, L. Pulina, A. Taccchella, 6th QBF solvers evaluation, http://www.qbfeval.org/2008 (2008).
• [13] S. Arnborg, D. Corneil, A. Proskurowski, Complexity of finding embeddings in a k-tree, SIAM Journal on Algebraic and Discrete Methods 8 (1987) 277-284.
• [14] H. Samulowitz, R. Memisevic, Learning to Solve QBF, in: 22nd Nat.l Conf. on Artificial Intelligence, 2007, pp. 255-260.
• [15] E. Giunchiglia, M. Narizzano, A. Tacchella, Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability, Artificial Intelligence Research 26 (2006) 371-416, available on-line at http://www.jair.org/vol/vol26.html.
• [16] L. Zhang, S. Malik, Conflict driven learning in a Quantified Boolean Satisfiability solver, in: 2002 IEEE/ACM Int.l Conf. on Computer-aided Design, 2002, pp. 442-449.
• [17] M. Benedetti, sKizzo: a Suite to Evaluate and Certify QBFs, in: 20th Int.l. Conf. on Automated Deduction, Vol. 3632 of LNCS, 2005, pp. 369-376.
• [18] A. Biere, Resolve and Expand, in: 7th Intl. Conf. on Theory and Applications of Satisfiability Testing, Vol. 3542 of LNCS, 2005, pp. 59-70.
• [19] G. Pan, M. Vardi, Symbolic Decision Procedures for QBF, in: 10th Int.l Conf. on Principles and Practice of Constraint Programming, 2004, pp. 453-467.
• [20] H. Samulowitz, J. Davies, F. Bacchus, Preprocessing QBF, in: 12th Int.l Conf. on Principles and Practice of Constraint Programming, Vol. 4204 of LNCS, 2006, pp. 514-529.
• [21] U. Bubeck, H. Büning, Bounded Universal Expansion for Preprocessing QBF, in: 10th Int.l Conf. of Theory and Applications of Satisfiability Testing, Vol. 4501 of LNCS, Springer, 2007, pp. 244-257.
• [22] L. Pulina, A. Tacchella, MIND-Lab projects and related information, http://www.mind-lab.it/projects (2008).
• [23] R. Tarjan, M. Yannakakis, Addendum: Simple Linear-Time Algorithms to Test Chordality of Graphs, Test Acyclicity of Hypergraphs, and Selectively Reduce Acyclic Hypergraphs, SIAM J. Comput. 14 (1) (1985) 254-255.
• [24] D. J. Rose, A graph-theoretic study of the numerical solution of sparse positive definite systems of linear equations., Graph Theory and Computing (1972) 183-217.
• [25] S. Subbarayan, H. Andersen, Backtracking Procedures for Hypertree, HyperSpread and Connected Hypertree Decomposition of CSPs, in: 20th Int.l Joint Conf on Artificial Intelligence, 2007, pp. 180-185.
• [26] U. Kjærulff, Triangulation of graphs: Algorithms giving small total state space., Tech. rep., University of Aalborg. (1990).
• [27] M. Benedetti, Quantifier Trees for QBFs, in: 8th Int.l Conf. on Theory and Applications of Satisfiability Testing, Vol. 3569 of LNCS, 2005, pp. 378-385.
• [28] E. Giunchiglia, M. Narizzano, A. Tacchella, Quantifier Structure in search based procedures for QBFs, IEEE Trans. on Computer Aided Design of Integrated Circuits and Systems 26 (3) (2007) 497-507.
• [29] G. Csardi, T. Nepusz, Igraph Reference Manual (2006).
• [30] V. Gogate, R. Dechter, A Complete Anytime Algorithm for Treewidth, in: 20th Conf. in Uncertainty in Artificial Intelligence, 2004, pp. 201-208.
• [31] I. Rish, R. Dechter, Resolution versus Search: Two Strategies for SAT., Journal of Automated Reasoning 24 (1/2) (2000) 225-275.
• [32] G. Gottlob, N. Leone, F. Scarcello, A comparison of structural CSP decomposition methods, Artificial Intelligence 124 (2000) 243-282.
• [33] N. Eén, N. Sorensson, MiniSat v1.13: A SAT solver with conflict-clause minimization, in: 8th Intl. Conf. On Theory and Applications of Satisfiability Testing, Vol. 3569 of LNCS, 2005, p. 53.
• [34] I. Witten, E. Frank, Data Mining (2nd edition), Morgan Kaufmann, 2005.
• [35] M. Davis, H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7 (3) (1960) 201-215.
• [36] A. Ayari, D. Basin, Bounded Model Construction for Monadic Second-Order Logics, in: 12th Int.l Conf. On Computer Aided Verification, no. 1855 in LNCS, 2000, pp. 99-113.
• [37] H. Palacios, H. Geffner, Mapping Conformant Planning into SAT Through Compilation and Projection, in: 11th Conf. of the Spanish Association for Artificial Intelligence, Vol. 4177 of LNCS, 2005, pp. 311-320.
• [38] G. Pan, M. Vardi, Optimizing a BDD-based Modal Solver, in: 19th Int.l Conf. on Automated Deduction, Vol. 2741 of LNCS, 2003, pp. 75-89.
• [39] P. Balsiger, A. Heuerding, S. Schwendimann, A Benchmark Method for the Propositional Modal Logics K, KT, S4, Journal of Automated Reasoning 24 (3) (2000) 297-317.
• [40] Z. H. N. Dershowitz, J. Katz, Bounded Model Checking with QBF, in: 8th Int.l Conf. on Theory and Applications of Satisfiability Testing, Vol. 3569 of LNCS, 2005, pp. 408-414.
• [41] M. Mneimneh, K. Sakallah, Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution, in: 6th Int.l Conf. on Theory and Applications of Satisfiability Testing, Vol. 2919 of LNCS, 2003, pp. 411-425.
• [42] T. Jussila, A. Biere, Compressing BMC Encodings with QBF, in: Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), 2006.
• [43] E. Giunchiglia, M. Narizzano, A. Tacchella, QuBE++: an Efficient QBF Solver, in: 5th Conf. on Formal Methods in Computer Aided Design, Vol. 3312 of LNCS, 2004, pp. 201-213.
• [44] E. Giunchiglia, P. Marin, M. Narizzano, STAR-Lab projects and related information, http://www.star. dist.unige.it (2009).
• [45] D. Tang, Y. Yu, D. Ranjan, S. Malik, Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit Space Diameter Problem, in: 7th Int.l Conf. on Theory and Applications of Satisfiability Testing, Vol. 3542 of LNCS, 2004, pp. 292-2305.
• [46] D. J. Watts, S. H. Strogatz, Collective dynamics of small-world networks, Nature 393 (1998) 440-442.
• [47] L. Pulina, A. Tacchella, Treewidth: A useful marker of empirical hardness in quantified boolean logic encodings, in: 15th Int.l Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Vol. 5330 of LNCS, 2008, pp. 528-542.
• [48] J. Larrosa, R. Dechter, Boosting Search with Variable Elimination in Constraint Optimization and Constraint Satisfaction Problems, Constraints 8 (3) (2003) 303-326.