A Little Blocked Literal Goes a Long Way

Q-resolution is a generalization of propositional resolution that provides the theoretical foundation for search-based solvers of quantified Boolean formulas (QBFs). Recently, it has been shown that an extension of Q-resolution, called long-distance resolution, is remarkably powerful both in theory and in practice. However, it was unknown how long-distance resolution is related to ��������, a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that �������� polynomially simulates long-distance resolution. Two simple rules of �������� are crucial for our simulation—blocked-literal addition and blocked-literal elimination. Based on the simulation, we implemented a tool that transforms long-distance-resolution proofs into �������� proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding �������� proofs.