Abstract
Merge Resolution (MRes [Olaf Beyersdorff et al., 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ℛ in which the information of countermodels are stored in any prefixed complete representation ℛ. Hence, corresponding to each possible complete representation ℛ, we have a sound and refutationally complete QBFproof system in MResℛ. To handle these arbitrary representations, we introduce consistency checking rules in MResℛ instead of the isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable (NonP). 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 [Joshua Blinkhorn et al., 2021], which was designed to solve DQBFs (Dependency QBFs) using clausestrategy pairs like MRes. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in [Joshua Blinkhorn et al., 2021] and deduce that "Ordered" versions of the proof systems in MResℛ are indeed polynomial time verifiable.
On the lower bound side, we lift the lower bound result of regular MRes ([Olaf Beyersdorff et al., 2020]) by showing that the completion principle formulas (CR_n) from [Mikolás Janota and João MarquesSilva, 2015] which are shown to be hard for regular MRes in [Olaf Beyersdorff et al., 2020], are also hard for any regular proof system in MResℛ. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use various 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ℛ.
BibTeX  Entry
@InProceedings{chede_et_al:LIPIcs.STACS.2023.21,
author = {Chede, Sravanthi and Shukla, Anil},
title = {{Extending Merge Resolution to a Family of QBFProof Systems}},
booktitle = {40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
pages = {21:121:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772662},
ISSN = {18688969},
year = {2023},
volume = {254},
editor = {Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17673},
URN = {urn:nbn:de:0030drops176737},
doi = {10.4230/LIPIcs.STACS.2023.21},
annote = {Keywords: Proof complexity, QBFs, Merge Resolution, Simulation, Lower Bound}
}
Keywords: 

Proof complexity, QBFs, Merge Resolution, Simulation, Lower Bound 
Collection: 

40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023) 
Issue Date: 

2023 
Date of publication: 

03.03.2023 