On the expressive power of unit resolution

TL;DR

This paper investigates the expressive capabilities of unit resolution in propositional logic, characterizing computable functions and revealing limitations in polynomial-time computability due to exponential clause requirements.

Contribution

It introduces the concept of propagatable functions, linking them to monotone circuits, and highlights the exponential complexity in certain polynomial-time functions when using unit resolution.

Findings

Propagatable functions are characterized and linked to monotone circuits.

Some polynomial-time functions require exponential clauses in unit resolution.

Results inform CNF encoding strategies for NP-complete problems.

Abstract

This preliminary report addresses the expressive power of unit resolution regarding input data encoded with partial truth assignments of propositional variables. A characterization of the functions that are computable in this way, which we propose to call propagatable functions, is given. By establishing that propagatable functions can also be computed using monotone circuits, we show that there exist polynomial time complexity propagable functions requiring an exponential amount of clauses to be computed using unit resolution. These results shed new light on studying CNF encodings of NP-complete problems in order to solve them using propositional satisfiability algorithms.