Near-Optimal Encodings of Cardinality Constraints

1. 문제 정의 (Problem)

SAT (Satisfiability) 문제 해결에서 카디널리티 제약은 매우 기본적이면서도 중요한 구성 요소입니다. 가장 대표적인 제약은 AtMostOne (주어진 변수들 중 최대 1 개만 참이어야 함) 과 AtMostk (최대 k 개만 참이어야 함) 입니다.

• 기존의 문제점:
  • $n$개의 변수에 대한 AtMostOne 을 직접 인코딩하면 $\binom{n}{2}$개의 절이 필요하여 $O(n^2)$의 크기로 급증합니다.
  • 보조 변수 (auxiliary variables) 를 도입하여 선형 크기 ($O(n)$) 로 줄인 인코딩들이 존재하지만 (예: Sequential Counter), 절의 수나 보조 변수의 수를 더 줄일 수 있는지가 연구 주제였습니다.
  • 특히 Chen 의 "Product Encoding"이 절의 수 측면에서 최적이라는 추측이 있었으나, 이를 반증할 수 있는지가 미해결 상태였습니다.
  • AtMostk 제약에 대해서는 $k$가 작을 때 더 효율적인 인코딩이 필요했습니다.

2. 주요 방법론 (Methodology)

저자들은 세 가지 핵심 기법을 도입하여 문제를 해결했습니다.

A. 다분할 그래프 기반 인코딩 (Multipartite Encoding)

• 개념: Chen 의 Product Encoding 을 격자 (grid) 관점이 아닌 완전 이분 그래프 (complete bipartite graph) 관점에서 재해석했습니다.
• 혁신: 이분 그래프를 **완전 다분할 그래프 (complete multipartite graph)**로 확장했습니다. $n$개의 입력 변수를 그래프의 간선에 매핑하고, 각 정점 (vertex) 에 보조 변수를 할당합니다.
• 작동 원리: "최대 1 개의 간선만 선택됨"이라는 조건은 "(a) 각 파티션 (part) 에서 최대 1 개의 정점만 선택되고, (b) 선택된 정점이 있는 파티션은 최대 2 개이다"라는 조건으로 변환됩니다.
• 효과: 이 구조를 통해 절의 수를 $2n + 2\sqrt{2n} + O(\sqrt[3]{n})$까지 줄였습니다. 이는 Chen 의 $2n + 4\sqrt{n}$보다 더 작은 2 차항 계수를 가집니다.

B. 분산 스위칭 (Disjunctive Switching)

• 개념: 알고리즘의 조건부 분기 (switch/case) 를 CNF 로 인코딩할 때 발생하는 비효율성을 해결하는 새로운 패러다임입니다.
• 문제: 기존 방식은 모든 가능한 분기에 대한 절을 모두 포함하여 크기가 분기들의 합이 됩니다.
• 해결: "어떤 분기가 선택될 것이다"라는 넓은 절 (wide clause) 을 도입하고, 선택되지 않은 분기의 조건은 부정을 통해 효율적으로 처리합니다.
• 적용: AtMostk 의 일반화된 Product Encoding 에 적용하여, $k$가 작을 때 $(k+1)n$에서 $2n$으로 절의 수를 획기적으로 줄였습니다.

C. 그리드 압축 (Grid Compression)

• 개념: 해시 테이블 (hash tables) 의 아이디어에서 영감을 받았습니다.
• 작동 원리: $n$개의 입력 변수를 큰 격자 $M$에 배치한 후, 이를 더 작은 격자 $L$로 "압축"합니다. $M$에서 참인 열 (occupied columns) 들이 $L$의 열로 매핑되도록 제약합니다.
• 효과: 작은 격자 $L$에 대해 AtMostk 제약을 부과함으로써 전체 절의 수를 줄입니다.
  • $k = o(\sqrt[3]{n})$일 때: $2n + o(n)$ 절 사용 (Disjunctive Grid Compression).
  • $k = o(n)$일 때: $4n + o(n)$ 절 사용 (Grid Compression).

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

1) AtMostOne 인코딩의 최적성 반증 및 하한 증명

