Symmetry-breaking answer set solving

Issue title: Answer Set Programming

Article type: Research Article

Authors: Drescher, Christian | Tifrea, Oana | Walsh, Toby

Affiliations: NICTA and University of New South Wales, Sydney, Australia. E-mails: {christian.drescher, toby.walsh}@nicta.com.au | Computer Science Faculty, Free University of Bozen-Bolzano, Bolzano, Italy. E-mail: [email protected]

Abstract: We investigate the role of symmetry detection and symmetry breaking in answer set programming to eliminate symmetric parts of the search space and, thereby, simplify the solution process. We reduce symmetry detection to a graph automorphism problem which allows us to extract symmetries of a logic program from the symmetries of the constructed coloured graph. The correctness of our reduction is proven. We also propose an encoding of symmetry-breaking constraints in terms of permutation cycles and use only generators in this process to implicitly represent symmetries with exponential compression. These ideas are formulated as preprocessing and implemented in a completely automated flow that first detects symmetries from a given answer set program, adds symmetry-breaking constraints, and can be applied to any existing answer set solver. We demonstrate computational impact on benchmarks versus direct application of the solver.

Keywords: Answer set programming, symmetry breaking, graph automorphism problem

DOI: 10.3233/AIC-2011-0495

Journal: AI Communications, vol. 24, no. 2, pp. 177-194, 2011