Home // ADVCOMP 2010, The Fourth International Conference on Advanced Engineering Computing and Applications in Sciences // View article

Using Autarky to Evaluate Quantified Boolean Formulae

Authors:
Jens Rühmkorf

Keywords: Autarky; Davis-Putnam; SAT; QBF

Abstract:
In this paper, we discuss algorithmical implications for the extension of autarky from propositional logic to evaluate quantified boolean formulae (QBF). First, the Davis-Putnam procedure for the satisfiability problem (SAT) is described. Then we explain efficient known data structures for SAT and extensions to QBF which we used in our solver. Finally, we introduce the concept of autarky and describe how detecting 2-autarky structures in a given QBF formula helps pruning the search tree. To the best of our knowledge we are the first to describe such techniques for QBF.

Pages: 154 to 159

Copyright: Copyright (c) IARIA, 2010

Publication date: October 25, 2010

Published in: conference

ISSN: 2308-4499

ISBN: 978-1-61208-101-4

Location: Florence, Italy

Dates: from October 25, 2010 to October 30, 2010