SAT 풀이기

소프트웨어 수치해석 마지막 수정: 2026-08-29 04:27:40

1. 개요[편집]

SAT 풀이기 SAT solver
입력	명제 논리식 (보통 CNF, DIMACS 형식)
출력	충족 배정 또는 «충족 불가능» + 반박 증명
이론 복잡도	NP-완전 (쿡-레빈, 1971)
주력 알고리즘	DPLL(1962) → CDCL(1996~)
핵심 부품	단위 전파 · 1UIP 절 학습 · 비시간순 백점프 · VSIDS · two-watched literals · 재시작
실무 규모	산업 인스턴스 변수 $10^6$ 이상도 초 단위
최난 지점	랜덤 3-SAT $\alpha = m/n \approx 4.27$
대표 구현	MiniSat · Glucose · CaDiCaL · Kissat

SAT 풀이기(SAT solver)는 명제 논리식을 참으로 만드는 변수 배정이 존재하는지 판정하고, 있으면 그 배정을, 없으면 없다는 증명을 내놓는 프로그램이다. 입력은 거의 항상 논리곱 표준형(CNF) — 리터럴의 논리합인 절(clause)들의 논리곱 — 이고, 사실상의 표준 파일 형식은 DIMACS CNF다.

이 물건이 흥미로운 이유는 한 문장으로 요약된다. SAT 은 최초로 NP-완전임이 증명된 문제인데, 지난 30년간 가장 성공적으로 “그럼에도 실무에서 풀리게” 된 문제이기도 하다. 1990년대 초까지 변수 수백 개짜리도 버거웠던 것이, 지금은 변수 수백만·절 수천만 개짜리 하드웨어 검증 인스턴스가 노트북에서 몇 초에 끝난다. 그 사이에 $\mathrm{P} = \mathrm{NP}$ 가 증명된 것은 물론 아니고, 실제 문제 인스턴스가 최악의 경우와 전혀 다르게 생겼다는 사실을 공학적으로 뽑아먹은 결과다. 그래서 SAT 풀이기는 “이론적 난이도와 실무적 난이도는 다른 축이다”라는 명제의 가장 유명한 물증으로 인용된다.

절 길이를 2 로 제한하면 선형 시간에 풀린다는 것은 2-SAT 문서에서 다뤘다. 여기서는 길이 3 이상, 즉 진짜 NP-완전 영역의 이야기다.

2. DPLL — 뼈대[편집]

1960년 데이비스와 퍼트넘의 원본 알고리즘은 분해(resolution) 기반이었는데 메모리가 폭발했다. 2년 뒤 데이비스·로지먼·러브랜드가 분해를 분기로 바꿔 메모리 문제를 없앤 것이 오늘날 말하는 DPLL 이다.¹ 골격은 백트래킹, 즉 해 공간 트리 위의 깊이 우선 탐색이다.

DPLL(F):
    F = 단위 전파(F);  F = 순수 리터럴 제거(F)
    if F 에 빈 절: return UNSAT
    if 모든 절이 만족: return SAT
    x = 분기 변수 선택
    return DPLL(F ∧ x) or DPLL(F ∧ ¬x)

두 개의 가지치기 규칙이 전부다.

단위 전파(unit propagation, BCP) — 어떤 절에 미배정 리터럴이 딱 하나 남았으면 그 리터럴은 참일 수밖에 없다. 강제된 배정을 하고 나면 또 다른 절이 단위절이 되어 연쇄가 일어난다. 현대 풀이기 실행 시간의 80~90 %가 여기서 소모되며, 그래서 성능 개선의 대부분이 “BCP 를 어떻게 더 싸게 하느냐”의 문제다.
순수 리터럴(pure literal) — 어떤 변수가 논리식 전체에서 한쪽 부호로만 나타나면 그쪽으로 배정해도 손해가 없다. 개념적으로는 깔끔하지만, 뒤에 나올 감시 리터럴 자료구조와 궁합이 나빠서(부호별 등장 횟수를 정확히 유지하려면 비용이 든다) 현대 CDCL 풀이기는 탐색 중에는 대체로 쓰지 않고 전처리 단계에서만 적용한다. 교과서와 실제 코드가 갈리는 대표적인 지점.

