Incremental QBF Solving

Abstract

We consider the problem of incrementally solving a sequence of quantified Boolean formulae (QBF). Incremental solving aims at using information learned from one formula in the process of solving the next formulae in the sequence. Based on a general overview of the problem and related challenges, we present an approach to incremental QBF solving which is application-independent and hence applicable to QBF encodings of arbitrary problems. We implemented this approach in our incremental search-based QBF solver DepQBF and report on implementation details. Experimental results illustrate the potential benefits of incremental solving in QBF-based workflows.

revision (camera-ready, to appear in the proceedings of CP 2014, LNCS, Springer)

References in corpus (2)

• Conformant Planning as a Case Study of Incremental QBF Solving
• SAT-Based Synthesis Methods for Safety Specs

Cited by in corpus (6)

• DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
• The Second Reactive Synthesis Competition (SYNTCOMP 2015)
• Conformant Planning as a Case Study of Incremental QBF Solving
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
• Automated Benchmarking of Incremental SAT and QBF Solvers