Unit contradiction versus unit propagation

TL;DR

This paper explores two models of unit resolution in CNF formulas, demonstrating they can compute the same functions efficiently and relating this to Boolean constraint encoding.

Contribution

It establishes the equivalence of two models of unit resolution for computing functions and analyzes their relation to CNF encodings of Boolean constraints.

Findings

Both models can compute the same functions with polynomially related formula sizes

The results connect unit resolution behavior to CNF encoding strategies

The study clarifies the computational power of unit resolution in propositional logic

Abstract

Some aspects of the result of applying unit resolution on a CNF formula can be formalized as functions with domain a set of partial truth assignments. We are interested in two ways for computing such functions, depending on whether the result is the production of the empty clause or the assignment of a variable with a given truth value. We show that these two models can compute the same functions with formulae of polynomially related sizes, and we explain how this result is related to the CNF encoding of Boolean constraints.