증명 복잡도 — 짧은 증명이 없는 항진식을 찾아서
Cook 과 Reckhow 는 NP ≠ coNP 가 「어떤 증명 체계에도 짧은 증명이 없는 항진식이 있다」와 같은 말임을 보였다. 분해 체계에서는 Haken 이 지수 하한을 증명했지만, 교과서의 명제 논리 체계인 프레게 체계부터는 하한이 알려져 있지 않다.
화면·그림·수식 전수 점검(2026-10-07)으로 내용을 확인했습니다. 증명이 옳다는 뜻은 아닙니다.
Cook 과 Reckhow 는 NP ≠ coNP 가 「어떤 증명 체계에도 짧은 증명이 없는 항진식이 있다」와 같은 말임을 보였다. 이 글은 그 틀과, 분해 체계의 지수 하한에서 하한이 알려지지 않은 프레게 체계까지 증명 체계들의 현황을 살펴본다.
NP 대 coNP 를 증명의 길이로
논리식이 만족 가능하다는 것은 짧게 증명할 수 있다. 식을 참으로 만드는 값을 하나 보여 주면 된다. 그렇다면 논리식이 항진식(tautology), 곧 변수에 무엇을 넣어도 참인 식이라는 것도 언제나 짧게 증명할 수 있을까? 이것이 NP 대 coNP 문제다.
Cook 과 Reckhow 는 1979년 논문에서 이 물음에 정확한 틀을 주었다.
항진식의 집합 TAUT 에 대한 증명 체계(proof system)란 다항 시간에 계산되는 함수 f 로서 그 치역이 정확히 TAUT 인 것이다. f(x) = y 이면 x 를 y 의 증명이라 부른다. 증명이 옳은지를 다항 시간에 검사할 수 있다는 것만 요구하는 아주 넓은 정의다.
모든 항진식 y 가 길이가 |y| 의 다항식 이하인 증명을 가지면 그 체계를 다항식 유계(polynomially bounded)라 한다.
증명된 정리 NP 가 여집합에 대해 닫혀 있다(NP = coNP) ⇔ TAUT 에 다항식 유계인 증명 체계가 있다.
따라서 NP ≠ coNP 는 「어떤 증명 체계를 가져와도 짧은 증명이 없는 항진식들이 있다」와 같은 말이다. P = NP 이면 NP = coNP 이므로, NP ≠ coNP 를 증명하면 P ≠ NP 도 따라 나온다.
「어떤 증명 체계」의 범위는 넓다. 분해나 프레게 같은 논리 체계만이 아니라, 집합론 ZFC 안에서의 증명을 그대로 쓰는 것도 하나의 증명 체계다. 그러니 이 명제는 수학의 어떤 방법을 동원해도 짧게 증명할 수 없는 항진식이 있다는 뜻이 된다.
여기서 연구 계획이 나온다. 모든 증명 체계를 한꺼번에 다루기는 어려우니, 약한 체계부터 차례로 「이 체계에는 짧은 증명이 없는 항진식이 있다」를 증명해 올라간다. 체계의 강약은 한 체계의 증명을 다른 체계의 증명으로 다항 시간에 옮길 수 있는가로 견준다. 두 사람은 통상의 체계들이 다항식 유계가 아닐 것이라고 추측했다.
분해 체계의 지수 하한
가장 잘 이해된 체계는 분해(resolution)다. 식이 만족 불가능함을 보이는 체계로, 두 절 (x ∨ A) 와 (¬x ∨ B) 에서 새 절 (A ∨ B) 를 끌어내는 규칙 하나만 쓴다. 빈 절이 나오면 원래 식은 만족 불가능하다.
작은 예: 분해 규칙 따라가기
세 절 (x), (¬x ∨ y), (¬y) 를 모두 참으로 만들 수 없음을 보이자.
- (x) 와 (¬x ∨ y) 에서 x 를 지워 새 절 (y) 를 얻는다.
- (y) 와 (¬y) 에서 y 를 지우면 빈 절이 나온다.
- 빈 절이 나왔으므로 원래 식은 만족 불가능하다.
1985년 Haken 은 비둘기집 원리(n+1 마리의 비둘기를 n 개의 집에 한 마리씩만 넣을 수는 없다)를 나타내는 식들은 분해 증명이 지수적으로 길 수밖에 없음을 보였다. Aaronson 의 풀이로는, 분해는 「이 비둘기를 여기에, 저 비둘기를 저기에」 하는 국소적 추론만 할 수 있고 비둘기의 수를 세는 추론을 하지 못한다. 뒤에 Ben-Sasson 과 Wigderson 은 「짧은 증명은 좁다」는 원리로 이 증명을 훨씬 단순하게 만들었다.
이 결과는 알고리즘에도 뜻이 있다. 널리 쓰이는 DPLL 계열 만족 가능성 알고리즘이 만족 불가능한 식을 처리한 과정은 분해 증명으로 읽을 수 있다. 그래서 이런 알고리즘은 비둘기집 식에서 지수 시간이 걸린다.
더 강한 체계에서는
| 증명 체계 | 알려진 것 |
|---|---|
| 분해 | 비둘기집 원리에 지수 하한 (Haken, 1985) |
| 깊이가 제한된 프레게 체계 | 비둘기집 원리에 초다항 하한 (Ajtai, 1988), 뒤에 지수 하한으로 강화 |
| 절단 평면(cutting planes) | 지수 하한 (Pudlák, 1997) |
| 프레게(Frege) 체계: 교과서의 명제 논리 | 비자명한 하한이 없다. 비둘기집 원리는 다항 크기 증명을 가진다 (Buss, 1987) |
| 확장 프레게 체계: 식에 줄임 기호를 허용 | 하한이 없다 |
Buss 의 결과는 비둘기집 원리가 프레게 체계에서는 어려운 예가 아니라는 뜻이다. 프레게 체계는 분해보다 지수적으로 강하고, 이 체계의 하한을 얻으려면 다른 종류의 어려운 항진식이 있어야 한다.
회로 하한과의 닮음도 눈에 띈다. 깊이가 제한된 프레게 체계의 하한은 AC⁰ 하한에 쓰인 무작위 제한법으로 얻었다. 그리고 회로 쪽과 마찬가지로 그 너머에서는 진전이 멈춰 있다. 프레게 체계에 대한 비자명한 하한은 오랜 미해결 문제다.
이 길의 위치
- 프레게 체계의 하한이 나오더라도 P ≠ NP 에는 못 미친다고 Fortnow 는 짚는다. 임의의 증명 체계에 대해 보여야 하기 때문이다.
- NP ≠ coNP 는 P ≠ NP 보다 강한 명제다. Aaronson 은 회로 크기의 하한이 대응하는 증명 복잡도 하한보다 「다소 쉬운」 편이라고 본다.
- 알려진 형식적 장벽은 없다. 다만 자연 증명과 이어지는 결과가 있다. Razborov 는 유계 산술(bounded arithmetic)의 어떤 체계에서는 일반 회로에 대한 초다항 하한의 증명이 모두 자연 증명으로 바뀜을 보였다.
- 다른 모든 체계만큼 효율적인 「최적의 증명 체계」가 있는지도 미해결이다.
출처
- S. A. Cook, R. A. Reckhow, "The Relative Efficiency of Propositional Proof Systems", J. Symbolic Logic 44(1), 36–50 (1979). 저자 공개본에서 §1(명제 1.1, 정의 1.3, 명제 1.4, 정의 1.5 와 추측)을 확인.
- A. Haken, "The Intractability of Resolution", Theoret. Comput. Sci. 39, 297–308 (1985). 서지는 DOI 등록 정보로, 내용은 Aaronson 2017 정리 46 과 Fortnow 2009 §4.3 으로 확인.
- E. Ben-Sasson, A. Wigderson, "Short Proofs Are Narrow — Resolution Made Simple", J. ACM 48(2), 149–169 (2001). 서지는 DOI 등록 정보로, 내용은 Aaronson 2017 §6.2.1 각주로 확인.
- S. R. Buss, "Polynomial Size Proofs of the Propositional Pigeonhole Principle", J. Symbolic Logic 52(4), 916–927 (1987). 학술지 페이지의 초록을 확인.
- M. Ajtai, "The Complexity of the Pigeonhole Principle", FOCS 1988, 346–355. 서지는 DOI 등록 정보로, 내용은 Wikipedia 「Proof complexity」 로 확인.
- P. Pudlák, "Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations", J. Symbolic Logic 62(3), 981–998 (1997). 서지는 DOI 등록 정보로, 내용은 Wikipedia 「Proof complexity」 로 확인.
- J. Krajíček, P. Pudlák, "Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations", J. Symbolic Logic 54(3), 1063–1079 (1989). 서지는 DOI 등록 정보로, 최적 증명 체계 문제가 미해결이라는 점은 Wikipedia 「Proof complexity」 로 확인.
- J. Krajíček, "Proof Complexity", Proc. 4th European Congress of Mathematics, 221–231 (2005). 저자 공개본의 머리말과 §2 를 확인.
- Wikipedia, "Proof complexity" (보조 자료). 「Lower bounds」 절과 미해결 문제 서술을 확인.
- A. A. Razborov, S. Rudich, "Natural Proofs", J. Comput. System Sci. 55(1), 24–35 (1997). 저자 공개본 §1 에서 유계 산술에 관한 서술을 확인.
- S. Aaronson, "P =? NP", 저자 공개본(2017). §6.2.1 을 확인.
- L. Fortnow, "The Status of the P versus NP Problem", Commun. ACM 52(9), 78–86 (2009). §4.3 을 확인.
출처·이용 조건: 직접 작성
참고문헌 12
- 접근원문 확인The relative efficiency of propositional proof systemsStephen A. Cook, Robert A. Reckhow · 1979The Journal of Symbolic Logic 44(1), 36–50쪽 (1979) · 예비판 「On the lengths of proofs in the propositional calculus」, STOC 1974, 135–148쪽
명제 증명 체계를 일반적으로 정의하고 증명 길이의 문제를 NP 대 coNP 문제와 이은 논문이다. 모든 항진식에 다항 길이의 증명을 주는 증명 체계가 있는 것과 NP = coNP 가 같은 말임을 보여 증명 복잡도라는 분야의 틀을 세웠다. 증명 복잡도 접근을 공부하려는 독자의 출발점이다. Cook 의 누리집에 있는 공개본으로 연결한다.
확인:저자 공개본을 열어 §1(명제 1.1·1.4, 정의 1.3·1.5)을 읽음. - 부분 결과서지만 확인The intractability of resolutionArmin Haken · 1985Theoretical Computer Science 39, 297–308쪽 (1985)
비둘기집 원리를 resolution 으로 증명하려면 지수 길이가 필요함을 보인 논문이다. resolution 증명 체계에 대한 지수 하한의 원전으로, 증명 복잡도의 대표 결과다. resolution 에 바탕을 둔 SAT 풀이 프로그램의 한계를 이해하려는 독자에게도 뜻이 있다. 게시자(Elsevier) 페이지로 연결된다.
확인:게시자 누리집이 자동 접속을 막아 원문을 열지 못함. 서지는 Crossref 의 DOI 등록 기록으로, 내용은 Aaronson 2017 정리 46 과 Fortnow 2009 §4.3 으로 확인. - 부분 결과서지만 확인Short Proofs Are Narrow — Resolution Made SimpleE. Ben-Sasson, A. Wigderson · 2001Journal of the ACM 48(2), 149–169쪽 (2001) · 학회 발표 STOC 1999, 517–526쪽
「짧은 증명은 좁다」는 원리로 분해 체계의 하한 증명을 단순하게 만든 논문이다. Haken 의 지수 하한 증명을 훨씬 단순하게 만든 논문으로, 2-3 의 증명 복잡도 글이 인용한다. ACM 디지털 도서관으로 연결된다.
확인:원문은 확인하지 못함. 서지는 DOI 등록 기록으로, 내용은 Aaronson 2017 §6.2.1 의 각주로 확인. - 부분 결과서지만 확인Polynomial Size Proofs of the Propositional Pigeonhole PrincipleS. R. Buss · 1987Journal of Symbolic Logic 52(4), 916–927쪽 (1987)
비둘기집 원리가 프레게 체계에서는 다항 크기 증명을 가짐을 보인 논문이다. 비둘기집 원리가 프레게 체계에서는 어려운 예가 아니라는 뜻으로, 2-3 의 증명 복잡도 글이 체계별 하한 표에서 인용한다.
확인:학술지 페이지의 초록까지 확인. 본문을 읽었다는 기록은 없음. - 부분 결과서지만 확인The Complexity of the Pigeonhole PrincipleM. Ajtai · 1988FOCS 1988 (29th Annual Symposium on Foundations of Computer Science), 346–355쪽 · 학술지 게재 Combinatorica 14(4), 417–433쪽 (1994)
깊이가 제한된 프레게 체계에서 비둘기집 원리의 증명에 초다항 하한을 보인 논문이다. 분해 다음 단계의 증명 체계에 대한 하한으로, 뒤에 지수 하한으로 강화되었다. 2-3 의 증명 복잡도 글이 체계별 하한 표에서 인용한다.
확인:원문은 확인하지 못함. 서지는 DOI 등록 기록으로, 내용은 영어 위키백과 「Proof complexity」 문서로 확인. - 부분 결과서지만 확인Lower Bounds for Resolution and Cutting Plane Proofs and Monotone ComputationsP. Pudlák · 1997Journal of Symbolic Logic 62(3), 981–998쪽 (1997)
절단 평면 증명 체계에 대한 지수 하한을 증명한 논문이다. 2-3 의 증명 복잡도 글이 체계별 하한 표에서 인용한다.
확인:원문은 확인하지 못함. 서지는 DOI 등록 기록으로, 내용은 영어 위키백과 「Proof complexity」 문서로 확인. - 접근서지만 확인Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of ComputationsJ. Krajíček, P. Pudlák · 1989Journal of Symbolic Logic 54(3), 1063–1079쪽 (1989)
명제 증명 체계, 일차 이론의 무모순성, 계산 복잡도 사이의 관계를 다룬 논문이다. 다른 모든 체계만큼 효율적인 「최적의 증명 체계」가 있는가라는 미해결 문제와 관련해, 2-3 의 증명 복잡도 글이 인용한다.
확인:원문은 확인하지 못함. 서지는 DOI 등록 기록으로, 최적 증명 체계 문제가 미해결이라는 점은 영어 위키백과 「Proof complexity」 문서로 확인. - 개관원문 확인Proof ComplexityJ. Krajíček · 2005Proceedings of the 4th European Congress of Mathematics (Stockholm 2004), European Mathematical Society, 221–231쪽 (2005)
증명 복잡도 분야를 소개한 유럽 수학자 대회(2004) 논문집의 글이다. 2-3 의 증명 복잡도 글이 분야의 틀을 정리하는 데 썼다. 저자 누리집의 공개본으로 연결한다.
확인:저자 공개본을 열어 머리말과 §2 를 읽음. - 보조 자료원문 확인Proof complexityWikipedia contributors · 2026영어 위키백과 (2026년 확인)
증명 복잡도를 다룬 영어 위키백과 문서다. 2-3 의 증명 복잡도 글이 체계별 하한의 목록과 미해결 문제 서술을 확인하는 보조 자료로 썼다.
확인:위키백과 문서를 직접 열어 「Lower bounds」 절과 미해결 문제 서술을 확인(2차 자료). - 장벽원문 확인Natural proofsAlexander A. Razborov, Steven Rudich · 1997Journal of Computer and System Sciences 55(1), 24–35쪽 (1997) · 학회 발표 STOC 1994 (Proceedings of the 26th Annual ACM Symposium on Theory of Computing), 204–213쪽
알려진 회로 하한 증명들의 공통된 꼴을 「자연 증명」으로 정식화하고 그 한계를 보인 논문이다. 어려움에 관한 가정(강한 유사난수 생성기의 존재)이 참이라면 자연 증명으로는 일반 회로에 대한 초다항 하한을 증명할 수 없다는 둘째 장벽의 원전이다. 회로 하한 연구가 왜 막혔는지 이해하려는 독자에게 권한다. 게시자(Elsevier) 페이지로 연결된다.
확인:저자 공개본을 열어 §2(정의), §3.1, §4(정리 4.1·4.3)를 읽음. 연결한 게시자 주소의 서지는 DOI 등록 기록으로 확인. - 개관원문 확인P =? NPScott Aaronson · 2017ECCC TR17-004 (2017년 1월 8일 공개) · 책 Open Problems in Mathematics (John Forbes Nash Jr., Michael Th. Rassias 엮음, Springer, 2016), 1–122쪽에 실린 글
P 대 NP 문제의 의미와 알려진 결과, 장벽, 접근 전반을 120여 쪽에 정리한 개관이다. 수학·과학·공학 배경의 넓은 독자를 겨냥해, 왜 P ≠ NP 라고 믿는지, 왜 증명이 어려운지, 지난 반세기에 무엇이 진전되었는지를 저자의 관점과 함께 설명한다. 상대화·자연 증명·대수화 장벽과 GCT 까지 다루므로, 이 서비스의 2부를 한 편으로 깊이 읽고 싶은 독자에게 가장 먼저 권한다.
확인:저자 공개본(2017년 판)을 열어 인용한 절들을 읽음. - 개관원문 확인The status of the P versus NP problemLance Fortnow · 2009Communications of the ACM 52(9), 78–86쪽 (2009)
P 대 NP 문제의 의미와 2009년 시점의 연구 상황을 전산학 일반 독자에게 풀어 쓴 개관이다. 문제를 풀려던 시도들과 그 한계, NP-완전 문제를 현실에서 다루는 법, 양자 컴퓨터의 가능성까지 짧게 훑는다. 수식이 거의 없어 입문 독자가 처음 읽을 영어 글로 알맞다. 저자 누리집의 공개본으로 연결한다.
확인:저자 공개본을 열어 인용한 절들을 읽음.
하위 정보 0
이 자료에 대한 질의 · 보완 · 반론 · 관련 자료 · 메모를 글이나 파일로 더합니다.
아직 없습니다.