Olivier Bailleux
On the expressive power of unit resolution.
Mon, 06/20/2011 - 15:01 — SomNambulAuthors: Olivier Bailleux
Subjects: Artificial Intelligence
AbstractThis 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.On the CNF encoding of cardinality constraints and beyond.
Mon, 12/20/2010 - 16:01 — SomNambulAuthors: Olivier Bailleux
Subjects: Artificial Intelligence
AbstractIn this report, we propose a quick survey of the currently known techniques
for encoding a Boolean cardinality constraint into a CNF formula, and we
discuss about the relevance of these encodings. We also propose models to
facilitate analysis and design of CNF encodings for Boolean constraints.
User login
