06046562

a

06046562 Bordeaux, Lucas Marques-Silva, Joao Knowledge compilation with empowerment. Bielikov\'a, M\'aria (ed.) et al., SOFSEM 2012: Theory and practice of computer science. 38th conference on current trends in theory and practice of computer science, \v{S}pindler{\uu}v Ml\'yn, Czech Republic, January 21--27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27659-0/pbk). Lecture Notes in Computer Science 7147, 612-624 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-27660-6_50

Summary: When we encode constraints as Boolean formulas, a natural question is whether the encoding ensures a ``propagation completeness'' property: is the basic unit propagation mechanism able to deduce all the literals that are logically valid? We consider the problem of automatically finding encodings with this property. Our goal is to compile a na{\"\i}ve definition of a constraint into a good, propagation-complete encoding. Well-known Knowledge Compilation techniques from AI can be used for this purpose, but the constraints for which they can produce a polynomial size encoding are few. We show that the notion of empowerment recently introduced in the SAT literature allows producing encodings that are shorter than with previous techniques, sometimes exponentially.