Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player (countermodels) within the proofs as merge maps. Merge maps are deterministic branching programs in which isomorphism checking is efficient, as a result MRes is a polynomial time verifiable proof system.
In this paper, we introduce a family of proof systems MRes-R in which the information of countermodels are stored in any pre-fixed complete representation R. Hence, corresponding to each possible complete representation R, we have a sound and refutationally complete QBF-proof system in MRes-R. To handle these arbitrary representations, we introduce consistency checking rules in MRes-R instead of the isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable (Non-P). Consequently, the paper shows that using merge maps is too restrictive and with a slight change in rules, it can be replaced with arbitrary representations leading to several interesting proof systems.
We relate these new systems with the implicit proof system from the algorithm in [Blinkhorn et al. SAT.'2021], which was designed to solve DQBFs (Dependency QBFs) using MRes like clause-strategy pairs. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in the paper and deduce that `Ordered' versions of the proof systems in MRes-R are indeed polynomial time verifiable.
On the lower bound side, we lift the lower bound result of regular MRes ([Beyersdorff et al. FSTTCS.'2020]) by showing that the completion principle formulas (CR_n) from [Jonata et al. Theor. Comput. Sci.'2015] which are shown to be hard for regular MRes in [Beyersdorff et al. FSTTCS.'2020], are also hard for any regular proof system in MRes-R. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use some complete representations, including those undiscovered, instead of only merge maps. Thereby proving that the hardness of CR_n formulas is intact even after changing the weak isomorphism checking in MRes to the stronger consistency checking in MRes-R.
Updated the contributions and motivation.
Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player within the proofs. Every line of this proof system consists of existential clauses along with countermodels. MRes stores the countermodels as merge maps. Merge maps are deterministic branching programs in which isomorphism checking is efficient as a result MRes is a polynomial time verifiable proof system.
In this paper, we introduce a family of proof systems MRes-$\mathcal{R}$ in which, the information of countermodels are stored in any pre-fixed complete representation $\mathcal{R}$, instead of merge maps. Hence corresponding to each possible complete representation $\mathcal{R}$, we have a sound and refutationally complete QBF-proof system in MRes-$\mathcal{R}$. To handle arbitrary representations for the strategies, we introduce consistency checking rules in MRes-$\mathcal{R}$ instead of isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable. Consequently, the paper shows that using merge maps is too restrictive and can be replaced with arbitrary representations leading to several interesting proof systems.
The paper also studies proof theoretic properties of the family of new proof systems MRes-$\mathcal{R}$. We show that eFrege+$\forall$red simulates all valid refutations from proof systems in MRes-$\mathcal{R}$. Since proof systems in MRes-$\mathcal{R}$ may use arbitrary representations, in order to simulate them, we first represent the steps used by the proof systems as a new simple complete structure. As a consequence, the corresponding proof system belonging to MRes-$\mathcal{R}$ is able to simulate all proof systems in MRes-$\mathcal{R}$. Finally, we simulate this proof system via eFrege+$\forall$red using the ideas from [Chew et al. ECCC.'2021].
On the lower bound side, we lift the lower bound result of regular MRes ([Beyersdorff et al. FSTTCS.'2020]) for all regular proof systems in MRes-$\mathcal{R}$. To be precise, we show that the completion principle formulas from [Jonata et al. Theor. Comput. Sci.'2015] which are shown to be hard for regular MRes in [Beyersdorff et al. FSTTCS.'2020], are also hard for any regular proof system in MRes-$\mathcal{R}$. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use some complete representation, including those undiscovered, instead of merge maps.