• 추측 반증: Chen 의 Product Encoding 이 절의 수 측면에서 최적이라는 추측을 반증했습니다. 새로운 인코딩은 $2n + 2\sqrt{2n} + O(\sqrt[3]{n})$개의 절을 사용합니다.
• 무조건적 하한 (Unconditional Lower Bound): 전파 완전성 (propagation completeness) 을 가정하지 않은 상태에서, AtMostOne 인코딩은 최소 $2n + \sqrt{n} + 1 - 2$개의 절이 필요함을 증명했습니다. 이는 해당 제약에 대한 첫 번째 비자명한 무조건 하한입니다.
• 결론: AtMostOne 인코딩의 최소 절 수는 $\Theta(\sqrt{n})$ 항을 포함한 $2n + \Theta(\sqrt{n})$임을 확정했습니다.

2) 회로 복잡성 (Circuit Complexity) 의 오랜 난제 해결

• Threshold-2 회로 개선: AtMostOne 의 부정은 Threshold-2 함수 ($T_2$) 입니다. 저자들의 구성은 Adleman (1976) 의 50 년 된 구성을 개선하여 $2n + \sqrt{2n} + O(\sqrt[3]{n})$ 개의 게이트를 사용하는 단조 부울 회로 (monotone boolean circuit) 를 제시했습니다.
• Single-Level Conjecture 반증: $T_2$ 함수에 대한 최소 단조 부울 회로는 단일 레벨 (single-level) 이 아님을 보였습니다. 이는 Bloniarz (1979) 가 제기한 47 년 된 오픈 문제를 해결하며, "단일 레벨 회로 복잡도가 항상 단조 회로 복잡도와 같다"는 추측이 가장 간단한 2 차 부울 함수에서도 성립하지 않음을 증명했습니다.

3) AtMostk 인코딩의 개선

• 새로운 상한: $k$가 $n$에 비해 작을 때, 기존에 알려진 $(k+1)n$ 또는 $7n$ 크기의 인코딩보다 훨씬 작은 인코딩을 제시했습니다.
  • $k = o(\sqrt[3]{n})$일 때: $2n + o(n)$ 절.
  • $k = o(n)$일 때: $4n + o(n)$ 절.
• 하한: AtMostk 인코딩에 대해 $2(n-k) + \Omega(\sqrt{n-k})$의 하한을 유도했습니다.

4) 실용적 성능 (Empirical Evaluation)

• 전파 완전성 (Propagation Completeness) 에 대한 통념 도전: 전파 완전성은 SAT 솔버 성능에 필수적이라는 통념이 있었으나, 저자들의 인코딩 (특히 Disjunctive Grid Compression) 은 전파 완전성이 없음에도 불구하고 많은 벤치마크에서 기존 인코딩 (Sequential Counter 등) 과 경쟁하거나 더 좋은 성능을 보였습니다.
• 결과: 절의 수가 적다는 것이 항상 성능을 보장하지는 않지만, 절 수를 줄이는 이론적 접근이 실용적으로도 유효할 수 있음을 보여주었습니다.

4. 의의 및 중요성 (Significance)

1. 이론적 한계 돌파: CNF 인코딩 이론에서 50 년 이상 지속되어 온 회로 복잡성 및 인코딩 최적성 문제에 대한 중요한 진전을 이루었습니다.
2. 새로운 패러다임 제시: '다분할 그래프', '분산 스위칭', '그리드 압축'과 같은 새로운 기법들은 CNF 인코딩 설계에 있어 그래프 이론과 해시 구조를 활용하는 새로운 방향을 제시합니다.
3. 실용적 함의: 전파 완전성이 필수적이지 않을 수 있다는 실험적 결과는 SAT 솔버 개발자와 제약 프로그래밍 연구자들에게 인코딩 선택의 유연성을 제공합니다. 특히 대규모 변수를 다루는 문제에서 절의 수를 줄이는 것이 솔버 성능 향상에 직접적인 영향을 미칠 수 있음을 시사합니다.
4. 확장성: 제시된 기법들은 단순한 AtMostOne 을 넘어 다양한 카디널리티 제약 및 부울 함수 인코딩에 적용 가능한 일반적인 프레임워크를 제공합니다.

요약하자면, 이 논문은 카디널리티 제약 인코딩의 이론적 하한과 상한을 동시에 좁혀 "거의 최적 (near-optimal)"인 인코딩을 제시했을 뿐만 아니라, 회로 복잡성 이론의 오래된 난제를 해결하고 실용적인 SAT 솔버 성능 개선에 기여한 획기적인 연구입니다.