Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Better Extension Variables in DQBF via Independence

Leroy Chew, Tomáš Peitl

TL;DR

This work introduces independent extension variables for DQBF that condition definitions on universal assignments, yielding smaller dependency sets and enabling easier refutations. It formulates the proof system $ abla\mathsf{IndExtFrege}$+$\boldsymbol{\forall}\mathsf{red}$, proving soundness and refutational completeness for S-form DQBFs and establishing line-by-line p-simulations of a broad spectrum of QBF/DQBF techniques such as QRAT, IR($\mathcal{D}^{rrs}$)-calc, Fork Resolution, and G. By allowing extension variables to drop dependencies after conditioning, the approach unifies and strengthens preprocessing and solving strategies across diverse QBF frameworks, potentially enabling broader integration with other inference steps. The results indicate that IndExtFrege+∀red can capture the core power of many existing systems while offering finer control over dependencies, with implications for practical QBF/DQBF solvers and certification workflows. Overall, the paper advances a principled, scalable route to leveraging conditioned extensions to tackle challenging QBF/DQBF problems.

Abstract

We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations. This simple modification instantly solves many challenges in p-simulating the QBF expansion rule, which cannot be p-simulated in proof systems that have strategy extraction. Simulating expansion is even more crucial in DQBF, where other methods are incomplete. In this paper we provide an overview of the strength of this new independent extension rule. We find that a new version of Extended Frege called IndExtFrege+Red can p-simulate a multitude of difficult QBF and DQBF techniques, even techniques that are difficult to approach with ExtFrege+Red. We show six p-simulations, that IndExtFrege+Red p-simulates QRAT, IR(D)-Calc, Q(Drrs)-Res, Fork Resolution, DQRAT and G, which together underpin most DQBF solving and preprocessing techniques. The p-simulations work despite these systems using complicated rules and our new extension rule being relatively simple. Moreover, unlike recent p-simulations by ExtFrege+Red we can simulate the proof rules line by line, which allows us to mix QBF rules more easily with other inference steps.

Better Extension Variables in DQBF via Independence

TL;DR

This work introduces independent extension variables for DQBF that condition definitions on universal assignments, yielding smaller dependency sets and enabling easier refutations. It formulates the proof system +, proving soundness and refutational completeness for S-form DQBFs and establishing line-by-line p-simulations of a broad spectrum of QBF/DQBF techniques such as QRAT, IR()-calc, Fork Resolution, and G. By allowing extension variables to drop dependencies after conditioning, the approach unifies and strengthens preprocessing and solving strategies across diverse QBF frameworks, potentially enabling broader integration with other inference steps. The results indicate that IndExtFrege+∀red can capture the core power of many existing systems while offering finer control over dependencies, with implications for practical QBF/DQBF solvers and certification workflows. Overall, the paper advances a principled, scalable route to leveraging conditioned extensions to tackle challenging QBF/DQBF problems.

Abstract

We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations. This simple modification instantly solves many challenges in p-simulating the QBF expansion rule, which cannot be p-simulated in proof systems that have strategy extraction. Simulating expansion is even more crucial in DQBF, where other methods are incomplete. In this paper we provide an overview of the strength of this new independent extension rule. We find that a new version of Extended Frege called IndExtFrege+Red can p-simulate a multitude of difficult QBF and DQBF techniques, even techniques that are difficult to approach with ExtFrege+Red. We show six p-simulations, that IndExtFrege+Red p-simulates QRAT, IR(D)-Calc, Q(Drrs)-Res, Fork Resolution, DQRAT and G, which together underpin most DQBF solving and preprocessing techniques. The p-simulations work despite these systems using complicated rules and our new extension rule being relatively simple. Moreover, unlike recent p-simulations by ExtFrege+Red we can simulate the proof rules line by line, which allows us to mix QBF rules more easily with other inference steps.

Paper Structure

This paper contains 9 sections, 3 theorems, 2 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Organisation
  4. Preliminaries
  5. Proof systems
  6. (Dependency) Quantified Boolean Formulas
  7. $\mathsf{IndExt\mathsf{Frege}\xspace}$ $\,\raisebox{.2ex}{$+$}\,\boldsymbol{\forall}\mathsf{red}\xspace$, an S-form DQBF proof system
  8. Independent Extension
  9. A Sound and Complete Proof System

Key Result

lemma thmcounterlemma

Suppose $\Pi \phi \wedge L(u)$ is a true S-form DQBF, and $L$ contains no existential variables $x$ such that $u$ is in the dependency set of $x$. Then the S-form DQBF $\Pi \phi \wedge L(u)\wedge L(0)$ is true and the S-form DQBF $\Pi \phi \wedge L(u)\wedge L(1)$ is also true.

Figures (3)

  • Figure 1: The p-simulation structure of refutational QBF proof systems
  • Figure 2: A $\mathsf{Frege}$ system for connectives $0,1, \neg, \rightarrow \vee, \wedge$ .
  • Figure 3: Proof rules of DQBF-IR-calcBeyersdorffBlinkhornChewSchmidtSuda19 .

Theorems & Definitions (6)

  • lemma thmcounterlemma: $\forall$red soundness
  • proof
  • lemma thmcounterlemma
  • proof
  • theorem thmcountertheorem
  • proof