超越SAT-对称界面的算法
摘要：对于解决实际中出现的各种满足性问题（SAT），对对称性进行专门处理是不可或缺的。然而，对称性的利用通常采用黑盒方法。通常情况下，调用现成的外部通用对称性检测工具来计算公式的对称群。生成的群是一组传递给单独的工具以进一步分析群结构的排列。第二次计算的结果被用于静态对称性破坏或动态剪枝等任务。在这个工具流程中，对对称性的检测和分析通常会产生大部分时间开销。 在本文中，我们提倡对我们所称的SAT-对称性界面有一个更全面的观点。我们提出了一个以新概念的图/群对为中心的计算设置，用于分析和改进对称性的检测和分析。使用我们的方法，在SAT-对称性界面上执行计算任务时不会丢失任何信息。可以访问整个输入，可以使用简单但高效的算法。 具体而言，我们设计了用于计算最佳直接不相交分解、寻找等价轨道和寻找自然对称群作用的算法和启发式方法。我们的算法在我们称为实例准线性时间的情况下运行，即根据原始公式的输入大小和由对称性检测工具返回的对称群的描述长度几乎是线性时间。我们的算法在比起最先进的对称性利用工具中使用的启发式方法以及理论通用算法上都有所改进。
作者：Markus Anders, Pascal Schweitzer, Mate Soos
论文ID：2306.00613
分类：Data Structures and Algorithms
分类简称：cs.DS
提交时间：2023-06-02