Comparing Different Prenexing Strategies for Quantified Boolean Formulas

Uwe Egly, Martina Seidl, Hans Tompits, Stefan Woltran, M. Zolda

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

    27 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationTheory and Applications of Satisfiability Testing
    EditorsEnrico Giunchiglia, Armando Tacchella
    PublisherSpringer Nature
    Number of pages15
    ISBN (Electronic)978-3-540-24605-3
    ISBN (Print)978-3-540-20851-8
    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


    Conference6th Int Conf, SAT 2003
    CitySanta Margherita Ligure


    Dive into the research topics of 'Comparing Different Prenexing Strategies for Quantified Boolean Formulas'. Together they form a unique fingerprint.

    Cite this