Reified unit resolution and the failed literal rule

TL;DR

This paper demonstrates that the failed literal rule in SAT solving can be fully simulated by unit resolution through the construction of a reified formula, revealing new insights into the expressive power of unit resolution.

Contribution

It introduces a polynomial-size reified formula that simulates any CNF formula's unit resolution process, showing that the failed literal rule is redundant.

Findings

Failed literal rule can be simulated by unit resolution

Reified formulas are polynomially related in size to original formulas

Provides new insights into the expressive power of unit resolution

Abstract

Unit resolution can simplify a CNF formula or detect an inconsistency by repeatedly assign the variables occurring in unit clauses. Given any CNF formula sigma, we show that there exists a satisfiable CNF formula psi with size polynomially related to the size of sigma such that applying unit resolution to psi simulates all the effects of applying it to sigma. The formula psi is said to be the reified counterpart of sigma. This approach can be used to prove that the failed literal rule, which is an inference rule used by some SAT solvers, can be entirely simulated by unit resolution. More generally, it sheds new light on the expressive power of unit resolution.