Exploiting Symmetry in Model Expansion for Predicate and Propositional Logic

Many combinatorial problems exhibit symmetry, a transformational property that does not fundamentally alter the nature of a problem. For instance, renaming a set of identical trucks in a routing problem, mirroring or rotating a chessboard onto itself, or the automorphisms of an input graph give rise to symmetry. These symmetry properties often hinder an algorithm solving a combinatorial problem, as it wastefully investigates different configurations of essentially the same solution.

In this thesis, we set out to explore symmetry properties in model expansion problems for both predicate and propositional logic. The goal is to equip automated systems with the necessary tools to adequately handle symmetry. By investigating both symmetry detection and symmetry exploitation, we present symmetry exploitation techniques that rely only on problem specifications as input, without additional symmetry information. Systems equipped with these techniques are able to tackle a wider range of problems with less human input – the eventual goal of any artificial intelligence.

First, we present BreakID, a novel symmetry breaking preprocessor for propositional logic. BreakID’s core idea is to investigate structural properties of the symmetry group of a problem, and to adjust any generated symmetry breaking formulas accordingly. Furthermore, we also added usability features and technical optimizations that allow symmetry detection and subsequent breaking for a broader range of propositional formulas, both in a Boolean satisfiability and an answer set programming context. Experimental results show that BreakID improves on Shatter and sbass, the previous state-of- the-art static symmetry breaking preprocessors for propositional logic.

Second, we investigate two new dynamic symmetry handling algorithms for propositional solvers, based on symmetrically deriving logical consequences.

The first algorithm, SP, focuses on propagating literals that are symmetrical to already propagated literals. SP is based on the notion of weak activity, a generalization of the constraint programming notion of activity. Experiments show that this approach is effective, but can be improved by also performing symmetrical propagations not based on the weak activity status of a symmetry. This leads to the second algorithm, SEL, which derives symmetrical explanation clauses and, as such, is a form of symmetrical learning. Even though SEL is a straightforward form of symmetry handling, we provide experiments that indicate it is competitive to BreakID’s advanced symmetry breaking.

However, working on a propositional level burdens the algorithms that detect symmetry and derive symmetry group information, as these properties are more readily available at the predicate level. Hence thirdly, we investigate how symmetry manifests itself in first-order logic. We propose the notion of local domain symmetry, a form of symmetry in predicate logic theories that captures a broad range of symmetry groups occurring in practical problems. Based on theoretical properties of local domain symmetry, we design efficient ways of both detecting and breaking it. Our implementation in IDP outperforms other approaches in symmetry detection time, and in symmetry breaking power for problems with large row interchangeability groups. Moreover, our approach is one of the few automated approaches that detects symmetry at the predicate level. The modest price to pay is that some forms of symmetry are not captured by the notion of local domain symmetry.

Finally, we establish a promising link between local search algorithms and symmetries by noting that a local search neighborhood for a problem can be constructed from its quasisymmetry group. These quasisymmetries can be automatically detected with previously established techniques, leading to a novel automated local search approach with good initial performance.

Summarized, our work provides new insights in how symmetry can be detected and exploited without human interaction. These ideas, rooted in propositional and predicate logic, are useful for anyone designing automated combinatorial problem solving systems, be they affiliated with constraint programming, operations research, Boolean satisfiability solving, answer set programming, or related fields.