Is Four Enough? Automated Reasoning Approaches and Dual Bounds for Condorcet Dimensions of Elections

이 논문은 **"Condorcet 승리 집합 (Condorcet Winning Sets, CWS)"의 존재를 보장하기 위해 필요한 위원회 (Committee) 의 최소 크기 (Condorcet 차원)**에 대한 이론적 간극을 해소하기 위해 자동 추론 (Automated Reasoning) 기법을 적용한 연구입니다. 저자들은 카네기 멜론 대학교 (CMU) 소속 연구진으로 구성되어 있으며, 혼합 정수 선형 계획법 (MILP) 과 선형 계획법 (LP) 의 쌍대성 (Duality) 을 활용하여 기존 이론적 상한선을 개선하고 새로운 추측을 제시합니다.

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

1. 문제 정의 및 배경 (Problem & Background)

• Condorcet 승리 집합 (CWS): $n$명의 유권자가 $m$명의 후보를 순위로 매기는 선거에서, 위원회 $W$가 Condorcet 승리 집합이 되기 위해서는 위원회 외부의 어떤 후보 $c$에 대해서도, 유권자의 과반수 (strict majority, $\alpha > 1/2$) 가 $c$를 $W$의 모든 구성원보다 선호하지 않아야 합니다.
• Condorcet 차원: 어떤 선거에서도 CWS 가 존재하도록 보장하는 위원회의 최소 크기 $k$를 의미합니다.
• 현재의 이론적 간극:
  • 하한선 (Lower Bound): $k=1$과 $k=2$는 CWS 를 보장하지 않는다는 것이 알려져 있습니다. Charikar et al. 은 $k=3$이 필요한 특정 선거 구성을 보여주었습니다. 즉, $k \ge 3$입니다.
  • 상한선 (Upper Bound): Nguyen et al. 은 최근 $k=5$면 항상 CWS 가 존재함을 증명했습니다.
  • 간극: 현재 $3 \le k \le 5$로 알려져 있어, $k=3$ 또는 $k=4$가 실제로 충분할지 여부가 불확실합니다.
• 연구 목표: 자동 추론 기법을 사용하여 이 간극을 좁히고, $k=4$가 충분하다는 것을 증명하거나 반증하는 것입니다.

2. 방법론 (Methodology)

저자들은 유권자의 수를 이산적인 개수가 아닌 연속적인 확률 분포로 모델링하여 무한한 유권자 집단을 가정하고, 이를 해결하기 위해 다음과 같은 최적화 기법을 개발했습니다.

2.1 기본 MILP (Mixed-Integer Linear Programming)

• 목적: 주어진 후보 수 $m$과 위원회 크기 $k$에 대해, 최악의 경우에도 CWS 가 존재하지 않는 선거 프로파일 (유권자 분포 $x$) 을 찾는 것.
• 최적화 문제:
  $$\alpha^* = \max_{x \in \Delta(S)} \min_{W \in M_k} \max_{c \notin W} \left( \sum_{s \in S | c \succ_s W} x[s] \right)$$
  여기서 $\alpha^*$는 위원회 $W$를 이길 수 있는 외부 후보 $c$에 대한 최대 지지율입니다. 만약 $\alpha^* > 1/2$라면 해당 $k$에서는 CWS 가 존재하지 않습니다.
• 변수:
  • $x[s]$: 특정 순위 $s$를 가진 유권자의 비율.
  • $y_{W,c}$: 위원회 $W$를 이기는 외부 후보 $c$를 선택하는 이진 변수.
• 제약 조건: 각 위원회 $W$에 대해 정확히 하나의 외부 후보가 $W$를 이기는지 여부를 결정하고, 그 지지율이 $\alpha$보다 크거나 같도록 강제합니다.

2.2 확장된 MILP (infMILP) - 무한 클론 (Infinite Clones)

• 아이디어: 후보를 단일 개체가 아닌 **무한한 순환 클론 (cyclic clones)**의 집합으로 간주합니다. 예를 들어, 후보 $A$가 $A_1, A_2, \dots$로 나뉘어 $A_{i+1}$이 $A_i$를 이기는 순환 구조를 가정합니다.
• 효과: 이 추상화를 통해 특정 후보가 위원회에 포함되더라도, 그 후보의 '클론'이 위원회를 이길 수 있는 상황을 모델링할 수 있어 더 강력한 하한선 (tighter bounds) 을 도출할 수 있습니다.
• 다중집합 (Multisets): 위원회 내에 동일한 후보의 여러 복사본이 포함될 수 있도록 허용하여 문제를 일반화합니다.

2.3 최적화 기법 (Optimizations)

계산 복잡도를 줄이고 대규모 문제를 해결하기 위해 다음 기법들을 적용했습니다:

