Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algorithms Transcending the SAT-Symmetry Interface

Markus Anders, Pascal Schweitzer, Mate Soos

TL;DR

The paper addresses the inefficiency of traditional, black-box symmetry workflows in SAT by proposing a holistic SAT-symmetry interface built on joint graph/group pairs $(G,S)$ with $\langle S\rangle = Aut(G)$. It defines an instance-linear runtime model and develops instance-linear/quasi-linear algorithms for three core tasks: finest disjoint direct decomposition, natural symmetric action detection, and equivalent orbit computation, all grounded in the joint input rather than separate tools. Key contributions include an orbit-graph based finest decomposition, a probabilistic giant-test framework for natural symmetric action, and a cycle-type graph framework (with enhancements) to compute equivalent orbits efficiently. These methods reduce over- and under-utilization of symmetry information, enabling faster static and dynamic symmetry exploitation in SAT and offering pathways to generalize to MIP and CSP contexts with complex symmetry structures.

Abstract

Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.

Algorithms Transcending the SAT-Symmetry Interface

TL;DR

The paper addresses the inefficiency of traditional, black-box symmetry workflows in SAT by proposing a holistic SAT-symmetry interface built on joint graph/group pairs with . It defines an instance-linear runtime model and develops instance-linear/quasi-linear algorithms for three core tasks: finest disjoint direct decomposition, natural symmetric action detection, and equivalent orbit computation, all grounded in the joint input rather than separate tools. Key contributions include an orbit-graph based finest decomposition, a probabilistic giant-test framework for natural symmetric action, and a cycle-type graph framework (with enhancements) to compute equivalent orbits efficiently. These methods reduce over- and under-utilization of symmetry information, enabling faster static and dynamic symmetry exploitation in SAT and offering pathways to generalize to MIP and CSP contexts with complex symmetry structures.

Abstract

Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.
Paper Structure (11 sections, 9 theorems, 1 equation, 8 figures, 4 algorithms)

This paper contains 11 sections, 9 theorems, 1 equation, 8 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries and Related Work
  3. SAT-Symmetry Computational Setting
  4. Favorable Group Structures in SAT
  5. Finest Disjoint Direct Decomposition
  6. Natural Symmetric Action
  7. Equivalent Orbits
  8. Cycle Type Graph
  9. Symmetries of Cycle Type Graph with Unique Cycles
  10. Cyclic Order to Equivalent Orbits
  11. Conclusion and Future Work

Key Result

Lemma 2

Let $H_M$ be a row interchangeability subgroup of $\Gamma = \mathop{\mathrm{Aut}}\nolimits(\mathcal{M}(F))$, and let $\Delta_i = (x_1, \dots{}, x_c)$ denote a row of $M$. $H_M$ is an elementary row interchangeability subgroup if and only if all of the following hold: (1) $\Delta_i$ is an orbit with

Figures (8)

  • Figure 1: Blurring the lines of the SAT-symmetry interface. We analyze existing practical routines (left), draw connections to existing concepts in computational group theory, and describe improved algorithms in our new SAT-symmetry context (right).
  • Figure 2: An illustration of a color refinement process.
  • Figure 3: Example model graph $\mathcal{M}(F_E) = \mathcal{M}(\{(x_1 \vee \overline{y_1}), (x_2 \vee \overline{y_2}), (x_3 \vee \overline{y_3}), (x_1\vee x_2 \vee x_3\vee z_1\vee z_2)\})$. The automorphisms of the graph correspond to the automorphisms of the formula. The coloring on the right side shows the orbit partition.
  • Figure 4: Model graph of $F_E$ colored with its orbit partition on the left. The corresponding graph with flipped edges is in the middle, which disconnects parts of the graph. On the right the orbit graph is shown, whose $3$ connected components correspond to the factors of the finest disjoint direct decomposition.
  • Figure 5: Illustration of two orbits that are non-homogeneously connected on the left in blue and purple. On the right, fixing a vertex of one orbit indicated in red immediately partitions the other orbit into two orbits: the neighbors of the red vertex in green, and the non-neighbors in orange.
  • ...and 3 more figures

Theorems & Definitions (14)

  • Definition 1: Equivalent orbits (see seress_2003)
  • Lemma 2
  • Lemma 3
  • proof
  • Theorem 4
  • Theorem 4
  • proof
  • Lemma 5
  • proof
  • Lemma 6
  • ...and 4 more