3. CDCL — 충돌에서 배우기[편집]

DPLL 을 산업용으로 바꾼 것은 1996년 마르케스-실바와 사칼라의 GRASP, 그리고 1997년 바야르도와 슈래그의 rel_sat 가 도입한 충돌 주도 절 학습(conflict-driven clause learning, CDCL)이다.² 아이디어는 이렇다. 순진한 백트래킹은 모순에 부딪히면 그냥 마지막 분기를 뒤집고 마는데, 그러면 같은 이유로 같은 모순에 몇 번이고 다시 부딪힌다. 실패의 원인을 명시적으로 추출해서 논리식에 새 절로 추가해 두면, 탐색 트리의 다른 가지에서 똑같은 실수를 반복하지 않는다.

원인 추출은 함의 그래프로 한다. 배정된 리터럴이 정점, “이 절 때문에 이 리터럴이 강제됐다”가 간선인 DAG 다. 결정 리터럴은 진입차수 0 이고, 어떤 절의 모든 리터럴이 거짓이 되는 순간 충돌 정점이 생긴다. 충돌 정점에서 역방향으로 절단(cut)을 하나 그으면, 절단의 결정 쪽에 걸린 리터럴들의 부정이 곧 학습 절이다. 어디를 자르느냐에 따라 여러 학습 방식이 나오는데, 실전의 표준은 1UIP(first unique implication point)다.

UIP — 현재 결정 레벨에서 결정 리터럴로부터 충돌 정점으로 가는 모든 경로가 반드시 지나는 정점. 결정 리터럴 자신도 항상 UIP 이므로 최소 하나는 존재한다.
1UIP — 충돌에서 거슬러 올라갈 때 처음 만나는 UIP. 여기서 자르면 학습 절에 현재 레벨의 리터럴이 정확히 하나만 남는다.

1UIP 절이 좋은 이유는 그 절이 단언적(asserting)이라는 데 있다. 학습 절 안에서 두 번째로 높은 결정 레벨까지 되돌아가면, 그 절이 자동으로 단위절이 되어 곧바로 새로운 전파를 강제한다. 즉 되돌아가자마자 탐색이 새 정보를 들고 다시 출발한다. 이때의 되돌아가기가 비시간순 백점프(non-chronological backjumping)로, 한 레벨씩 물러나는 게 아니라 충돌과 무관한 결정들을 통째로 건너뛴다. 결정 레벨 40 에서 터진 충돌의 진짜 원인이 레벨 3 이었다면 37개 레벨을 한 번에 날린다.

이론적으로도 근거가 있다. CDCL 이 만드는 학습 절 열은 그대로 분해 반박 증명이고, 재시작을 허용한 CDCL 은 일반 분해 증명계를 다항 시간 안에 흉내 낼 수 있다는 것이 알려져 있다.³ 뒤집으면 분해 증명이 지수 크기일 수밖에 없는 논리식 — 비둘기집 원리가 대표적이다 — 에서는 CDCL 도 지수 시간을 쓴다는 뜻이다. 실제로 비둘기 $n+1$ 마리를 구멍 $n$ 개에 넣는 CNF 는 $n$ 이 스무 개 안팎만 되어도 최신 풀이기가 나가떨어진다 — 사람 눈에는 한 줄이면 자명한 명제인데도 그렇다. CDCL 은 만능이 아니라 “분해로 짧게 증명되는 문제”에 강한 것이다.

4. 살아남게 만든 공학[편집]

CDCL 이라는 아이디어를 실제로 빠르게 만든 것은 2001년 Chaff 이후의 자료구조·휴리스틱 개선들이다. 이 목록이 사실상 현대 풀이기의 정의다.

