You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

CAQE and QuAbS: Abstraction Based QBF Solvers

Issue title: SAT 2018 Competitions and Evaluations

Guest editors: Martina Seidl and Luca Pulina

Article type: Research Article

Authors: Tentrup, Leander; *

Affiliations: Reactive Systems Group, Saarland University. E-mail: [email protected]

Note: [*] This work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center ‘Foundations of Perspicuous Software Systems’ (TRR 248, 389792660) and by the European Research Council (ERC) Grant OSARES (No. 683300).

Keywords: QBF solver, certification, conjunctive normal form, negation normal form

DOI: 10.3233/SAT190121

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 155-210, 2019

Received 1 November 2018
|
Revision received 1 April 2019
|
Published: 1 September 2019
Get PDF open access

Abstract

We present a detailed description, analysis, and evaluation of the clausal abstraction approach for solving quantified Boolean formulas (QBF). The clausal abstraction algorithm started as a solving algorithm for QBFs in prenex conjunctive normal form (PCNF) incorporating an efficient Skolem and Herbrand function extraction. Extracting witnesses from solving is especially important as it enables the certification of the solver’s verdict and it is the foundation for applications built on QBF, like verification and synthesis. Later, the algorithmic ideas were extended to non-prenex and negation normal form formulas, leading the way for improved performance in solving and function extraction. The implementations of the algorithms in the solvers CAQE and QuAbS won the QBF competition (QBFEVAL’18) in their respective categories, prenex CNF and prenex non-CNF.

Show more