Abstract
Many research works had been done in order to define a semantics for logic programs. The well know is the stable model semantics which selects for each program one of its canonical models. The stable models of a logic program are in a certain sens the minimal Herbrand models of its reduct programs. On the other hand, the notion of symmetry elimination had been widely studied in constraint programming and shown to be useful to increase the efficiency of the associated solvers. However symmetry in non monotonic reasoning still not well studied in general. For instance Answer Set Programming (ASP) is a very known framework but only few recent works on symmetry breaking are known in this domain. Ignoring symmetry breaking in the answer set systems could make them doing redundant work and lose on their efficiency. Here we study the notion of local and global symmetry in the framework of answer set programming. We show how local symmetries of a logic program can be detected dynamically by means of the automorphisms of its graph representation. We also give some properties that allow to eliminate theses symmetries in SAT-based answer set solvers and show how to integrate this symmetry elimination in these methods in order to enhance their efficiency.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Aloul, F.A., Ramani, A., Markov, I.L., Sakallak, K.A.: Solving difficult sat instances in the presence of symmetry. In: DAC, pp. 1117–1137 (2003)
Aloul, F.A., Ramani, A., Markov, I.L., Sakallak, K.A.: Symmetry breaking for pseudo-boolean satisfiability. In: ASPDAC 2004, pp. 884–887 (2004)
Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: The Proceedings of the 39th Design Automation Conference (DAC 2002), pp. 731–736. ACM Press (2002)
Benhamou, B.: Study of symmetry in constraint satisfaction problems. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 246–254. Springer, Heidelberg (1994)
Benhamou, B., Sais, L.: Theoretical study of symmetries in propositional calculus and application. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 281–294. Springer, Heidelberg (1992)
Benhamou, B., Sais, L.: Tractability through symmetries in propositional calculus. The Journal of Automated Reasoning 12, 89–102 (1994)
Benhamou, B., Nabhani, T., Ostrowski, R., Saïdi, M.R.: Dynamic symmetry detection and elimination in the satisfiability problem. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, Dakar, Senegal, April 25-May 1 (2010)
Benhamou, B., Nabhani, T., Siegel, P.: Reasoning by symmetry in non-monotonic inference. In: The Proceedings of the International Conference on Machine and Web Intelligence (ICMWI 2010), Algiers, Algeria, pp. 264–269 (October 3, 2010)
Benhamou, B., Nabhani, T., Siegel, P.: Reasoning by symmetry in non-monotonic logics. In: 13th International Workshop on Non-Monotonic Reasoning (NMR 2010) (May 14, 2010)
Benhamou, B., Saïdi, M.R.: Local symmetry breaking during search in cSPs. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 195–209. Springer, Heidelberg (2007)
Benhamou, B., Siegel, P.: Symmetry and non-monotonic inference. In: The Proceedings of Symcon 2008, Sydney, Australia (September 2008)
Besnard, P., Siegel, P.: The preferential-models approach in nonmonotonic logics - in non-standard logic for automated reasoning. In: Smets, P. (ed.) Academic Press, pp. 137–156 (1988)
Bossu, G., Siegel, P.: Nonmonotonic reasoning and databases. In: Advances in Database Theory, pp. 239–284 (1982)
Bossu, G., Siegel, P.: Saturation, nonmonotonic reasoning and the closed-world assumption. Artif. Intell. 25(1), 13–63 (1985)
Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and data bases, pp. 293–322 (1978)
Crawford, J., Ginsberg, M.L., Luck, E., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148–159 (1996)
Davis, M., Logemann, G.W., Loveland, D.W.: A machine program for theorem proving. Journal of Communications of The ACM - CACM 5(7), 394–397 (1962)
Drescher, C., Tifrea, O., Walsh, T.: Symmetry-breaking answer set solving. AI Commun. 24(2), 177–194 (2011)
Drescher, C., Tifrea, O., Walsh, T.: Symmetry-breaking in answer set solving. In: ICLP 2010 Workshop ASPOCP 2010 (2010)
Erdem, E., Lifschitz, V.: Tight logic programs. Thoery and Practice of Logic Programming 3, 499–518 (2003)
Fages, F.: Consistency of Clark’s completion and existence of stable models. Journal of Methods of Logic Programming in Computer Sciences 1, 51–60 (1994)
Freuder, E.: Eliminating interchangeable values in constraints satisfaction problems. In: AAAI 1991, pp. 227–233 (1991)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Advanced pre-processing for answer set solving. In: Proceedings of the 18th European Conference on Artificial Intelligence, pp. 15–19. IOS Press, Amsterdam (2008)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: A conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 260–265. Springer, Heidelberg (2007)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kawalski, R., Bowen, K. (eds.) Logic Programming: Fifth Int’l Conf. and Symp., pp. 1070–1080 (1988)
Giunchiglia, E., Lierler, Y., Maratea, M.: Sat-based answer set programming. In: 19th National Conference on Artificial Intelligence, July 25-29. AAAI, San Jose (2004)
Haselbck, A.: Exploiting interchangeabilities in constraint satisfaction problems. IJCAI 93, 282–289 (1993)
Kraus, S., Lehmann, D.J., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artificial Intelligence 44(1-2), 167–207 (1990)
Krishnamurty, B.: Short proofs for tricky formulas. Acta Inf. (22), 253–275 (1985)
Lierler, Y., Maratea, M.: Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 346–350. Springer, Heidelberg (2003)
Lin, F., Zhao, Y.: Assat: Computing answer sets of a logic program by sat solver. In: Proceedings of AAAI 2002 (2002)
McKay, B.: Practical graph isomorphism. Congr. Numer. 30, 45–87 (1981)
Mears, C., de la Banda, M.G., Wallace, M.: On implementing symmetry detection. In: Proceedings of SymCon 2006, pp. 1–8 (2006)
Montanari, U.: Networks of constraints: Fundamental properties and applications to picture processing. Information Science 7, 95–132 (1974)
Puget, J.-F.: Automatic detection of variable and value symmetries. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 475–489. Springer, Heidelberg (2005)
Puget, J.F.: On the satisfiability of symmetrical constrained satisfaction problems. In: Komorowski, J., Raś, Z.W. (eds.) ISMIS 1993. LNCS (LNAI), vol. 689, Springer, Heidelberg (1993)
Reiter, R.: A logic for default reasoning. Artificial Intelligence 13, 81–132 (1980)
Siegel, P., Forget, L., Risch, V.: Preferential logics are x-logics. Journal of Logic and Computation 11(1), 71–83 (2001)
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
Benhamou, B. (2013). Dynamic and Static Symmetry Breaking in Answer Set Programming. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)