Unit contradiction versus unit propagation
This work addresses theoretical aspects of SAT solving for researchers in computational logic, but it appears incremental as it builds on existing formalizations of unit resolution.
The paper tackles the problem of formalizing unit resolution outcomes in CNF formulas by comparing two computational models—unit contradiction and unit propagation—and shows they can compute the same functions with polynomially related formula sizes, relating this to Boolean constraint encoding.
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.