two-watched literals — 절마다 미배정 리터럴 두 개만 감시한다. 감시하지 않는 리터럴이 거짓이 되어도 절은 단위절이 될 수 없으므로 아무것도 하지 않아도 된다. 그래서 변수 하나를 배정할 때 그 변수가 등장하는 모든 절이 아니라 그 변수를 감시 중인 절만 방문한다. 결정적으로, 백트래킹할 때 감시 포인터를 되돌릴 필요가 없다 — 이 비대칭 덕분에 되돌리기 비용이 사실상 0 이 된다. 실행 시간의 대부분을 차지하는 BCP 의 상수를 통째로 깎아 낸 자료구조라 파급이 컸다.
VSIDS(Variable State Independent Decaying Sum) — 분기 변수 선택 휴리스틱. 충돌 분석에 등장한 변수의 점수를 올리고 주기적으로 전체 점수에 감쇠 계수를 곱한다. 결과적으로 최근에 자주 말썽을 일으킨 변수가 우선 선택된다. “논리식의 구조를 분석해서 좋은 변수를 고른다”는 정공법을 버리고 “최근 충돌 이력을 따라간다”는 값싼 지표로 갈아탄 것이 요점이다. 요즘은 지수 이동 평균 기반 변형(EVSIDS, VMTF, LRB)이 함께 쓰인다.
위상 저장(phase saving) — 변수를 마지막으로 어느 값에 두었는지 기억했다가 다음 결정 때 같은 값을 재사용해, 백점프로 날아간 작업을 다시 하지 않게 한다.
재시작(restart) — 주기적으로 배정을 전부 지우고 처음부터 다시 시작한다. 학습 절과 VSIDS 점수는 남기므로 잃는 것보다 얻는 것이 많다. 나쁜 초기 결정에 갇혀 무한정 헤매는 무거운 꼬리(heavy-tailed) 실행 시간 분포를 깨는 장치이며, 주기는 루비 수열 같은 고정 스케줄이나 학습 절 품질 기반 동적 스케줄로 정한다.
절 데이터베이스 정리 — 학습 절을 다 들고 있으면 메모리도 터지고 BCP 도 느려진다. 그래서 주기적으로 “쓸모없어 보이는” 절을 버리는데, 품질 척도로 널리 쓰이는 것이 LBD(literal block distance, 절 안 리터럴들이 걸쳐 있는 결정 레벨의 개수)다. LBD 가 작은 절일수록 좋은 절이라는 경험칙이 Glucose 계열의 출발점이었다.
전처리·중간처리 — 변수 소거, 포섭(subsumption) 제거, 그리고 2-SAT 문서에 나오는 2-절 함의 그래프의 강한 연결 요소를 이용한 동치 리터럴 병합. 산업 인스턴스에서 변수의 수십 퍼센트가 이 단계에서 사라지는 일이 드물지 않다.

5. NP-완전인데 왜 풀리나[편집]

정직한 답은 “완전히는 모른다”이지만, 합의된 관찰 몇 가지는 있다.

산업 인스턴스는 무작위가 아니다. 회로·프로그램·계획 문제에서 나온 CNF 는 변수들이 국소적으로 뭉쳐 있는 커뮤니티 구조를 갖고, 소수의 변수만 정하면 나머지가 전파로 줄줄이 결정되는 백도어(backdoor) 집합이 작은 경우가 많다. 학습 절이 이 국소 구조를 따라 쌓이면 탐색 공간이 실제로는 지수보다 훨씬 좁게 잘린다.

학습 절이 문제 구조를 재발견한다. 사람이 “이 모듈과 저 모듈은 독립”이라고 알려 주지 않아도, 충돌 분석이 짧고 재사용성 높은 절을 뽑아내면서 사실상 문제의 계층을 복원한다. 반대로 인스턴스에 그런 구조가 없으면 — 랜덤 인스턴스나 조합론적 원리 — 학습이 아무 도움이 안 되고 지수 시간이 그대로 돌아온다.

경쟁이 공학을 밀었다. 연례 SAT Competition 덕에 발표된 개선이 다음 해 모두의 코드에 들어가는 문화가 자리 잡았고, MiniSat 이 2003년에 “핵심 CDCL 은 수백 줄이면 된다”는 것을 보인 뒤로는 진입 장벽까지 낮아졌다.

답이 “없다”일 때도 검증 가능하다. 현대 풀이기는 UNSAT 판정 시 DRAT 형식의 반박 증명을 뱉고 별도의 검사기가 독립적으로 확인한다. 풀이기를 신뢰하지 않고도 결론을 신뢰할 수 있다는 이 성질이 형식 검증 파이프라인에 SAT 을 넣을 수 있게 해 준다.

6. 랜덤 3-SAT 과 상전이[편집]

