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.

翻译：在可满足性问题（SAT）中，对对称性的专门处理对于解决实践中出现的各类实例不可或缺。然而，对称性的利用通常采取黑盒方法。典型做法是调用现成的外部通用对称性检测工具来计算公式的对称群。由此生成的群是一组置换，这些置换被传递给另一个单独的工具，以进一步分析并理解群的结构。第二次计算的结果随后用于诸如静态对称性破缺或搜索空间动态剪枝等任务。在这一工具链中，对称性的检测与分析通常占据了对称性利用的大部分时间开销。本文倡导对所谓的SAT-对称性接口采取更全面的视角。我们基于联合图/群对的新概念构建了一个计算框架，用于分析和改进对称性的检测与分析。使用我们的方法，在执行SAT-对称性接口上的计算任务时不会丢失任何信息。能够访问完整输入使得我们能够设计更简单且高效的算法。具体而言，我们设计了用于计算最精细直接不交分解、寻找等价轨道以及发现自然对称群作用的算法与启发式方法。我们的算法运行在所谓的实例-准线性时间内，即关于原始公式的输入规模和对称性检测工具返回的对称群描述长度均接近线性时间。我们的算法相较于现有最先进的对称性利用工具中使用的启发式方法以及通用的理论算法均有改进。