Automated Reencoding Meets Graph Theory

이 논문은 현대 SAT(Satisfiability) 솔버의 핵심 전처리 기술 중 하나인 **유계 변수 추가 (Bounded Variable Addition, BVA)**의 이론적 특성과 한계를 그래프 이론을 통해 정밀하게 분석하고, 이를 바탕으로 더 효율적인 알고리즘을 제안합니다.

저자 Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule (Carnegie Mellon University) 는 BVA 가 2-CNF(Conjunctive Normal Form) 식을 어떻게 재인코딩 (reencoding) 하는지, 그리고 그 한계가 어디까지인지에 대한 새로운 통찰을 제공합니다.

다음은 논문의 상세한 기술적 요약입니다.

---

1. 문제 정의 (Problem)

• 배경: 현대 SAT 솔버는 다양한 휴리스틱, 전처리 (preprocessing), 인프로세싱 (inprocessing) 기법을 결합하여 높은 성능을 보입니다. 그중 BVA 는 보조 변수를 도입하여 입력 식을 동치 만족 (equisatisfiable) 인 더 적은 절 (clause) 수를 가진 식으로 변환하는 중요한 전처리 기술입니다.
• 현황: BVA 는 실험적으로 매우 유용함이 입증되었으나 (예: 2023, 2024 SAT Competition 우승 솔버에 사용됨), 이론적으로 그 능력과 한계가 명확히 규명되지 않았습니다.
• 핵심 질문: BVA 는 어떤 2-CNF 식을 재인코딩할 수 있는가? 최적의 절 감소율은 어느 정도이며, BVA 가 달성할 수 없는 구조는 무엇인가?

2. 방법론 (Methodology)

저자들은 BVA 의 동작을 그래프 이론, 특히 **정류기 네트워크 (Rectifier Networks)**의 개념을 사용하여 모델링했습니다.

• 그래프 표현 (Diagram): 2-CNF 식을 그래프로 표현합니다.
  • 변수는 정점 (vertex) 에 대응.
  • 절 (clause) 은 간선 (edge) 에 대응 (방향성 유무에 따라 함축 관계나 비방향 관계로 매핑).
• 엄격한 편향 정류기 네트워크 (Strict Polarized Rectifier Network, SPRN):
  • BVA 의 재인코딩 과정은 그래프의 간선을 줄이기 위해 보조 정점 (auxiliary vertices) 을 추가하는 과정으로 해석됩니다.
  • 저자들은 이상적인 BVA 알고리즘이 생성할 수 있는 모든 재인코딩이 SPRN에 의해 실현된다는 것을 증명했습니다.
  • SPRN 은 보조 정점이 유효한 경로 (valid walk) 에 반드시 포함되어야 하고, 기본 정점 간의 함축 관계를 여러 경로로 중복 실현하지 않는 등의 '엄격성 (strictness)' 조건을 만족해야 합니다.
• 이론적 분석: SPRN 의 성질을 이용하여 BVA 가 달성할 수 있는 절 수의 상한선 (upper bound) 과 하한선 (lower bound) 을 정보 이론적 방법과 조합론적 분석을 통해 유도했습니다.

3. 주요 기여 및 결과 (Key Contributions & Results)

3.1. 일반 2-CNF 식에 대한 재인코딩 한계

• 최적성 증명: 이상적인 BVA 는 $n$개의 변수를 가진 임의의 2-CNF 식을 $O(n^2 / \log n)$개의 절로 재인코딩할 수 있음을 보였습니다.
  • 단순화 전 (Idealized BVA): 상한선은 $(1 + o(1)) \frac{n^2}{\log n}$.
  • 단순화 후 (Equivalent Literal Substitution 등 포함): 상한선은 $(\frac{\log 3}{4} + o(1)) \frac{n^2}{\log n} \approx 0.396 \frac{n^2}{\log n}$.
• 하한선: 단순화 전 BVA 의 하한선은 $(1 - o(1)) \frac{n^2}{\log n}$이며, 단순화 후에는 $(\frac{\log 3}{4} - o(1)) \frac{n^2}{\log n}$입니다. 이는 BVA 가 최악의 경우에서 상수 인자 내에서 최적임을 의미합니다.
• 보편적 하한선: 어떤 재인코딩 방법이라도 2-CNF 출력에 대해 $(\frac{1}{4} - o(1)) \frac{n^2}{\log n}$보다 적은 절 수를 보장할 수 없음을 증명했습니다.

