SAT 문제 해결에서의 궤도 팔(Orbitopal) 고정 기법

Orbitopal Fixing in SAT

정교한 휴리스틱을 사용함에도 불구하고, 불리언 만족 가능성(SAT) 솔버는 여전히 대칭 문제에 취약하여 이미 탐색된 영역과 대칭적인 영역을 반복적으로 탐색하는 경우가 발생합니다. 다른 해결 방식에서는 대칭 처리 기술이 일반적으로 사용되지만, 최첨단 증명 생성 SAT 솔버에 이러한 기술을 통합하는 것은 어렵습니다. 추가적인 추론 과정은 빠르고, 솔버의 휴리스틱에 영향을 미치지 않으며, 형식적인 증명 로깅과 호환되어야 하기 때문입니다. 이러한 문제점을 해결하기 위해, 혼합 정수 프로그래밍에서 파생된 궤도 팔 고정(orbitopal fixing) 기법을 기반으로 하는 실용적인 정적 대칭 해소 방법을 제안합니다. 저희의 접근 방식은 단위 절(unit clause)만 추가하여 후속 처리 속도 저하를 최소화하며, 치환 중복 증명 시스템에서 간결한 증명 인증서를 생성합니다. satsuma 도구에 구현된 저희의 방법은 대칭성이 높은 벤치마크에서 일관된 속도 향상을 제공하며, 다른 영역에서는 미미한 성능 저하만 발생합니다.

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.