Hardness measures and resolution lower bounds

TL;DR

This paper provides a unified framework for various hardness measures in resolution proof systems, extending them to all clause-sets and offering insights into proof complexity and SAT solving hardness.

Contribution

It introduces a unified view of multiple hardness measures and extends these concepts to all clause-sets, enhancing understanding of resolution proof complexity.

Findings

Unified view of width, space, and size measures

Extension of hardness measures to all clause-sets

Theoretical insights into proof complexity and SAT hardness

Abstract

Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this report we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. We also extend these measures to all clause-sets (possibly satisfiable).