On Proof Systems for #QBF

제목: #QBF를 위한 증명 체계에 관하여

문제 정의
본 논문은 양화된 불리언 공식(QBF)의 존재적 플레이어(existential player)를 위한 승리 전략의 수를 계산하는 #QBF 문제를 다룬다. 이 문제는 #PSPACE-complete임이 밝혀졌으며, 이는 모델 카운팅(model counting)을 수행하는 #SAT 문제보다 계산적으로 더 어려운 문제임을 의미한다. #SAT의 솔루션 수는 최대 지수적(exponential)인 반면, #QBF의 승리 전략 수는 이중 지수적(doubly exponential)일 수 있다. #SAT를 위한 증명 체계(예: KCPS, CPOG, CLIP, MICE)와 QBF를 위한 체계(예: Q-Res, ∀Exp)는 연구되어 왔으나, 일반적인 #QBF 문제에 대해 승리 전략의 수를 인증할 수 있는 전용 증명 체계는 부족한 실정이었다. d4-QBF 및 qCounter와 같은 기존 솔버들은 존재하지만, 인증을 위한 정형화된 증명 복잡도 프레임워크는 갖추지 못하고 있다.

방법론
저자들은 QBF 증명 체계와 #SAT 증명 체계의 개념을 확장하여 #QBF를 위한 새로운 증명 체계를 설계한다. 저자들은 세 가지 뚜렷한 접근 방식을 탐구한다:

1. 나이브 체계 (Naive System): $k$개의 모든 승리 전략을 열거하는 기초적인 체계이다. 이 체계는 각 전략의 정당성(Skolem 함수의 타우톨로지 증명을 통해), 전략 간의 구별 가능성(witness 할당을 통해), 그리고 다른 전략의 부재(거짓 QBF 인코딩을 통해)를 증명함으로써 그 수를 인증한다. 저자들은 이 체계가 승리 전략의 수가 이중 지수적일 때 자명한 하한(trivial lower bounds)을 갖는다는 점을 지적한다.
2. 확장 기반 체계 (Expansion-based System, ∀Exp+MICE): 이 방식은 QBF 솔빙에서 사용되는 ∀-expansion 규칙을 채택한다. 이는 모든 유니버설 변수에 대한 가능한 할당에 대해 QBF를 의미론적으로 확장하여, #QBF 문제를 #SAT 문제로 변환한다. 생성된 CNF는 이후 #SAT 증명 체계인 MICE에 의해 처리된다. 저자들은 이 체계가 유니버설 할당의 수를 보존하기 위해 반드시 모든 유니버설 할당을 확장해야 하므로, 유니버설 변수에 대해 본질적으로 지수적 크기를 요구한다고 주장한다.
3. 라인 기반 체계 (Line-based System, Q-MICE): 본 논문의 주요 기여는 Q-MICE(Quantified Model-counting Induction by Claim Extension)의 제안이다. MICE 시스템에서 영감을 받은 Q-MICE는 각 라인이 $(Q.F, A, c)$ 형태의 클레임(claim)으로 구성된 라인 기반 증명 체계이다.
   • $Q.F$: 참인 QBF.
   • $A$: 일부 존재적 변수들에 대한 Skolem 함수로 구성된 부분 전략(partial strategy).
   • $c$: $A$를 완전한 승리 전략으로 확장하는 방법의 수.
   • 추론 규칙: Q-MICE는 세 가지 핵심 규칙을 사용한다:
     • 공리 규칙 (Axiom Rule): 매트릭스가 타우톨로지인 제한된 QBF에 대한 클레임을 도출하며, 이를 통해 직접적인 조합론적 확장 계산을 허용한다.
     • 조합 규칙 (Composition Rules): 클레임을 결합하거나 단순화한다. Composition-a는 서로 다른 완전한 전략들을 합산하고, Composition-b는 유일성이 증명되었을 때 전략의 제한을 제거하며, Composition-c는 "모델의 부재" 증명이 다른 전략이 존재하지 않음을 인증할 때 특정 변수에서만 차이가 나는 클레임들을 결합한다.
     • 조인 규칙 (Join Rule): 유니버설 변수에 대한 제한이 서로 다르지만 구조가 경로 그래프(path graphs)를 형성하는 두 클레임을 결합하여 그 수를 곱한다.

주요 기여 및 결과

• Q-MICE의 정형화: 논문은 Q-MICE를 정의하고 이것이 건전하고 완전함을 증명한다(정리 16). 또한 이는 다항 시간 내에 검증 가능하다.
• 지수적 분리 (Exponential Separation): 저자들은 Q-MICE가 나이브 체계 및 ∀Exp+MICE 체계보다 지수적으로 강력함을 입증한다(정리 17).
  • XOR-PAIRS 패밀리: 유니버설 변수를 확장해야 하기 때문에 ∀Exp+MICE에서는 초다항식(super-polynomial, 즉 지수적) 증명이 필요한 양화된 명제 XOR-PAIRS 공식을 도입한다. 반면, Q-MICE는 공리 및 Composition-b 규칙을 활용하여 상수 길이의 다항 크기 증명을 제공한다.
  • Indexed Affine QBF 패밀리: 단순한 암호화 과정을 나타내는 QBF 패밀리를 구축한다. 이 패밀리는 $2^n$개의 승리 전략을 가지며, 나이브 및 ∀Exp+MICE 체계에서는 지수적 증명이 필요하다. Q-MICE는 조합 및 조인 규칙을 반복 적용함으로써 선형 길이의 다항 크기 증명으로 이를 처리한다.
• 구조적 분석: 논문은 확장 기반 체계가 유니버설 변수를 다룰 때 발생하는 본질적인 구조적 약점(지수적 팽창)을 강조하는 한편, Q-MICE는 효율성을 유지하기 위해 양화사 처리와 카운팅을 교차시킨다는 점을 밝힌다.

의의 및 주장
본 논문은 Q-MICE와 같은 증명 체계의 존재가 #QBF 이론을 발전시키고, 현재 초기 단계에 있는 #QBF 솔버의 정당성을 인증하는 데 필수적이라고 주장한다. 전략을 모두 열거하지 않고도 모델 수를 인증할 수 있는 Q-MICE를 제공함으로써, 더 견고한 솔버 검증을 향한 경로를 제시한다.

저자들은 Q-MICE가 강력하지만, 아직 d4-QBF와 같은 최첨단 솔버에서 발견되는 분해(decomposition) 규칙을 포함하고 있지 않음을 겸허히 언급하며, 이를 모듈형 추론 규칙으로 추가할 수 있다고 제안한다. 또한, Q-MICE에 대한 진정한 하한(lower bound)을 설정하는 것(propositional XOR-PAIRS가 Q-MICE에서도 어려울 것이라는 가설을 세웠으나 아직 증명되지 않음)과 다른 #SAT 증명 체계(CPOG, CLIP, KCPS)를 #QBF 영역으로 확장하는 것을 향후 과제로 꼽았다. 이 논문은 새로운 실험적 솔버를 제안하는 것이 아니라, 엄격하게 이론적 증명 복잡도와 이러한 체계들 간의 분리에 집중한다.