SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set

1. 문제 정의 (Problem)

• 코헨 - 스페커 (KS) 집합: 3 차원 이상의 힐베르트 공간에서 정의되며, 특정 조건 (직교 기저마다 정확히 하나의 '1' 할당, 직교하는 두 광선 중 최대 하나의 '1' 할당) 을 만족하는 {0, 1} 할당이 불가능한 유한한 광선 집합입니다. 이는 양자 역학의 비국소성과 문맥성을 증명하는 핵심 도구입니다.
• 현재까지의 한계: 3 차원에서 가장 작은 KS 집합의 크기는 60 년 가까이 미해결 문제였습니다. 알려진 가장 작은 KS 집합은 31 개의 광선 (Conway-Kochen) 이지만, 최소 크기는 24 이상임이 증명되었습니다.
• 연구 목표: 13 개의 광선으로 구성된 유 - 오 (Yu-Oh) 집합 (최소 상태 독립적 문맥성 집합, SI-C) 을 포함하는 KS 집합을 탐색합니다. 특히, 유 - 오 집합을 기반으로 직교하는 광선을 재귀적으로 추가하여 생성된 **25 개의 광선으로 구성된 '완전 SI-C 집합'**을 포함하는 33 개 이하의 광선을 가진 모든 KS 집합을 **완전 탐색 (Exhaustive Enumeration)**하는 것이 목표입니다.

2. 방법론 (Methodology)

A. SAT + NAUTY 기반의 질서 있는 생성 (Orderly Generation)

기존의 SAT 기반 접근법 (SAT+CAS, SMS) 은 **사전적 순서 (Lexicographical)**에 기반한 정규성 (Canonicity) 정의를 사용하여 동형 (Isomorphism) 을 제거했습니다. 그러나 이 방법은 그래프 크기가 커질수록 정규성 확인에 지수 함수적인 시간이 소요되어 25~33 개의 정점을 가진 대규모 KS 집합 탐색에는 비효율적이었습니다.

저자들은 이를 해결하기 위해 **재귀적 정규 라벨링 (Recursive Canonical Labeling, RCL)**을 도입했습니다.

• RCL 의 핵심: NAUTY(그래프 동형성 검사 도구) 의 높은 효율성을 활용하되, SAT 솔버의 부분 할당 (Partial Assignment) 에 대해 **계속성 (Hereditary property)**을 보장하도록 래핑 (Wrapping) 한 구조입니다.
  • 기존 NAUTY 는 부분 그래프가 정규형이 아닐지라도 전체 그래프가 정규형일 수 있어 (비계속성), SAT 솔버의 가지치기에 직접 적용하기 어렵습니다.
  • RCL 은 NAUTY 를 기반으로 하되, 가장 큰 라벨을 가진 정점을 재귀적으로 고정하여 부분 그래프가 항상 정규형인지 확인하는 계층적 구조를 만듭니다.
• SAT + NAUTY 프레임워크:
  • SAT 솔버 (CaDiCaL) 가 간선 변수를 할당하며 그래프를 생성합니다.
  • 매번 새로운 전치 (Prefix) 가 완성될 때마다 RCL 을 통해 정규성 확인을 수행합니다.
  • 비정규형 (Non-canonical) 으로 판명되면 즉시 차단 절 (Blocking Clause) 을 추가하여 탐색 공간을 줄입니다.

B. 기하학적 제약 및 검증 (Orthogonality Check)

단순한 조합적 그래프 생성을 넘어, 생성된 그래프가 3 차원 복소수 공간 ($\mathbb{C}^3$) 에서 실제로 **직교 벡터로 구현 가능 (Geometric Realizability)**한지 확인합니다.

• 동적 좌표 추론: 고정된 기저 벡터 (25 개) 에 대해, SAT 솔버가 새로운 정점의 연결 관계를 결정하면, 교차곱 (Cross Product) 을 통해 새로운 벡터 좌표를 실시간으로 유도합니다.
• 기하학적 모순 탐지: 유도된 벡터가 기존 벡터와 평행해지거나, 직교해야 할 관계에서 직교하지 않는 등 기하학적 모순이 발생하면 이를 감지하여 해당 탐색 경로를 차단합니다.
• 정확한 산술 (Exact Arithmetic): 부동소수점 오차를 피하기 위해 Z3 및 대수적 필드를 사용하여 정확한 산술 연산을 수행합니다.

