6533b7ddfe1ef96bd12754af

RESEARCH PRODUCT

Unit contradiction versus unit propagation

Olivier Bailleux

subject

FOS: Computer and information sciencesArtificial Intelligence (cs.AI)TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESComputer Science - Artificial IntelligenceComputer Science::Logic in Computer ScienceComputer Science::Computational Complexity

description

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.

yearjournalcountryeditionlanguage
2012-04-03
http://arxiv.org/abs/1204.0731