Lemma and model caching in decision procedures for quantified Boolean formulas. The increasing role of quantified Boolean logic in many applications calls for practically efficient decision procedures. One of the most promising paradigms is the semantic tree format implemented in the style of the DPLL procedure. In this paper, so-called learning techniques like intelligent backtracking and caching of lemmas which proved useful in the pure propositional case are generalised to the quantified Boolean case and the occuring differences are discussed. Due to the strong restriction of the variable selection in semantic tree procedures for quantified Boolean formulas, learning methods are more important than in the propositional case, as we demonstrate. Furthermore, in addition to the caching of lemmas, significant advances can be achieved by techniques based on the caching of models, too. The theoretical effect of these improvements is illustrated by a comparison of the search spaces on pathological examples. We also describe the basic features of the system Semprop, which is an efficient implementation of (some of) the developed techniques, and give the results of an experimental evaluation of the system on a number of practical examples.

References in zbMATH (referenced in 17 articles , 1 standard article )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Das, Anupam: From QBFs to \textsfMALLand back via focussing (2020)
  2. Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
  3. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  4. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  5. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  6. Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
  7. Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
  8. Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
  9. Kumar, Ramana; Weber, Tjark: Validating QBF validity in HOL4 (2011)
  10. Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
  11. Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
  12. Arieli, Ofer; Denecker, Marc; Van Nuffelen, Bert; Bruynooghe, Maurice: Computational methods for database repair by signed formulae (2006)
  13. Egly, Uwe; Pichler, Reinhard; Woltran, Stefan: On deciding subsumption problems (2005)
  14. Johannsen, Jan: The complexity of pure literal elimination (2005)
  15. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in sat-based formal verification (2005) ioport
  16. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in SAT-based formal verification (2005) ioport
  17. Letz, Reinhold: Lemma and model caching in decision procedures for quantified Boolean formulas (2002)