이 논문은 2023 년 QBF 갤러리라는 대규모 '지능형 퍼즐 대회'의 결과를 정리한 보고서입니다. 여기서 '퍼즐'은 컴퓨터 과학에서 매우 복잡한 논리 문제인 **QBF(양자화된 불리언 공식)**를 의미합니다.
이 대회를 이해하기 위해 다음과 같은 비유를 들어 설명해 드리겠습니다.
1. 대회는 무엇인가요? (QBF 갤러리)
상상해 보세요. 전 세계의 가장 똑똑한 **로봇 해설가들 (솔버, Solvers)**이 모여서, 인간이 만든 **초난감한 미로 (공식, Formulas)**를 통과하는 대회를 열었습니다.
미로 (QBF): 단순히 "A 가 참인가?"를 묻는 게 아니라, "A 가 참일 때 B 는 어떨까? 그리고 C 는 A 와 B 에 따라 어떻게 변할까?"처럼 변수들이 서로 얽히고설킨 복잡한 논리 구조입니다.
해설가들 (솔버): 이 미로를 가장 빠르고 정확하게 통과하는 알고리즘 프로그램들입니다.
목적: 누가 가장 잘하는지 경쟁하는 것뿐만 아니라, "어떤 종류의 미로가 가장 어려운지", "어떤 해설가들이 어떤 미로에 강한지"를 분석하여 미래의 인공지능과 소프트웨어 검증 기술을 발전시키는 것입니다.
2. 대회의 주요 트랙 (경쟁 종목)
이번 대회는 미로의 모양에 따라 4 가지 다른 종목으로 나뉘어 진행되었습니다.
PCNF 트랙 (정형화된 미로): 모든 미로가 미리 정해진 규칙 (전치형) 에 맞춰져 있습니다. 가장 많은 참가자들이 이 종목에 참여했습니다.
PNCNF 트랙 (자유로운 미로): 규칙이 덜 엄격해서, 미로의 구조가 더 자유롭고 복잡합니다.
DQBF 트랙 (의존성 미로): 변수들 사이에 특별한 '의존 관계'가 있는 미로로, 가장 어려운 난이도를 자랑합니다.
크래프트드 (Crafted) 트랙 (인위적 난이도): 수학자들이 의도적으로 만든, 특정 해설가의 약점을 공략하기 위해 설계된 미로들입니다.
3. 참가자들 (솔버와 전처리기)
해설가들 (솔버): 각자 다른 전략 (CEGAR, QCDCL 등) 을 가진 프로그램들이 참가했습니다. 어떤 해설가는 미로를 잘게 쪼개서 풀고, 어떤 해설가는 미로의 전체 구조를 파악해서 풀었습니다.
미리 정리하는 도우미 (전처리기, Preprocessors): 해설가들이 미로에 들어가기 전에, 미로의 불필요한 벽을 허물거나 길을 정리해주는 도구들입니다. 이 도우미가 미로를 정리해주면 해설가들이 훨씬 쉽게 통과할 수 있습니다.
4. 주요 발견 사항 (결과 요약)
🏆 누가 이겼나요?
CAQE 시리즈: 'CAQE'라는 이름의 해설가 세 가지 버전 (Bloqqer, HQSpre, pre) 이 가장 많은 미로를 통과했습니다. 특히 CAQE-pre가 전체적으로 가장 좋은 성적을 거두었습니다.
전처리기의 힘: 미로를 정리해주는 '도우미'를 사용하면 해설가들의 성적이 크게 향상되었습니다. 하지만 모든 해설가에게 똑같은 도우미가 좋은 것은 아니었습니다. 어떤 해설가는 A 도우미와, 또 다른 해설가는 B 도우미와 짝을 이루었을 때 가장 잘 작동했습니다.
📊 미로의 난이도
너무 쉽거나 너무 어렵지 않게: 대회 주최측은 "너무 쉬워서 1 초 만에 다 풀리는 미로"나 "너무 어려워서 모든 해설가가 15 분 (제한 시간) 을 다 써도 못 푸는 미로"는 제외했습니다. 오직 해설가들의 실력을 가려낼 수 있는 적절한 난이도의 미로들만 최종 선정되었습니다.
새로운 미로: 이번 대회에는 기존에 없던 새로운 미로들이 대거 추가되었습니다. 특히 논리 구조가 자유로운 '비 CNF' 형태의 미로가 많이 등장했습니다.
🔍 흥미로운 사실
해설가들의 성향: 어떤 해설가는 '참 (SAT)'인 미로를 잘 풀고, 어떤 해설가는 '거짓 (UNSAT)'인 미로를 잘 풀었습니다. 마치 어떤 선수가 공격은 잘하지만 수비는 약한 것과 비슷합니다.
비슷한 해설가들: heatmap(열지도) 분석을 통해, 어떤 해설가들은 서로 매우 비슷하게 행동한다는 것을 발견했습니다. 반면, 어떤 해설가들은 전혀 다른 방식으로 문제를 접근했습니다.
5. 이 대회가 우리에게 주는 의미
이 보고서는 단순히 "누가 1 등이다"를 알려주는 것을 넘어, 어떤 기술이 어떤 상황에서 효과적인지에 대한 지도를 제공합니다.
미래의 소프트웨어: 이 기술들은 자동차의 자동 주행 시스템, 반도체 설계, 혹은 중요한 보안 시스템이 제대로 작동하는지 검증하는 데 쓰입니다.
오픈 소스: 대회에서 사용된 모든 미로와 결과는 공개되었습니다. 이는 전 세계 연구자들이 이 데이터를 바탕으로 더 똑똑한 AI 를 만들 수 있다는 뜻입니다.
요약
"2023 년 QBF 갤러리"는 복잡한 논리 퍼즐을 푸는 최강의 알고리즘들을 한자리에 모아, 누가 어떤 상황에서 가장 뛰어난지 분석한 '지능 대결 보고서'입니다. 이를 통해 우리는 더 강력한 소프트웨어 검증 도구를 개발하고, 인공지능의 한계를 넓혀갈 수 있는 통찰을 얻었습니다.
QBF Gallery 2023 기술 보고서 요약
이 문서는 2023 년에 개최된 QBF Gallery의 기술 보고서로, 양화 부울 논리식 (Quantified Boolean Formulas, QBF) 해결사 (Solver) 와 벤치마크의 최신 상태를 조사하고 문서화한 내용을 담고 있습니다. 본 보고서는 QBF 커뮤니티의 연구 및 벤치마킹을 지원하기 위해 제출된 솔버와 공식 (Formulas) 을 분석하고, 새로운 통합 벤치마크 세트를 공개하며, 다양한 트랙별 성능을 비교 평가합니다.
1. 문제 정의 (Problem)
QBF 결정 문제는 PSPACE-완전 (PSPACE-complete) 문제로 알려져 있으며, SAT 문제보다 더 높은 계산 복잡도를 가집니다. 이는 형식 검증 (Formal Verification), 합성 (Synthesis), 인공지능 등 다양한 분야에서 핵심적인 역할을 합니다. QBF Gallery 는 기존 QBFEval 과는 달리 경쟁적 평가보다는 커뮤니티 참여와 결과 분석에 중점을 둔 오프라인 가상 이벤트입니다. 이 행사의 주요 목적은 다음과 같습니다.
최신 QBF 솔버 및 벤치마크의 상태 파악.
다양한 입력 형식 (PCNF, QCIR, DQBF 등) 에 대한 솔버 성능 비교.
새로운 벤치마크 세트 구축을 통한 연구 방향성 제시.
2. 방법론 (Methodology)
2.1 트랙 구성 (Tracks)
2023 년 QBF Gallery 는 다음과 같은 5 가지 트랙으로 구성되었습니다.
Prenex CNF (PCNF) Track: 표준 QDIMACS 형식을 사용하는 전치형 (Prenex) 컨쥬네이티브 정규형 (CNF) 공식. 가장 많은 솔버와 벤치마크가 제출됨.
Prenex Non-CNF (PNCNF) Track: QCIR (Quantified Circuit) 형식을 사용하는 전치형이지만 CNF 가 아닌 구조의 공식.
DQBF Track: 의존성 QBF (Dependency QBF) 트랙으로, Henkin 양화자를 사용하여 NEXPTIME-complete 문제를 다룸. (새로운 공식은 제출되지 않아 이전 데이터 재사용)
Crafted Instances Track: 증명 복잡도 (Proof Complexity) 에서 유래한 인위적으로 제작된 공식들. 증명 시스템의 강점과 약점을 분석하기 위해 사용.
Preprocessor Track: 주어진 공식을 해결하기 쉽게 변환하거나 불필요한 부분을 제거하는 전처리 도구 평가.
2.2 실험 환경
하드웨어: 오스트리아 린츠의 Johannes Kepler University (JKU) 내 Symbolic AI 연구소 클러스터 (20 노드, AMD EPYC 7313, 16 코어/소켓).
제한 조건: 각 공식당 **15 분 (900 초)**의 시간 제한과 8GB 메모리 제한을 적용 (일부 실험에서는 100GB 메모리 테스트도 수행).
벤치마크 선정: 제출된 공식 중 모든 솔버가 1 초 이내에 해결하거나 (너무 쉬움), 모든 솔버가 타임아웃 (너무 어려움) 하는 공식은 제외하여 적정 난이도의 공식만 최종 벤치마크 세트로 선정됨.
2.3 평가 지표
해결된 공식 수 (Solved Instances): 시간 제한 내에 해결한 공식의 수.
PAR-2 점수: 해결된 공식의 실행 시간 합 + (해결되지 않은 공식 수 × 타임아웃 시간 × 2) 를 총 공식 수로 나눈 값. 점수가 낮을수록 성능이 우수함.
유일 해결 (Uniquely Solved): 다른 어떤 솔버도 해결하지 못한 공식을 해결한 수.
상관관계 분석 (Similarity): 솔버 간 실행 시간 패턴의 유사성을 Spearman 순위 상관 계수로 분석 (히트맵 시각화).
3. 주요 기여 (Key Contributions)
통합 벤치마크 세트 공개:
PCNF 트랙: 4 명의 저자가 제출한 518 개 공식 중 130 개를 선정 (Linear Domino, Nested Counterfactuals, Matrix Multiplication 등).
PNCNF (QCIR) 트랙: 5 명의 저자가 제출한 418 개 공식 중 200 개를 선정 (Hyper-Properties, Hadwiger Conjecture, Circuit Minimization 등).
DQBF 트랙: 이전 세대의 354 개 공식 재사용.
Crafted Instances: 14 가지 공식 계열 (Family) 에서 71 개씩 총 994 개 생성.
이 모든 데이터는 공개되어 향후 연구의 기초 자료로 활용됨.
솔버 및 전처리 도구 평가:
PCNF 트랙: CAQE (Bloqqer, HQSpre, Pre 버전), DepQBF, RAReQS, Qute 등 12 개 솔버 평가.
PNCNF 트랙: QuAbS, CQESTO, GhostQ, miniQU 등 11 개 솔버 평가.
DQBF 트랙: Pedant, DQBDD, HQS 등 4 개 솔버 평가.
Preprocessor: Bloqqer, HQSpre, QRATPre+ 의 성능 비교.
새로운 분석 기법 도입:
솔버 간 성능 유사성을 시각화한 히트맵 (Heatmap) 제공.
벤치마크 세트별 성능을 보여주는 스파이더 플롯 (Spiderplot) 을 통해 특정 문제 유형에 대한 솔버의 강약점 분석.
4. 결과 (Results)
4.1 PCNF 트랙 (QDIMACS)
성능:CAQE 시리즈 (특히 CAQE-pre) 가 가장 많은 공식을 해결 (231 개) 하여 1 위를 차지했습니다.
유일 해결:dynQBF가 가장 많은 유일 해결 공식 (16 개) 을 기록했으나, 전체 해결 수는 CAQE 에 미치지 못했습니다.
메모리 영향: 일부 솔버 (RAReQS, miniQU-q) 는 메모리 제한을 100GB 로 늘렸을 때 해결 수가 크게 증가했습니다. 반면 dynQBF 는 실행 간 결과 편차가 커서 재현성 문제가 지적되었습니다.
전처리 효과: Bloqqer, HQSpre, QRATPre+ 전처리기를 적용한 결과, 대부분의 솔버가 성능 향상을 보였으나, 최적의 전처리기는 솔버마다 달랐습니다.
4.2 PNCNF 트랙 (QCIR)
성능:QuAbS-CAQE-HQSpre가 286 개 공식을 해결하여 1 위를 차지했습니다.
특이점: QCIR 솔버들은 PCNF 솔버들과 달리 SAT(참) 인 공식을 더 많이 해결하는 경향을 보였습니다.
유일 해결:CQESTO가 9 개의 유일 해결 공식을 기록하여 두 번째로 높은 성능을 보였습니다.
4.3 DQBF 트랙
성능:Pedant 솔버가 284 개 공식을 해결하여 1 위를 차지했습니다.
참고: 이 트랙에서는 새로운 공식이 제출되지 않아 기존 데이터만 사용되었습니다.
4.4 Crafted Instances
CAQE-Bloqqer가 모든 공식 계열 (Family) 에서 모든 71 개의 공식을 해결한 유일한 솔버였습니다.
다른 솔버들은 특정 계열 (예: Qute 는 EQ 계열, CAQE 는 KBKF 계열) 에 강점을 보였으나, 전반적인 범용성은 CAQE-Bloqqer 가 가장 뛰어났습니다.
4.5 솔버 유사성 분석
PCNF 트랙에서는 솔버 간 실행 시간 패턴의 상관관계가 낮아 (다양한 강점 존재) 벤치마크 세트의 다양성이 부족함을 시사했습니다.
PNCNF 트랙에서는 솔버 간 유사성이 더 높게 나타났습니다.
5. 의의 및 결론 (Significance)
커뮤니티 발전: QBF Gallery 2023 은 비경쟁적, 협력적 환경에서 솔버 개발자와 연구자들이 서로의 결과를 공유하고 분석할 수 있는 중요한 플랫폼을 제공했습니다.
데이터 공개: 새로 선정된 300 개 이상의 고품질 벤치마크 공식과 다양한 솔버의 성능 데이터를 공개함으로써, 향후 QBF 연구의 표준적인 평가 기준을 마련했습니다.
기술적 통찰:
전처리기의 중요성: 전처리가 솔버 성능에 결정적인 영향을 미치며, 솔버와 전처리기의 조합 최적화가 필요함을 입증했습니다.
형식 변환의 가치: 동일한 문제를 다른 형식 (QDIMACS vs QCIR) 으로 변환하여 해결할 때 성능 차이가 발생하므로, 형식 변환 도구의 중요성이 부각되었습니다.
다양한 접근법: CEGAR, QCDCL, Expansion 등 다양한 알고리즘 접근법이 서로 다른 문제 유형에서 우위를 점함을 보여주었습니다.
이 보고서는 QBF 해결 기술의 현재 수준을 종합적으로 정리하고, 향후 더 다양하고 도전적인 벤치마크와 솔버 개발을 위한 방향성을 제시한다는 점에서 학술적, 실용적 가치가 매우 높습니다.