Abstract
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ï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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. of Artif. Intel. Research (JAIR) 40, 353–373 (2011); preliminary version in SAT 2009
Bacchus, F.: GAC Via Unit Propagation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133–147. Springer, Heidelberg (2007)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. of the ACM 48(2), 149–169 (2001)
Bessiere, C., Katsirelos, G., Narodytska, N., Quimper, C.G., Walsh, T.: Decompositions of all different, global cardinality and related constraints. In: Int. Joint. Conf. on Artif. Intel. (IJCAI), pp. 419–424 (2009)
Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Int. Joint. Conf. on Artif. Intel. (IJCAI), pp. 412–418 (2009)
Brand, S., Narodytska, N., Quimper, C.-G., Stuckey, P.J., Walsh, T.: Encodings of the Sequence Constraint. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 210–224. Springer, Heidelberg (2007)
Cadoli, M., Donini, F., Liberatore, P., Schaerf, M.: Preprocessing of intractable problems. Information and Computation 176, 89–120 (2002)
Darwiche, D., Marquis, P.: A knowledge compilation map. J. of Artif. Intel. Research (JAIR) 17, 229–264 (2002)
Feydy, T., Stuckey, P.J.: Lazy Clause Generation Reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352–366. Springer, Heidelberg (2009)
Gent, I.P.: Arc consistency in SAT. In: Euro. Conf. on Artif. Intel. (ECAI), pp. 121–125 (2002)
Huang, J.: Universal Booleanization of Constraint Models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144–158. Springer, Heidelberg (2008)
Marquis, P., Sadaoui, S.: A new algorithm for computing theory prime implicates compilations. In: Conf. on Artif. Intel. (AAAI), pp. 504–509 (1996)
Marquis, P.: Knowledge compilation using theory prime implicates. In: IJCAI, pp. 837–845 (1995)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intel. 175(2), 512–525 (2011); preliminary works in AAAI 2008 (notion of empowerment) and CP (2009)
Quimper, C.G., Walsh, T.: Decompositions of grammar constraints. In: Conf. on Artif. Intel. (AAAI), pp. 1567–1570 (2008)
del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Knowledge Representation and Reasoning (KR), pp. 551–561 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bordeaux, L., Marques-Silva, J. (2012). Knowledge Compilation with Empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds) SOFSEM 2012: Theory and Practice of Computer Science. SOFSEM 2012. Lecture Notes in Computer Science, vol 7147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27660-6_50
Download citation
DOI: https://doi.org/10.1007/978-3-642-27660-6_50
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27659-0
Online ISBN: 978-3-642-27660-6
eBook Packages: Computer ScienceComputer Science (R0)