University of Hertfordshire

Comparing Different Prenexing Strategies for Quantified Boolean Formulas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Uwe Egly
  • Martina Seidl
  • Hans Tompits
  • Stefan Woltran
  • M. Zolda
View graph of relations
Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing
EditorsEnrico Giunchiglia, Armando Tacchella
PublisherSpringer
Pages214-228
Number of pages15
ISBN (Electronic)978-3-540-24605-3
ISBN (Print)978-3-540-20851-8
DOIs
Publication statusPublished - 2004
Event6th Int Conf, SAT 2003 - Santa Margherita Ligure, Italy
Duration: 5 May 20038 May 2003

Publication series

NameLecture Notes in Computer Science
Volume2919

Conference

Conference6th Int Conf, SAT 2003
CountryItaly
CitySanta Margherita Ligure
Period5/05/038/05/03

Abstract

The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a prepositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not.

Research outputs

ID: 1343912