Abstract
Answer-set programs become more expressive if extended by cardinality rules. Certain implementation techniques, however, presume the translation of such rules back into normal rules. This has been previously realized using a BDD-based transformation which may produce a quadratic number of rules in the worst case. In this paper, we present two further constructions which are based on Boolean circuits for merging and sorting and which have been considered, e.g., in the context of the propositional satisfiability (SAT) problem and its extensions. Such circuits can be used to express cardinality constraints in a more compact way. Thus, in order to normalize cardinality rules, we first develop an ASP encoding of a sorting circuit, on top of which the second translation, one encoding a selection circuit, is devised. Because sorting is more general than cardinality checking, we also present ways to prune the resulting sorting and selection programs. The experimental part illustrates the compactness of the new normalizations and points out cases where computational performance is improved.
The support from the Finnish Centre of Excellence in Computational Inference Research (COIN) funded by the Academy of Finland (under grant #251170) is gratefully acknowledged.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)
Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo Boolean constraints to SAT. JSAT 2(1-4), 191–200 (2006)
Batcher, K.: Sorting networks and their applications. In: AFIPS Spring Joint Computer Conference, pp. 307–314. ACM (1968)
Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Communications of the ACM 54(12), 92–103 (2011)
Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 154–172. Springer, Heidelberg (2010)
Denecker, M., Vennekens, J., Bond, S., Gebser, M., Truszczyński, M.: The second answer set programming competition. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 637–654. Springer, Heidelberg (2009)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4), 1–26 (2006)
Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187, 52–89 (2012)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proceedings of ICLP 1988, pp. 1070–1080 (1988)
Giunchiglia, E., Lierler, Y., Maratea, M.: Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36(4), 345–377 (2006)
Janhunen, T., Niemelä, I.: Compact translations of non-disjunctive answer set programs to propositional clauses. In: Balduccini, M., Son, T.C. (eds.) Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning. LNCS, vol. 6565, pp. 111–130. Springer, Heidelberg (2011)
Janhunen, T., Niemelä, I.: Applying visible strong equivalence in answer-set program transformations. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds.) Correct Reasoning. LNCS, vol. 7265, pp. 363–379. Springer, Heidelberg (2012)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Transactions on Computational Logic 2(4), 526–541 (2001)
Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157(1-2), 115–137 (2004)
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138(1-2), 181–234 (2002)
Woltran, S.: A common view on strong, uniform, and other notions of equivalence in answer-set programming. Theory and Practice of Logic Programming 8(2), 217–234 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bomanson, J., Janhunen, T. (2013). Normalizing Cardinality Rules Using Merging and Sorting Constructions. In: Cabalar, P., Son, T.C. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2013. Lecture Notes in Computer Science(), vol 8148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40564-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-40564-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40563-1
Online ISBN: 978-3-642-40564-8
eBook Packages: Computer ScienceComputer Science (R0)