Computing Shortest Resolution Proofs

Abstract

Propositional resolution is a powerful proof system for unsatisfiable propositional formulas in conjunctive normal form. Resolution proofs represent useful explanations of infeasibility, with important applications. This motivates the challenge of computing shortest resolution proofs, i.e. those with the smallest number of inference steps. This paper proposes a SAT-based approach for this problem. Concretely, the paper investigates new propositional encodings for computing shortest resolution proofs and devises a number of optimizations, including symmetry breaking, additional constraints on the structure of proofs, as well as exploiting related concepts in infeasibility analysis, such as minimal correction subsets. Experimental results show the suitability of the proposed approach.