Unified characterisations of resolution hardness measures

ABSTRACT. Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanation for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size.

As our main contribution we obtain combinatorial characterisations of these hardness measures. Our characterisations are both in terms of Prover-Delayer games and of sets of partial assignments with some consistency strength. These unified characterisations allow elegant proofs of relations between the different hardness measures. In particular, we obtain a generalised version of Atserias and Dalmau's result on the relation between resolution width and space from (J. Comput. Syst. Sci. 2008). Our results do not only hold for unsatisfiable instances, but also transfer to the satisfiable case, for which little is known regarding hardness measures.