Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations

Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic*, Martina Seidl, Florian Lonsing, Uwe Egly

*Korrespondierende/r Autor/in für diese Arbeit

Publikation: Beitrag in einer FachzeitschriftArtikelBegutachtung

Abstract

In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the ∀Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.
Originalspracheenglisch
Seiten (von - bis)157-177
Seitenumfang21
FachzeitschriftFormal Methods in System Design
Jahrgang57
Ausgabenummer2
DOIs
PublikationsstatusVeröffentlicht - 23 Aug 2021

ASJC Scopus subject areas

  • Software
  • Theoretische Informatik
  • Hardware und Architektur

Fingerprint

Untersuchen Sie die Forschungsthemen von „Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren