Abstract
Quantified Boolean formulas (QBFs) extend propositional logic by universal and existential quantifiers over the propositional variables. In the same way as the satisfiability problem of propositional logic is the archetypical problem for NP, the satisfiability problem of QBFs is the archetypical problem for PSPACE. Hence, QBFs provide an attractive framework for encoding many applications from verification, artificial intelligence, and synthesis, thus motivating the quest for efficient solving technology. Already in the very early stages of QBF solving history, attempts have been made to parallelize the solving process, either by splitting the search space or by portfolio-based approaches. In this chapter, we review and compare approaches for solving QBFs in parallel.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cyrille Artho, Armin Biere, and Martina Seidl. Model-Based Testing for Verification Back-Ends. In Margus Veanes and Luca Viganò, editors, Proc. of the 7th Int. Conference on Tests and Proofs (TAP 2017), volume 7942 of LNCS, pages 39–55. Springer, 2013.
Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, and Yoriyuki Yamagata. Model-Based Testing of Stateful APIs with Modbat. In Myra B. Cohen, Lars Grunske, and Michael Whalen, editors, Proc. of the 30th Int. Conference on Automated Software Engineering (ASE 2015), pages 858–863. IEEE Computer Society, 2015.
Bengt Aspvall, Christos Levcopoulos, Andrzej Lingas, and Robert Storlind. On 2-QBF Truth Testing in Parallel. Information Processing Letters, 57(2):89–93, 1996.
Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett., 8(3):121–123, 1979.
Abdelwaheb Ayari and David A. Basin. QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. In Mark Aagaard and John W. O’Leary, editors, Proc. of the 4th Int. Conference on Formal Methods in Computer-Aided Design (FMCAD 2002), volume 2517 of LNCS, pages 187–201. Springer, 2002.
Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45–65, 2012.
Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolás Janota, and Magdalena Widl. Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. In Blai Bonet and Sven Koenig, editors, Proc. of the 29th AAAI Conference on Artificial Intelligence (AAAI 2015), pages 3694–3701. AAAI Press, 2015.
Tomas Balyo and Florian Lonsing. HordeQBF: A Modular and Massively Parallel QBF Solver. In Nadia Creignou and Daniel Le Berre, editors, Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of LNCS, pages 531–538. Springer, 2016.
Tomas Balyo, Peter Sanders, and Carsten Sinz. HordeSat: A Massively Parallel Portfolio SAT Solver. In Marijn Heule and Sean Weaver, editors, Proc. of the 18th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2015), volume 9340 of LNCS, pages 156–172. Springer, 2015.
Marco Benedetti and Hratch Mangassarian. QBF-Based Formal Verification: Experience and Perspectives. Journal on Satisfiability, Boolean Modeling and Computation, 5(1-4):133–191, 2008.
Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. In Ernst W. Mayr and Nicolas Ollinger, editors, Proc. of the 32nd Int. Symposium on Theoretical Aspects of Computer Science (STACS 2015), volume 30 of LIPIcs, pages 76–89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
Armin Biere. Resolve and Expand. In Holger H. Hoos and David G. Mitchell, editors, Proc. of the 7th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2004), volume 3542 of LNCS, pages 59–70. Springer, 2004.
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
Roderick Bloem, Robert Könighofer, and Martina Seidl. SAT-Based Synthesis Methods for Safety Specs. In Kenneth L. McMillan and Xavier Rival, editors, Proc. of the 15th Int. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), volume 8318 of LNCS, pages 1–20. Springer, 2014.
Bart Bogaerts, Tomi Janhunen, and Shahab Tasharrofi. Solving QBF instances with nested SAT solvers. In Adnan Darwiche, editor, Proc. of the 2016 AAAI Workshop Beyond NP, volume WS-16-05 of AAAI Workshops. AAAI Press, 2016.
Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of LNCS, pages 44–57. Springer, 2010.
Uwe Bubeck and Hans Kleine Büning. Bounded Universal Expansion for Preprocessing QBF. In Proc. of the 10th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2007), volume 4501 of LNCS, pages 244–257. Springer, 2007.
Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An Algorithm to Evaluate Quantified Boolean Formulae. In Jack Mostow and Chuck Rich, editors, Proc. of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (AAAI/IAAI 1998), pages 262–267. AAAI Press / The MIT Press, 1998.
Koen Claessen, Niklas Eén, Mary Sheeran, Niklas Sörensson, Alexey Voronov, and Knut Åkesson. SAT-Solving in Practice, with a Tutorial Example from Supervisory Control. Discrete Event Dynamic Systems, 19(4):495–524, 2009.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752–794, 2003.
Benoit Da Mota. Quantified Boolean formulae: formal processings and parallel computations. Thesis, Université d’Angers, December 2010.
Martin Davis, George Logemann, and DonaldW. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Proc. of the 8th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2005), volume 3569 of LNCS, pages 61–75. Springer, 2005.
Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Proc. of the 9th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2006), volume 2919 of LNCS, pages 502–518. Springer, 2003.
Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci., 89(4):543–560, 2003.
Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell., 80(1):21–45, 2017.
Wolfgang Faber and Francesco Ricca. Solving hard ASP programs efficiently. In Chitta Baral, Gianluigi Greco, Nicola Leone, and Giorgio Terracina, editors, Proc. of the 8th Int. Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005), volume 3662 of LNCS, pages 240–252. Springer, 2005.
Rainer Feldmann, Burkhard Monien, and Stefan Schamberger. A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In Henry A. Kautz and Bruce W. Porter, editors, Proc. of the 17th Nat. Conference on Artificial Intelligence and 12th Conference on on Innovative Applications of Artificial Intelligence (AAA/IAAI 2000), pages 285–290. AAAI Press / The MIT Press, 2000.
Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Michela Milano, editor, Proc. of the 18th Int. Conference on Principles and Practice of Constraint Programming (CP 2012), volume 7514 of LNCS, pages 647–663. Springer, 2012.
Allen Van Gelder. Primal and Dual Encoding from Applications into Quantified Boolean Formulas. In Christian Schulte, editor, Proc. of the 19th Int. Conference on Principles and Practice of Constraint Programming (CP 2013), volume 8124 of LNCS, pages 694–707. Springer, 2013.
Ian P. Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew G. D. Rowley, and Armando Tacchella. Watched data structures for QBF solvers. In Enrico Giunchiglia and Armando Tacchella, editors, Proc. of the 6th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2003), volume 2919 of LNCS, pages 25–36. Springer, 2003.
Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 761–780. IOS Press, 2009.
Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. QuBE7.0. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):83–88, 2010.
Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning. In Ofer Strichman and Stefan Szeider, editors, Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of LNCS, pages 85–98. Springer, 2010.
Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas. J. Artif. Intell. Res. (JAIR), 26:371–416, 2006.
Alexandra Goultiaeva and Fahiem Bacchus. Recovering and Utilizing Partial Duality in QBF. In Matti Järvisalo and Allen Van Gelder, editors, Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2013), volume 7962 of LNCS, pages 83–99. Springer, 2013.
Alexandra Goultiaeva, Martina Seidl, and Armin Biere. Bridging the gap between dual propagation and CNF-based QBF solving. In Enrico Macii, editor, Proc. of the Int. Conference on Design, Automation and Test in Europe (DATE 2013), pages 811–814. EDA Consortium / ACM DL, 2013.
Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR), 53:127–168, 2015.
Marijn J.H. Heule and Armin Biere. Compositional Propositional Proofs. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Proc. of the 20th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), volume 9450 of LNCS, pages 444–459. Springer, 2015.
Tamir Heyman, Dan Smith, Yogesh Mahajan, Lance Leong, and Husam Abu-Haimed. Dominant Controllability Check Using QBF-Solver and Netlist Optimizer. In Carsten Sinz and Uwe Egly, editors, Proc. of the 17th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2014), volume 8561 of LNCS, pages 227–242. Springer, 2014.
Mikolás Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, and Allen Van Gelder. The QBF Gallery 2014: The QBF Competition at the FLoC Olympic Games. Journal on Satisfiability, Boolean Modeling and Computation, 9:187–206, 2016.
Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1–25, 2016.
Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25–42, 2015.
Mikolás Janota and Joao Marques-Silva. Solving QBF by Clause Selection. In Qiang Yang and Michael Wooldridge, editors, Proc. of the 24th Int. Joint Conference on Artificial Intelligence (IJCAI 2015), pages 325–331. AAAI Press, 2015.
Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing Rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proc. of the 6th Int. Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of LNCS, pages 355–370. Springer, 2012.
Charles Jordan, Lukasz Kaiser, Florian Lonsing, and Martina Seidl. MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. In Carsten Sinz and Uwe Egly, editors, Proc. of the 17th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2014), volume 8561 of LNCS, pages 430–437. Springer, 2014.
Hans Kleine Büning and Uwe Bubeck. Theory of quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 735–760. IOS Press, 2009.
Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for Quantified Boolean Formulas. Inf. Comput., 117(1):12–18, 1995.
William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke. A nonprenex, non-clausal QBF solver with game-state learning. In Ofer Strichman and Stefan Szeider, editors, Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of LNCS, pages 128–142. Springer, 2010.
Reinhold Letz. Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In Uwe Egly and Christian G. Fermüller, editors, Proc. of the Int. Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), volume 2381 of LNCS, pages 160–175. Springer, 2002.
Matthew Lewis, Tobias Schubert, Bernd Becker, Paolo Marin, Massimo Narizzano, and Enrico Giunchiglia. Parallel QBF Solving with Advanced Knowledge Sharing. Fundamenta Informaticae, 107(2-3):139–166, 2011.
Matthew D.T. Lewis, Tobias Schubert, and Bernd Becker. QmiraXT - A Multithreaded QBF Solver. In Carsten Gremzow and Nico Moser, editors, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), pages 7–16. Universitätsbibliothek Berlin, Germany, 2009.
Tao Li and Nan-feng Xiao. Parallel solving model for quantified Boolean formula based on machine learning. Journal of Central South University, 20(11):3156–3165, 2013.
Paolo Liberatore. Redundancy in logic I: CNF propositional formulae. Artif. Intell., 163(2):203–232, 2005.
Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, and Martina Seidl. Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Proc. of the 20th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), volume 9450 of LNCS, pages 418–433. Springer, 2015.
Florian Lonsing and Armin Biere. DepQBF: A Dependency-Aware QBF Solver. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):71–76, 2010.
Florian Lonsing and Armin Biere. Integrating dependency schemes in searchbased QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of LNCS, pages 158–171. Springer, 2010.
Florian Lonsing and Uwe Egly. Incremental QBF Solving. In Barry O’Sullivan, editor, Proc. of the 20th Int. Conference on Principles and Practice of Constraint Programming (CP 2014), volume 8656 of LNCS, pages 514–530. Springer, 2014.
Florian Lonsing, Uwe Egly, and Martina Seidl. Q-Resolution with Generalized Axioms. In Nadia Creignou and Daniel Le Berre, editors, Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of LNCS, pages 435–452. Springer, 2016.
Florian Lonsing, Martina Seidl, and Allen Van Gelder. The QBF Gallery: Behind the scenes. Artif. Intell., 237:92–114, 2016.
Paolo Marin, Christian Miller, Matthew D.T. Lewis, and Bernd Becker. Verification of partial designs using incremental QBF solving. In Wolfgang Rosenstiel and Lothar Thiele, editors, Proc. of the Design, Automation & Test in Europe Conference & Exhibition (DATE 2012), pages 623–628. IEEE, 2012.
Paolo Marin, Massimo Narizzano, Enrico Giunchiglia, Matthew D.T. Lewis, Tobias Schubert, and Bernd Becker. Comparison of knowledge sharing strategies in a parallel QBF solver. In Proc. of the Int. Conference on High Performance Computing & Simulation (HPCS 2009), pages 161–167. IEEE, 2009.
Paolo Marin, Massimo Narizzano, Luca Pulina, Armando Tacchella, and Enrico Giunchiglia. Twelve Years of QBF Evaluations: QSAT Is PSPACE-Hard and It Shows. Fundam. Inform., 149(1-2):133–158, 2016.
Albert R. Meyer and Larry J. Stockmeyer. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. In 13th Annual Symposium on Switching and Automata Theory, pages 125–129. IEEE Computer Society, 1972.
Christian Miller, Paolo Marin, and Bernd Becker. Verification of partial designs using incremental QBF. AI Commun., 28(2):283–307, 2015.
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In Proc. of the 38th Design Automation Conference (DAC 2001), pages 530–535. ACM, 2001.
Benoit Da Mota, Pascal Nicolas, and Igor Stéphan. A new parallel architecture for QBF tools. In Proc. of the Int. Conference on High Performance Computing and Simulation (HPCS 2010), pages 324–330. IEEE, 2010.
Alexander Nadel and Vadim Ryvchin. Efficient SAT Solving under Assumptions. In Alessandro Cimatti and Roberto Sebastiani, editors, Proc. of the 15th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2012), volume 7317 of LNCS, pages 242–255. Springer, 2012.
Knot Pipatsrisawat and Adnan Darwiche. A Lightweight Component Caching Scheme for Satisfiability Solvers. In João Marques-Silva and Karem A. Sakallah, editors, Proc. of the 10th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2007), volume 4501 of LNCS, pages 294–299. Springer, 2007.
David A. Plaisted, Armin Biere, and Yunshan Zhu. A satisfiability procedure for quantified Boolean formulae. Discrete Applied Mathematics, 130(2):291–328, 2003.
Luca Pulina. The Ninth QBF Solvers Evaluation - Preliminary Report. In Proc. of the 4th Int. Workshop on Quantified Boolean Formulas (QBF 2016), volume 1719, pages 1–13. CEUR Workshop Proceedings, 2016.
Markus N. Rabe and Sanjit A. Seshia. Incremental Determinization. In Nadia Creignou and Daniel Le Berre, editors, Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of LNCS, pages 375–392. Springer, 2016.
Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In Roope Kaivola and Thomas Wahl, editors, Proc. of the Int. Conference on Formal Methods in Computer-Aided Design (FMCAD 2015), pages 136–143. IEEE, 2015.
Jussi Rintanen. Improvements to the evaluation of quantified Boolean formulae. In Thomas Dean, editor, Proc. of the 16th Int. Joint Conference on Artificial Intelligence (IJCAI 1999), pages 1192–1197. Morgan Kaufmann, 1999.
Jussi Rintanen. Asymptotically Optimal Encodings of Conformant Planning in QBF. In Proc. of the 22nd AAAI Conference on Artificial Intelligence (AAAI 2007), pages 1045–1050. AAAI Press, 2007.
Thomas J. Schaefer. On the Complexity of Some Two-Person Perfect-Information Games. J. Comput. Syst. Sci., 16(2):185–225, 1978.
Tobias Schubert, Matthew D.T. Lewis, and Bernd Becker. PaMiraXT: Parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation, 6(4):203–222, 2009.
João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 131–153. IOS Press, 2009.
João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Proc. of the Int. Conference on Computer-Aided Design (ICCAD 1996), pages 220–227, 1996.
João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999.
L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time (preliminary report). In Proc. of the 5th Annual ACM Symposium on Theory of Computing (STOC’73), pages 1–9, New York, NY, USA, 1973. ACM.
Larry J. Stockmeyer. The Polynomial-Time Hierarchy. Theor. Comput. Sci., 3(1):1–22, 1976.
Leander Tentrup. Non-prenex QBF Solving Using Abstraction. In Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of LNCS, pages 393–401. Springer, 2016.
Leander Tentrup. Solving QBF by abstraction. CoRR, http://arXiv.org/abs/1604.06752, 2016.
Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. Proceedings of the IEEE, 103(11):2021–2035, 2015.
Siert Wieringa and Keijo Heljanko. Asynchronous Multi-core Incremental SAT Solving. In Nir Piterman and Scott A. Smolka, editors, Proc. of the 19th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 of LNCS, pages 139–153. Springer, 2013.
Ralf Wimmer, Sven Reimer, Paolo Marin, and Bernd Becker. HQSpre - An Effective Preprocessor for QBF and DQBF. In Proc. of the 23rd Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), volume 10205 of LNCS, pages 373–390. Springer, 2017.
Hantao Zhang, Maria Paola Bonacina, and Jieh Hsiang. PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. J. Symb. Comput., 21(4):543–560, 1996.
Lintao Zhang. Solving QBF by Combining Conjunctive and Disjunctive Normal Forms. In Proc. of the 21st Nat. Conference on Artificial Intelligence and the 8th Innov. Applications of Artificial Intelligence Conference (AAAI/IAAI 2006), pages 143–150. AAAI Press, 2006.
Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In Rolf Ernst, editor, Proc. of the Int. Conference on Computer-Aided Design (ICCAD 2001), pages 279–285. IEEE, 2001.
Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean Satisfiability solver. In Lawrence T. Pileggi and Andreas Kuehlmann, editors, Proc. of the Int. Conference on Computer-Aided Design (ICCAD 2002), pages 442–449. ACM / IEEE Computer Society, 2002.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Lonsing, F., Seidl, M. (2018). Parallel Solving of Quantified Boolean Formulas. In: Hamadi, Y., Sais, L. (eds) Handbook of Parallel Constraint Reasoning. Springer, Cham. https://doi.org/10.1007/978-3-319-63516-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-63516-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63515-6
Online ISBN: 978-3-319-63516-3
eBook Packages: Computer ScienceComputer Science (R0)