1. 순열 축소 (Reducing Permutations): 순위의 하단 $k$개 위치의 순서는 논리적 제약에 영향을 주지 않으므로, 상단 $m-k$개 위치만 고려하여 변수 수를 $m!$에서 $m!/k!$로 줄입니다.
2. 대칭성 깨기 (Symmetry Breaking): 후보 라벨의 순열은 CWS 존재 여부에 영향을 주지 않으므로, 특정 위원회나 도전자 (challenger) 를 고정하여 탐색 공간을 축소합니다.
3. 부분 표본 추출 (Subsampling): 모든 가능한 순위를 고려하는 대신 무작위로 고정된 수 ($z$) 의 순위만 샘플링하여 MILP 크기를 줄입니다. (완전성은 잃지만 반례 발견에는 유효함)
4. 제약 생성 (Constraint Generation): 모든 위원회에 대한 제약 조건을 한 번에 생성하지 않고, 현재 해가 위반하는 위원회만 발견하여 점진적으로 추가하는 방식 (Restricted Master Problem) 을 사용합니다.

3. 주요 결과 (Results)

• 실험 환경: Gurobi Optimizer 를 사용하며, 32 코어 CPU 와 512GB RAM 을 갖춘 HPC 클러스터에서 실행되었습니다.
• 하한선 검증: 알고리즘은 기존에 알려진 $k=3$이 필요한 사례를 성공적으로 재발견했습니다.
• 반례 탐색 실패: $m \le 9$까지의 다양한 후보 수와 $k$에 대해 광범위한 탐색을 수행했으나, $k > 3$이 필요한 (즉, $\alpha^* > 1/2$인) 어떤 선거도 발견하지 못했습니다.
• 상한선 경향성:
  • MILP 와 infMILP 모두에서 계산된 상한선 (LP relaxation bounds) 은 이론적 추측인 $\alpha \le \frac{2}{k}$를 강력하게 지지했습니다.
  • 특히 $k=4$인 경우, 모든 실험에서 $\alpha \le 0.5$ (즉, CWS 존재) 를 시사하는 결과를 보였습니다.
  • LP relaxation 의 초기 값은 $m$이 커질수록 1 에 수렴하는 경향이 있었으나, 분기 한정법 (branch-and-bound) 과정을 거치며 $\frac{2}{k}$로 수렴하는 구조적 특성이 관찰되었습니다.

4. 핵심 기여 및 추측 (Key Contributions & Conjecture)

저자들은 실험 결과를 바탕으로 **LP 완화 (Relaxation) 의 쌍대 문제 (Dual Problem)**를 분석하여 새로운 이론적 경로를 제시했습니다.

• 단순화된 쌍대 문제 (Simplified Dual): 복잡한 MILP 의 LP 완화 쌍대 문제를 분석하여, 매개변수 $Q$를 제거하고 단순화한 새로운 쌍대 프로그램을 유도했습니다.
• 추측 1.1 (Dual Bound on $\alpha$): 단순화된 쌍대 선형 계획법의 최적 목적 함수 값 $u^*_k$는 다음과 같이 제한된다고 추측합니다.
  $$u^*_k \le \frac{2}{k}$$
• 의미: 이 추측이 증명되면, 약한 쌍대성 (Weak Duality) 에 의해 원래 문제의 $\alpha \le \frac{2}{k}$가 성립함을 의미합니다.
  • $k=4$일 때, $\alpha \le 2/4 = 1/2$가 되므로, 크기 4 인 위원회는 항상 Condorcet 승리 집합이 됩니다.
  • 이는 기존에 알려진 상한선 $k=5$를 $k=4$로 개선하는 결과를 의미합니다.

5. 결론 및 의의 (Conclusion & Significance)

• 실증적 증거: 자동 추론을 통한 대규모 탐색은 Condorcet 차원이 현재 알려진 상한선 ($k=5$) 보다 작을 가능성이 매우 높음을 강력하게 시사합니다. 특히 $k=4$가 충분하다는 증거를 제시합니다.
• 방법론적 혁신:
  • 유권자의 수를 고정하지 않고 확률 분포로 모델링하여 무한한 유권자를 다룰 수 있게 했습니다.
  • 후보의 순환 클론 (cyclic clones) 개념을 도입하여 무한한 후보 공간까지 탐색 가능한 확장된 MILP (infMILP) 를 제안했습니다.
  • 기존 SAT 기반 접근법의 확장성 한계를 극복하고, 사회 선택 이론의 다른 문제들에 적용 가능한 일반적 프레임워크를 제시했습니다.
• 미래 작업: 실험적 결과는 강력하지만 수학적 증명은 아닙니다. 향후 연구의 핵심은 유도된 단순화된 쌍대 선형 계획법의 해가 $\frac{2}{k}$로 제한됨을 수학적으로 증명하는 것입니다. 이것이 성공한다면 Condorcet 차원에 대한 존재성과 불가능성 결과 간의 간극을 완전히 해소하게 됩니다.

요약하자면, 이 논문은 계산적 자동 추론 기법을 통해 Condorcet 승리 집합의 크기에 대한 기존 이론적 상한선 ($k=5$) 을 $k=4$로 개선할 수 있음을 강력하게 시사하며, 이를 증명하기 위한 구체적인 쌍대성 기반의 분석적 경로를 제시했습니다.