Lifted Symmetry Detection and Breaking for MAP Inference
Symmetry breaking is a technique for speeding up propositional satisfiability testing by adding constraints to the theory that restrict the search space while preserving satisfiability. In this work, we extend symmetry breaking to the problem of model finding in weighted and unweighted relational theories, a class of problems that includes MAP inference in Markov Logic and similar statistical-relational languages. We introduce term symmetries, which are induced by an evidence set and extend to symmetries over a relational theory. We provide the important special case of term equivalent symmetries, showing that such symmetries can be found in low-degree polynomial time. We show how to break an exponential number of these symmetries with added constraints whose number is linear in the size of the domain. We demonstrate the effectiveness of these techniques through experiments in two relational domains. We also discuss the connections between relational symmetry breaking and work on lifted inference in statistical-relational reasoning.
SUMMARY        The work concerns symmetries in relational models, which are       permutations of the set of atoms (i.e. predicates applied to       constants) that do not change a relational theory.A model of       a theory is a truth-assignment for each atom that makes the       theory true.A symmetry of a theory can therefore permute the       atoms in a model without changing whether the model satisfies       the theory.The authors define term symmetries to be those       symmetries that can be expressed as just a permutation of the       constants appearing in the atoms, rather than of the atoms       themselves.They further define term-equivalent symmetries as       term symmetries that can be expressed as a partition of the       constants, with the symmetries being all permutations that map       each constant to another in the same block.        Such symmetries thus define an equivalence relation on models,       with equivalence being with regard to satisfiability, weight,       or another objective.The idea of symmetry-breaking is to       introduce constraints to the theory that eliminate some       otherwise valid models, while making sure that at least one       model in each equivalence class survives.If implemented as a       pre-processing step to an inference or satisfiability       algorithm, this would serve to reduce the search space.        QUALITY        At a first glance, the work appears to be of fairly high       quality.The definitions are clear, and necessary theorems       are carefully stated and proved.        CLARITY        Having some knowledge of the field but not a deep background,       I found the exposition rather hard to follow.While the basic       definitions and concepts are clear enough (if rather dense), a       running example domain would have been helpful to illustrate       the types of symmetries being considered.        Some of the results seem counter-intuitive, but this is not       discussed.For example, the class of term symmetries being       larger than term-equivalent, one would expect that breaking       the former would result in a bigger speed-up than just       breaking the latter.The opposite seems to be the case in       many experiments; the "Term" procedure sometimes takes longer.       Some clarification would be appreciated on whether this is       because the term symmetry-breaking propositions cause a       slow-down.        ORIGINALITY AND SIGNIFICANCE        While the paper presents original algorithms for detecting and       breaking term and term-equivalent symmetries, the significance       of these symmetry classes was not immediately clear.An       argument should be made that these classes are sufficiently       rich and expressive to simplify real-world problems.        MINOR CORRECTIONS        In lines 188 and 189, "uniquely color" should be "unique       color". In line 88, "unique type" should perhaps be "single       type", since multiple constants can have the same type.