C. 증명서 (Proof Certificate)

탐색 결과의 신뢰성을 확보하기 위해 DRAT 증명 형식을 확장하여 다음과 같은 도메인 특화 절 (Clauses) 을 포함하는 증명서를 생성합니다.

• t-clauses (Canonicity): 동형 제거를 위한 차단 절.
• o-clauses (Orthogonality): 기하학적 모순을 차단하는 절.
• 외부 검증기 (Verifier) 가 이 증명서를 독립적으로 검증하여, 유효한 KS 집합이 누락되지 않았음을 보장합니다.

3. 주요 기여 (Key Contributions)

1. 새로운 정규성 프레임워크 (SAT+NAUTY): NAUTY 의 효율성과 SAT 기반 질서 있는 생성의 계층적 속성을 결합한 RCL 을 제안했습니다. 이는 기존 사전적 순서 기반 방법이 겪던 지수적 확장성 문제를 해결했습니다.
2. 완전 탐색 수행: 25 개의 광선으로 구성된 완전 SI-C 집합을 포함하는 33 개 이하의 광선을 가진 모든 KS 집합에 대한 첫 번째 완전 탐색을 수행했습니다.
3. 유일성 증명: 33 개의 광선으로 구성된 KS 집합 중, Schütte 가 발견한 집합이 25 개의 완전 SI-C 집합을 포함하는 유일한 집합임을 증명했습니다.
4. 검증 가능한 결과: 13 TiB 크기의 증명서를 생성하여 독립적으로 검증 가능한 결과를 제공했습니다.

4. 결과 (Results)

A. 성능 비교 (RCL vs. Lex-based)

• 실험: 15~26 개의 정점을 가진 4-색칠 가능한 K4-프리 그래프 100 개를 대상으로 정규성 확인 시간을 비교했습니다.
• 결과:
  • Lex-based (사전적 순서): 정점 수 $N=26$에서 평균 3.8 분 (약 230 초) 이 소요되었으며, $N$이 증가함에 따라 지수적으로 증가했습니다.
  • RCL (제안 방법): 정점 수와 무관하게 약 27ms 의 일정한 성능을 유지했습니다.
  • 속도 향상: $N=26$ 기준 약 8,499 배의 성능 향상을 기록했습니다. 이는 대규모 KS 집합 탐색에서 기존 방법이 병목 현상을 일으켰음을 보여줍니다.

B. KS 집합 탐색 결과

• 총 소요 시간: 128 코어 클러스터에서 약 1,641 시간 (CPU 시간) 소요.
• 탐색 결과: 조합적 조건을 만족하는 44 개의 비동형 후보가 발견되었으나, 기하학적 구현 가능성 (Orthogonal Representation) 검사를 거친 후 **단 하나의 해 (Schütte 의 33-광선 집합)**만이 유효함이 확인되었습니다.
• 결론: 33 개의 광선까지의 범위에서, 25 개의 완전 SI-C 집합을 포함하는 KS 집합은 Schütte 집합이 유일합니다.

5. 의의 및 결론 (Significance)

• 양자 기초 물리학: 3 차원 공간에서 최소 문맥성 구조의 기하학적 경계를 엄밀하게 정의했습니다. 이는 상태 독립적 문맥성 (SI-C) 의 최소 증인인 Yu-Oh 집합의 확장을 완전히 분류한 것입니다.
• 계산적 방법론의 발전: 조합적 생성 문제에서 대칭성 처리 (Symmetry Handling) 가 주요 병목일 때, NAUTY 와 SAT 를 결합한 RCL 프레임워크가 효과적인 해결책임을 입증했습니다.
• 실험적 적용: KS 집합은 양자 게임 및 자기 테스트 (Self-testing) 와 밀접한 관련이 있으며, 특히 Schütte 집합은 3 차원에서 최소 입력 크기를 가지는 게임 전략을 제공합니다. 본 연구는 이러한 물리적 실험의 이론적 기반을 확고히 했습니다.

이 논문은 계산 복잡도 이론과 양자 물리학의 교차점에서, 대규모 조합적 탐색 문제를 해결하기 위한 혁신적인 알고리즘적 접근을 제시했다는 점에서 중요한 의미를 가집니다.