Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>

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 ... more >>>

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, ... more >>>