Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into state-of-the-art proof-producing SAT solvers is difficult: added reasoning must be fast, non-interfering with solver heuristics, and compatible with formal proof logging. To address these issues, we present a practical static symmetry breaking approach based on orbitopal fixing, a technique adapted from mixed-integer programming. Our approach adds only unit clauses, which minimizes downstream slowdowns, and it emits succinct proof certificates in the substitution redundancy proof system. Implemented in the satsuma tool, our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.

翻译：尽管布尔可满足性（SAT）求解器采用了复杂的启发式策略，它们仍然容易受到对称性的影响，导致其探索与已搜索区域对称的搜索空间。虽然对称性处理在其他求解范式中已是常规操作，但将其集成到最先进的能生成证明的SAT求解器中却面临挑战：所添加的推理必须快速、不干扰求解器启发式策略，并且与形式化证明日志兼容。为解决这些问题，我们提出了一种基于轨道面固定的实用静态对称性破缺方法，该技术改编自混合整数规划。我们的方法仅添加单元子句，从而最大程度地减少下游性能损失，并在替换冗余证明系统中生成简洁的证明证书。通过在satsuma工具中实现，我们的方法在富含对称性的基准测试上实现了稳定的加速，而在其他情况下性能回归可忽略不计。