인스턴스가 어려워지는 지점을 통제된 방식으로 관찰하려면 랜덤 $k$ -SAT을 쓴다. 변수 $n$ 개에서 서로 다른 변수 $k$ 개를 고르고 부호를 동전으로 정한 절을 $m$ 개 독립적으로 뽑는다. 제어 변수는 절/변수 비 $\alpha = m/n$ 하나다.

$\alpha$ 가 작으면 제약이 헐거워 거의 항상 충족 가능하고, 크면 제약이 빡빡해 거의 항상 불가능하다. 그 사이의 전이가 $n \to \infty$ 에서 급격하다는 것이 요점이다. 3-SAT 의 임계값은 수치적으로

\alpha_c \;\approx\; 4.267

로 알려져 있다. 임계값이 존재한다는 것(전이가 $n$ 이 커질수록 날카로워진다는 것)은 프리트굿이 1999년에 증명했지만, 3-SAT 에 대해 그 값이 상수로 수렴한다는 것 자체는 아직 미해결이고, 충분히 큰 $k$ 에 대해서는 2015년에 증명됐다.⁴ 2-SAT 의 $\alpha_c = 1$ 이 깔끔하게 증명된 것과 대비된다.

계산적으로 재미있는 것은 난이도 곡선이다. $\alpha$ 를 0 에서 키우며 풀이 시간을 재면 easy-hard-easy 패턴이 나온다. 낮은 $\alpha$ 에서는 해가 널려 있어 아무렇게나 찍어도 맞고, 높은 $\alpha$ 에서는 모순이 금방 드러나 짧은 반박이 나오며, 정확히 임계점 근처에서 “해가 있긴 한데 극히 드물다”는 최악의 상황이 된다. 통계물리 쪽 언어로 읽으면 임계점 아래에서 해 공간이 여러 개의 멀리 떨어진 덩어리로 쪼개지는 군집화 전이가 먼저 일어나고, 그것이 국소 탐색과 믿음 전파 계열을 방해한다. 스핀글라스의 복제 대칭 깨짐 논의를 그대로 옮겨 온 서베이 전파(survey propagation)가 임계점 근처 대형 랜덤 인스턴스를 푸는 데 한동안 최강이었던 것이 이 대응의 실물 증거다.

단위 전파·순수 리터럴 제거·MOMS 분기를 갖춘 DPLL 로 랜덤 3-SAT 인스턴스를 실제로 풀어, 절 비율 α = m/n 빈마다 만족 가능 비율과 백트랙 수를 쌓는다. n=50 에서 만족 비율이 0.5 를 지나는 지점은 실측 α₅₀ = 4.36 이고(빈당 300표본 × 5시드), n 을 20 → 90 으로 올리면 계단 폭 α(0.9)→α(0.1) 이 1.78 → 0.66 으로 좁아지면서 교차점이 극한값 4.26 쪽으로 내려온다.

주의할 것은 랜덤 인스턴스가 CDCL 의 벤치마크로는 나쁘다는 점이다. 구조가 없으니 학습 절이 재사용되지 않고, 임계점 위 랜덤 $k$ -SAT 에는 분해 증명 크기의 지수 하한이 증명돼 있다. 그래서 SAT 대회도 랜덤 부문과 산업 부문을 아예 분리해서 운영한다. “어려운 인스턴스”와 “실무에서 마주치는 인스턴스”는 거의 겹치지 않는다는, 이 분야에서 가장 자주 반복되는 교훈이다.

7. 어디에 쓰나[편집]

