Search

In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

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 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 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 clause-strategy 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 Marques-Silva, 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 co