원문 보완판 — 사실 검토 반영

SAT 를 작은 시간과 작은 공간에서 동시에 풀 수는 없다는 것은 가정 없이 증명된 몇 안 되는 하한이다. 이 글은 그 하한의 지수를 묶어 두고 있는 기법의 한계를 넘어서는 계획을 제안한다.

아이디어 개요

P vs NP를 향한 부분 성과 가운데 아무 가정 없이 성립하는 몇 안 되는 하한이 SAT에 대한 시간-공간 트레이드오프 하한이다. Fortnow가 개척하고 Lipton–Viglas, Fortnow–van Melkebeek이 발전시켰으며 Williams가 확장한 이 계열은, 간접 대각화와 교대 절충(alternation trading) 논법으로 "SAT를 n^c 시간과 n^o(1) 공간에서 동시에 푸는 알고리즘은 존재하지 않는다"를 무조건적으로 증명하며, 지수 c는 sqrt(2)에서 황금비 1.618을 거쳐 현재 2cos(pi/7) 약 1.8019까지 올라와 있다.

특히 Williams는 이 유형의 증명 탐색을 선형계획법(LP)으로 자동화했고, Buss–Williams는 표준 규칙만 쓰는 교대 절충 증명으로는 이 지수를 넘을 수 없다는 기법 내부의 한계 정리까지 확립했다. 즉 이 분야는 기법의 유효 범위와 경계가 정리 수준으로 정확히 그려져 있는 드문 영역이어서, 벽을 넘으려면 무엇을 새로 추가해야 하는지가 명확하다.

본 아이디어는 교대 절충 증명 체계에 새로운 속도향상·감속 규칙과 비상대화 성분을 주입해 지수 한계를 밀어 올리고, 무작위·양자·비결정 모델로 하한을 확장하며, 궁극적으로 임의의 상수 c에 대한 하한 — 즉 NP가 다항시간·폴리로그 공간 계산(SC)에 속하지 않는다는 분리와 그 따름정리 L ≠ NP — 을 향해 무조건 분리 부품을 축적하는 프로그램이다. 회로가 아닌 균일 모델 하한이므로 자연 증명 장벽이 적용되지 않고, 현재 틀의 한계가 Buss–Williams 정리로 정확히 그려져 있어 새 성분을 어디에 주입할지 목표가 구체적이라는 점이 이 경로의 강점이다.

구체적 진행 방법

