Better Extension Variables in DQBF via Independence

TL;DR

This paper introduces a generalized extension variable concept in DQBF that simplifies refutations and enhances proof system simulations, significantly improving the ability to handle complex QBF and DQBF techniques.

Contribution

It proposes a new independent extension rule that reduces dependency sets, enabling better p-simulation of various proof systems and techniques in QBF and DQBF.

Findings

IndExtFrege+Red p-simulates multiple complex proof systems.

The new rule simplifies refutations and proof simulations.

Line-by-line proof rule simulation enables flexible proof composition.

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.