# Automating Resolution is NP-Hard

## TL;DR

This paper proves that finding optimal Resolution refutations is NP-hard, indicating that Resolution proof systems cannot be efficiently automated unless P equals NP, with implications for proof complexity and automated theorem proving.

## Contribution

It establishes the NP-hardness of approximating Resolution refutations within polynomial bounds, highlighting fundamental computational limitations in proof automation.

## Key findings

- Resolution is NP-hard to approximate within polynomial bounds
- Distinguishing formulas with polynomial vs. subexponential refutations is NP-hard
- Resolution cannot be automatized in subexponential or quasi-polynomial time unless NP is in SUBEXP or QP

## Abstract

We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, we show it is NP-hard to distinguish between formulas that have Resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that Resolution is not automatizable in subexponential time or quasi-polynomial time unless NP is included in SUBEXP or QP, respectively.