1. 기초 문헌 정독: van Melkebeek의 서베이(A Survey of Lower Bounds for Satisfiability and Related Problems, 2007)를 뼈대로 삼고, Fortnow의 원논문(1997), Lipton–Viglas, Fortnow–van Melkebeek의 황금비 하한, Williams의 귀납적 시공간 하한 논문과 2cos(pi/7) 도달 논문을 정독한다. 각 증명을 속도향상 규칙(공간 제한 결정적 계산을 교대 계산으로 가속하는 Nepomnjascii형 시뮬레이션)과 감속 규칙(귀류 가정 "SAT가 작은 시공간에서 풀린다"로 교대를 하나씩 제거)의 적용 수열로 분해해, 규칙 목록과 손실 계수를 명세화한 기술 대장을 만든다.
2. 증명 체계 형식화와 자동 탐색 재현: Williams의 LP 정식화(Alternation-Trading Proofs, Linear Programming, and Lower Bounds)를 재구현하여 표준 규칙 아래 최적 지수가 2cos(pi/7)임을 전산으로 재확인한다. 이 도구를 이후 모든 새 규칙 실험의 실험대로 삼는다. 여기까지가 1차 마일스톤이다.
3. 한계 정리의 가정 분해: Buss–Williams의 불가능성 증명이 요구하는 증명 정규형과 공리들을 목록화하고, 각 공리를 어기는 방법 — 새로운 형태의 시뮬레이션 정리, 규칙의 비지역적 결합, 입력 길이에 따라 달라지는 비균일 증명 수열 등 — 을 후보군으로 정리한다. 한계 정리는 "표준 규칙의 조합"만 배제하므로, 규칙 집합 자체를 늘리는 것이 정당한 공략로다.
4. 새 규칙 후보 발굴: (a) 더 강한 속도향상 — 공간 제한 계산에 대한 개선된 교대 시뮬레이션이나 시간-공간 설정에 특화된 새로운 붕괴 정리, (b) 비상대화 성분 주입 — SAT의 준선형 시간 완전성(초효율 Cook 정리 — 기존 증명은 이것을 하한을 SAT 로 옮기는 데만 쓴다)의 새 쓰임, IP=PSPACE류 산술화, Williams의 알고리즘적 방법(회로-SAT 알고리즘에서 하한 도출)의 시공간 버전 이식, (c) 메타복잡도·세분화 복잡도에서 온 가정 완화형 규칙. 각 후보를 2번의 LP 실험대에 넣어 지수 개선 여부를 기계적으로 판정한다.
5. 모델 확장 병행 트랙: 무작위 기계에 대한 Diehl–van Melkebeek의 하한, 비결정 모델에서의 tautology 하한(Fortnow–van Melkebeek — 현재 최고 4^(1/3)≈1.587, Diehl–van Melkebeek–Williams), 양자 시공간 하한 계열을 같은 규칙 언어로 재기술하고, 모델이 바뀔 때 어떤 규칙이 살아남는지 비교해 규칙의 본질적 성분을 역추출한다. 주 트랙이 정체되어도 이 트랙에서 독립 논문급 성과가 나온다.
6. 중간 마일스톤 사다리: (i) LP 도구 재현·공개, (ii) 2cos(pi/7)을 넘는 최초의 개선(아무리 작아도 기법사적 사건), (iii) 폴리로그 공간에서 c=2 도달, (iv) 임의 상수 c 도달로 NP ⊄ SC 와 그 따름정리 L ≠ NP. 각 단계는 그 자체로 발표 가능한 무조건 정리다.
7. 실패 회수 계획: 새 규칙이 끝내 안 나오면, 후보 규칙들을 포함하도록 Buss–Williams 한계 정리를 확장하는 방향으로 전환한다. "이만큼 넓힌 증명 클래스로도 1.8019를 못 넘는다"는 결과 역시 장벽 지도화에 기여하는 독립 성과다.

왜 해볼 만한 가치가 있는가

1. 무조건성: 이 계열은 어떤 미증명 가설도 쓰지 않는 진짜 정리들이다. SAT라는 NP 완전 문제에 대해 일반 랜덤 액세스 모델에서 알려진 거의 유일한 하한 계열이며, 단계마다 P≠NP 방향의 분리 부품이 실제로 축적된다.
2. 자연 증명 장벽 면제: 하한 대상이 회로가 아니라 균일 시공간 제한 기계이므로, 구성적·대규모 판별자를 요구하는 Razborov–Rudich 자연 증명 장벽이 원천적으로 적용되지 않는다고 본다(자연 증명은 비균일 회로 하한에 대한 장벽이다). 회로 하한 경로가 정면으로 부딪히는 벽 하나가 여기엔 없다.
3. 상대화·대수화 장벽이 나침반 역할: 교대 절충 논법과 상대화의 관계는 오라클 접근 방식에 따라 다르다 — 감속 보조정리는 상대화하지만, 표준 공간 제한 오라클 모델에는 NTIME^A[n] ⊆ TS^A[n^1.1, log n] 인 오라클이 있어 기존 하한은 그 의미로는 이미 상대화하지 않는다(해석에 이견 있음). 이 글은 산술화·알고리즘적 방법을 새 성분 후보로 본다. 장벽이 금지선이 아니라 "여기에 새 성분을 넣어라"는 좌표로 기능하는 보기 드문 구도라는 것이 이 글의 판단이다.
4. 기법의 경계가 정리로 그려져 있음: Buss–Williams 덕분에 "새 아이디어가 필요하다"가 수사가 아니라 정리다. 무엇이 부족한지 정확히 아는 상태에서 시작하므로 연구 자원의 낭비가 적고, 어떤 개선이든 곧바로 질적 돌파로 인정된다.
5. 자동화 가능한 실험 트랙: 증명 탐색이 LP로 환원되어 있어 규칙 추가 실험을 컴퓨터로 대량 수행할 수 있다. 사람의 직관이 놓치는 규칙 조합을 기계 탐색이 찾아낼 여지가 있고, 진입 장벽이 낮아 초기 성과(도구 재현·검증)까지의 거리가 짧다.