하드웨어 검증과 EDA — 유계 모델 검사(bounded model checking)는 회로의 시간 전개를 $k$ 스텝만큼 펼쳐 ” $k$ 스텝 안에 나쁜 상태에 도달하는가”를 CNF 로 인코딩한다. 합성 전후 회로가 같은 함수인지 보는 조합 등가 검사, 테스트 패턴 자동 생성(ATPG), 논리 합성 최적화도 SAT 을 부른다. 산업용 SAT 풀이기가 세상에서 제일 많이 돌아가는 곳이 사실상 반도체 설계 도구 내부다.
SMT — 정수 산술·배열·비트벡터·부동소수점 같은 이론이 섞인 논리식을 다루는 SMT 풀이기는, 대부분 DPLL(T) 구조를 쓴다. 즉 불 골격은 CDCL 에 맡기고, 이론 솔버가 “이 배정은 이론적으로 모순”이라고 알려 주면 그것을 절로 만들어 되먹인다. 프로그램 검증, 기호 실행, 컴파일러 최적화 검증이 전부 이 위에 서 있다.
계획·스케줄링·구성 — 계획 문제를 유한 지평으로 잘라 SAT 으로 푸는 SATPLAN 계열, 패키지 의존성 해결, 제품 구성기(configurator). “조건이 복잡하고 목적함수는 없거나 단순한” 조합 문제라면 정수계획법보다 SAT/MaxSAT 이 유리한 경우가 많다.
조합론 정리 증명 — 불 피타고라스 삼조 문제(2016)와 슈어 수 5(2017)가 대규모 병렬 SAT 으로 해결됐다. 전자의 증명 파일이 200 TB 라 “사람이 읽을 수 없는 증명”이라는 논쟁까지 낳았다.⁵ 해시·블록 암호의 라운드 축소판을 CNF 로 인코딩해 안전 여유를 재는 암호 해석도 같은 계열의 용법이다.

시뮬레이션 하는 사람 입장에서 SAT 은 대개 직접 쓰는 도구가 아니라 도구 안에 들어 있는 도구다. 회로 시뮬레이터, 검증 도구, 빌드·패키지 시스템, 제약 기반 형상 모델러의 밑바닥에 조용히 깔려 있다가, 어느 날 “제약이 모순됩니다”라는 메시지를 띄우며 존재를 드러낸다.

8. 관련 문서[편집]

Davis, M. & Putnam, H. (1960) 이 분해 기반 원본을, Davis, M., Logemann, G. & Loveland, D. (1962) 가 분기 기반 개정판을 냈다. 흔히 “DPLL”이라 뭉뚱그리지만 두 알고리즘의 자원 프로파일은 정반대다 — DP 는 메모리를, DPLL 은 시간을 태운다. 60년 뒤 CDCL 이 학습 절이라는 형태로 분해를 다시 데려온 것을 보면, 결국 두 논문이 화해한 셈이다. ↩
Marques-Silva, J. P. & Sakallah, K. A. (1996). “GRASP — a new search algorithm for satisfiability”. ICCAD. 같은 시기 Bayardo & Schrag (1997)의 rel_sat 이 독립적으로 유사한 학습을 제안했고, 1UIP 절 학습이 경험적으로 가장 좋다는 체계적 비교는 Zhang, Madigan, Moskewicz & Malik (2001)에서 나왔다. 두 감시 리터럴과 VSIDS 는 같은 팀의 Chaff (2001) 논문이 출처다. ↩
Pipatsrisawat, K. & Darwiche, A. (2011). “On the power of clause-learning SAT solvers as resolution engines”. Artificial Intelligence 175. 반대편 하한은 Haken, A. (1985)의 비둘기집 원리에 대한 분해 지수 하한이다. “우리 풀이기는 뭐든 푼다”고 자랑하는 사람에게 비둘기집 CNF 를 던지는 것이 이 바닥의 유서 깊은 인사법인 이유. ↩
Friedgut, E. (1999)가 날카로운 문턱의 존재를, Ding, J., Sly, A. & Sun, N. (2015)가 충분히 큰 $k$ 에 대해 임계값의 정확한 위치를 확립했다. 즉 인류는 3-SAT 의 임계값을 소수점 아래 여러 자리까지 수치적으로 알면서도 그것이 수렴한다는 것조차 증명하지 못한 상태다. 수치가 이론을 한참 앞서가는, 이 바닥에서 그리 낯설지 않은 풍경. ↩
Heule, M. J. H., Kullmann, O. & Marek, V. W. (2016)의 불 피타고라스 삼조 문제. 결론은 “1부터 7824까지는 2색으로 칠할 수 있고 7825부터는 불가능”이며, 증명은 대칭성 축약 후에도 200 TB 였다. 압축본이 68 GB 라 “누구든 검사기를 돌려 확인은 할 수 있지만 아무도 이해할 수는 없는 증명”이라는 표현이 붙었다. 수학의 4색 정리 논쟁이 컴퓨터 성능 세 자릿수 배 스케일로 재연된 사건. ↩