3.2. 특정 구조식: AtMostOne 제약

• AtMostOne 제약: $n$개의 변수 중 최대 1 개만 참이어야 하는 제약 ($\bigwedge_{i<j} (x_i \lor x_j)$) 에 대한 직접 인코딩은 $\Theta(n^2)$개의 절을 가집니다.
• BVA 의 한계: 실제 구현체 (Manthey et al.) 는 이를 $3n - 6$개의 절로 줄이는 것을 관찰했습니다. 저자들은 이상적인 BVA 가 휴리스틱과 무관하게 $3n - 6$개보다 적은 절로 재인코딩할 수 없음을 증명했습니다.
• 의미: 이는 BVA 가 $2n + o(n)$개의 절을 사용하는 'Product Encoding'과 같은 더 효율적인 구조를 생성할 수 없음을 의미합니다. BVA 의 '엄격성 (strictness)' 조건이 이러한 최적 구조 생성을 방해합니다.

3.3. 효율적인 알고리즘 구현 (BiVA)

• 기존 문제: 기존 BVA 구현체 (CaDiCaL 의 factor 등) 는 $O(n^3)$ 이상의 시간 복잡도를 가질 것으로 추정되었습니다.
• 새로운 구현: 최근 Krapivin et al. 의 이분 그래프 (biclique) 분할 알고리즘을 활용하여, 2-CNF 식에 대한 BVA 를 $O(n^2)$ 시간에 수행하는 알고리즘 (BiVA) 을 개발했습니다.
• 성능: 무작위 단조 (monotone) 2-CNF 식에 대해 기존 방법과 유사한 절 감소 효과를 내면서도, 재인코딩 속도가 기하급수적으로 빨라졌습니다.

4. 실험 결과 (Experimental Results)

• 테스트 환경: 무작위 그래프 ($G(n, 1/2)$) 에서 독립 집합 (Independent Set) 문제를 인코딩한 2-CNF 식을 사용.
• 비교 대상: 기존 BVA 구현, Kissat 의 factor, 제안된 BiVA, 그리고 이들의 조합 (BiVA+BVA, BiVA+factor).
• 결과:
  • 절 수 감소: 모든 방법이 유사한 절 감소율을 보였으나, BiVA 단독은 약 5-15% 정도 적게 줄였습니다. 그러나 BiVA + 기존 방법을 조합하면 BiVA 가 먼저 구조를 단순화하여 후속 처리가 더 빨라지므로, 전체적인 절 수와 실행 시간이 최적화되었습니다.
  • 실행 시간: BiVA 는 재인코딩 시간이 기존 방법보다 훨씬 짧아 (기존 BVA 는 $O(n^3)$, BiVA 는 $O(n^2)$), 대규모 인스턴스에서 전체 파이프라인 속도가 크게 향상되었습니다.
  • 보조 변수: BiVA 는 보조 변수를 적게 생성하지만, 조합 시에는 보조 변수가 증가하는 경향이 있었습니다.

5. 의의 및 결론 (Significance)

1. 이론적 명확성: BVA 가 왜 특정 구조 (예: Product Encoding) 를 생성하지 못하는지, 그리고 그 이론적 한계가 어디인지에 대한 첫 번째 엄밀한 그래프 이론적 설명을 제공했습니다.
2. 알고리즘 개선: BVA 의 핵심 연산을 그래프 이론 (이분 그래프 분할) 과 연결함으로써, 시간 복잡도를 $O(n^3)$에서 $O(n^2)$로 획기적으로 낮춘 새로운 구현체를 제시했습니다.
3. 실용적 가치: SAT 솔버의 전처리 단계에서 BVA 를 더 효율적으로 적용할 수 있는 길을 열었으며, 특히 대규모 무작위 2-CNF 식 처리에 있어 성능 향상을 입증했습니다.
4. 미래 방향: BVA 의 '엄격성'이 한계로 작용한다는 점을 지적하여, 이를 완화하거나 다른 재인코딩 기법과 결합하여 더 강력한 전처리 도구를 개발할 수 있는 가능성을 제시했습니다.

요약하자면, 이 논문은 BVA 를 단순한 휴리스틱이 아닌 그래프 이론적 구조로 해석하여 그 이론적 한계를 규명하고, 이를 바탕으로 더 빠르고 효율적인 알고리즘을 개발한 성공적인 사례입니다.