Lifting QBF Resolution Calculi to DQBF

Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    151 Downloads (Pure)

    Abstract

    We examine existing resolution systems for quantifed Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Res < IR-calc < IRM-calc, the situation is quite different in DQBF. The obvious adaptations of Q-Res and likewise universal resolution are too weak: they are not complete. The obvious adaptation of IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance resolution. Conceptually, we use the relation of DQBF to effectively propositional logic (EPR) and explain our new DQBF calculus based on IR-calc as a subsystem of frst-order resolution.
    Original languageEnglish
    Title of host publication Theory and Applications of Satisfiability Testing – SAT 2016
    Subtitle of host publication19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
    EditorsNadia Creignou, Daniel Le Berre
    PublisherSpringer Nature
    Pages490-499
    Number of pages10
    Volume9710
    ISBN (Electronic)978-3-319-40970-2
    ISBN (Print)978-3-319-40969-6
    DOIs
    Publication statusPublished - 2016

    Fingerprint

    Dive into the research topics of 'Lifting QBF Resolution Calculi to DQBF'. Together they form a unique fingerprint.

    Cite this