Extending Merge Resolution to a Family of QBF-Proof Systems

Merge Resolution ( MRes [ 6 ]) 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 article, we introduce a family of proof systems MRes- ℛ in which the information of countermodels is stored in any pre-fixed complete representation ℛ. Hence, corresponding to each possible complete representation ℛ, we have a sound and refutationally complete QBF-proof 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 (Non-P). Consequently, the article 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 [ 11 ], which was designed to solve DQBFs (Dependency QBFs) using clause-strategy pairs like MRes . We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in [ 11 ] and deduce that ‘ordered’ version of the proof systems in MRes- ℛ along with some additional restrictions are polynomial time verifiable. Demonstrating the strength of these systems, we show that the regular versions of systems in MRes- ℛ are exponentially stronger than regular MRes . We also lift the lower bound result of regular MRes ([ 7 ]) by showing that the completion principle formulas ( CR n ) from [ 25 ] which are shown to be hard for regular MRes in [ 7 ], are also hard for any regular proof system in MRes- ℛ. Therefore, the article 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- ℛ.