Abstract Solvers for Quantified Boolean Formulas and their Applications

solvers are a graph-based representation employed in many research areas, such as SAT, SMT and ASP, to model, analyze and compare search algorithms in place of pseudo-code-based representations. Such an uniform, formal way of presenting the solving algorithms proved effective for their understanding, for formalizing related formal properties and also for combining algorithms in order to design new solving procedures. In this paper we present abstract solvers for Quantified Boolean Formulas (QBFs). They include a direct extension of the abstract solver describing the DPLL algorithm for SAT, and an alternative formulation inspired by the two-layers architecture employed for the analysis of disjunctive ASP solvers. We finally show how these abstract solvers can be directly employed for designing solving procedures for reasoning tasks which can be solved by means of reduction to a QBF.