Parallel QBF Solving with Advanced Knowledge Sharing

• Autorzy: Lewis M. , Schubert T. , Becker B. , Marin P. , Narizzano M. , Giunchiglia E.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE’s progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results.

Słowa kluczowe

EN

Quantified Boolean Formula (QBF); parallel solving; knowledge sharing; MPI

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 2/3
• Strony: 139--166
• Opis fizyczny: Bibliogr. 46 poz., tab., wykr.

Twórcy

autor

Lewis M.

autor

Schubert T.

autor

Becker B.

autor

Marin P.

autor

Narizzano M.

autor

Giunchiglia E.

• University of Freiburg Freiburg, Germany,

Bibliografia

• [1] The Quaffle Web Page, Http://www.princeton.edu/˜chaff/quaffle.html.
• [2] Ball, T., Cook, B., Levin, V., Rajamani, S. K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, IFM, 2004.
• [3] Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs, International Conference on Automated Deduction, Springer, 2005.
• [4] Benedetti, M., Mangassarian, H.: QBF-Based Formal Verification: Experience and Perspectives, Journal on Satisfiability, Boolean Modeling and Computation, 5, 2008.
• [5] Bentley, B.: Validating the Intel Pentium 4 Microprocessor, Design Automation Conference, 2001, 244-248.
• [6] Biere, A.: Resolve and Expand, Conference on Theory and Applications of Satisfiability Testing, 2004.
• [7] Biere, A., Heule, M. J. H., van Maaren, H., Walsh, T., Eds.: Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, February 2009, ISBN 978-1-58603-929-5.
• [8] Blochinger, W., Sinz, C., Küchlin, W.: A Universal Parallel SAT Checking Kernel, International Conference on Parallel and Distributed Processing Techniques and Applications, 2003.
• [9] Bubeck, U., Buning, H. K.: Bounded Universal Expansion for Preprocessing QBF, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2007.
• [10] Büning, H. K., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas, Journal of Information and Computation, 117(1), 1995, 12-18, ISSN 0890-5401.
• [11] Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae, Journal of Automated Reasoning, AAAI Press, 1998.
• [12] Chrabakh, W., Wolski, R.: GrADSAT: A Parallel SAT Solver for the Grid, UCSB Computer Science Technical Report Number 2003-05, 2003.
• [13] Chrabakh, W., Wolski, R.: GridSAT: A Chaff-based Distributed SAT Solver for the Grid, ACM/IEEE Supercomputing Conference, 2003.
• [14] Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem-Proving, Communications of the ACM, 5, 1962, 394-397.
• [15] Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF, International Conference on Theory and Applications of Satisfiability Testing, Springer, 2005.
• [16] Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel Multithreaded Satisfiability Solver: Design and Implementation, Electronic Notes in Theoretical Computer Science, 128(3), 2005, 75-90.
• [17] Feldmann, R., Monien, B., Schamberger, S.: A Distributed Algorithm to Evaluate Quantified Boolean Formulae, In Proc. AAAI-00, AAAI Press, 2000.
• [18] Gent, I., Giunchiglia, E., Narizzano, M., Rowley, A., Tacchella, A.: Watched Data Structures for BF Solvers, International Conference on Theory and Applications of Satisfiability Testing, 2004.
• [19] Gent, I. P., Rowley, A. G. D.: Solution Learning and Solution Directed Backjumping Revisited, Technical Report APES-80-2004, APES Research Group, 2004.
• [20] Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2010.
• [21] Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability, Proceedings of the First International Joint Conference on Automated Reasoning, Springer-Verlag, London, UK, 2001, ISBN 3-540-42254-4.
• [22] Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: an Efficient QBF Solver, Formal Methods in Computer Aided Design Conference, 2004.
• [23] Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas, Journal of Artificial Intelligence Research (JAIR), 26, 2006, 371-416.
• [24] Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2009, Lecture Notes in Computer Science, Springer, 2009.
• [25] Gropp, W., Lusk, E., Doss, N., Skjellum, A.: A High-Performance, Portable Implementation of the MPI Message Passing Interface Standard, Parallel Computing, 22(6), 1996, 789-828.
• [26] Hamadi, Y., Jabbour, S., Sais, L.: Control-based Clause Sharing in Parallel SAT Solving, Twenty-first International Joint Conference on Artificial Intelligence, 2009.
• [27] Harwood, G. C. A., Stuckey, P. J.: Cache Conscious Data Structures for Boolean Satisfiability Solvers, Journal on Satisfiability, 2008.
• [28] Herbstritt, M., Becker, B.: On Combining 01X-Logic and QBF, Proceedings of 11th International Conference on Computer Aided Systems Theory, 4739, Springer-Verlag, 2007.
• [29] Jurkowiak, B., Li, C., Utard, G.: Parallelizing Satz using Dynamic Workload Balancing, LICS 2001 Workshop on Theory and Applications of Satisfiability Testing, 2001.
• [30] Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas, In TABLEAUX 2002, Springer, 2002.
• [31] Lewis, M., Marin, P., Schubert, T., Narizzano, M., Becker, B., Giunchiglia, E.: PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing, International Conference on Theory and Applications of Satisfiability Testing, 2009.
• [32] Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving, 12th Asia and South Pacific Design Automation Conference, 2007.
• [33] Lewis, M., Schubert, T., Becker, B.: QMiraXT - A Multithreaded QBF Solver, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2009.
• [34] Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF Solving, SAT (H. K. Büning, X. Zhao, Eds.), 4996, Springer, 2008, ISBN 978-3-540-79718-0.
• [35] MIND-Lab and STAR-Lab: The Quantified Boolean Formulas Satisfiability Library, 2008, Http://www.qbflib.org/, http://www.mind-lab.it/, http://www.star-lab.it/.
• [36] Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver, Design, Automation and Test in Europe, 2009.
• [37] Rintanen, J.: Constructing Conditional Plans by a Theorem-Prover, Journal of Artificial Intelligence Research, 10, AAAI Press, 1999.
• [38] Rintanen, J.: Improvements to the Evaluation of Quantified Boolean Formulae, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1999, ISBN 1-55860-613-0.
• [39] Sabharwal, A., Ansotegui, C., Gomes, C., Hart, J., Selman, B.: QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2006, Lecture Notes in Computer Science, Springer, 2006.
• [40] Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF, International Conference on Principles and Practice of Constraint Programming, Springer, 2006.
• [41] Schubert, T., Lewis, M., Becker, B.: MiraXT & PaMiraXT: Parallel SAT Solving with Threads and Message Passing, Journal on Satisfiability, Boolean Modeling and Computation, 2009.
• [42] Sinz, C., Blochinger, W., Küchlin, W.: PaSAT - Parallel SAT-Checking with Lemma Exchange: Implementation and Applications, Workshop on Theory and Applications of Satisfiability Testing, 2001.
• [43] Snir, M., Otto, S., Walker, D., Dongarra, J., Huss-Lederman, S.: MPI: The Complete Reference, 1995.
• [44] Zhang, H., Bonacina, M., Hsiang, J.: PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems, Journal of Symbolic Computation, 21(4), 1996, 543-560.
• [45] Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean Satisfiability Solver, Proceedings of the 2002 IEEE/ACM International Conference on Computer Aided Design, ACM Press, 2002.
• [46] Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation, Conference on Principles and Practice of Constraint Programming, 2002.