조지 불(George Boole)은 언어로 적은 부류 관계를 방정식으로 바꾸고, 전개와 소거를 거쳐 허용되는 경우를 찾으려 했습니다. 1848년 논문은 모든 변숫값에 따른 구성항을 전개하고, 방정식에 맞지 않는 항을 0으로 두는 규칙을 제시합니다. 이번에는 같은 생각이 후대의 명제 충족 가능성 문제, 곧 SAT에서 어떻게 탐색 절차로 발전했는지 네 변수 표로 확인합니다.
01 · 불이 풀려던 문제
여러 조건을 동시에 만족하는 경우가 하나라도 있을까요?
가상의 행사 배정에서 x와 y는 두 발표 선택, z와 w는 두 장비 사용 여부라고 합시다. “x 또는 y를 선택한다”, “x를 선택하면 z를 쓴다”, “y를 선택하면 w를 쓴다”, “z와 w를 함께 쓰지 않는다”를 모두 지켜야 합니다. 네 값에는 16개 조합이 있습니다. 조건을 식으로 바꾸면 각 행이 가능한 해인지 기계적으로 검사할 수 있습니다.
불 논리의 계산은 조건을 만족하는 부류와 만족하지 않는 부류를 분리하는 토대를 마련했습니다. 현대 SAT는 주어진 명제식을 참으로 만드는 0·1 배정이 존재하는지 묻습니다. 불이 오늘의 SAT 알고리즘을 제안한 것은 아니며, 불의 기호화·전개 방법이 후대의 자동 추론 문제와 이어지는 역사적 위치를 갖습니다.
불은 추론 문제를 기호 방정식과 가능한 구성항의 계산으로 옮겼습니다. 아래 활동은 그 목표를 현대의 절과 0·1 탐색으로 다시 표현합니다. 1962년 Davis·Logemann·Loveland의 탐색 절차와 1971년 Cook의 복잡도 연구는 후대의 발전입니다.
02 · 불의 방법에서 현대 SAT로
조건을 절로 적고, 거짓이 확정된 가지를 멈춥니다
네 조건은 (x∨y) ∧ (¬x∨z) ∧ (¬y∨w) ∧ (¬z∨¬w)로 적을 수 있습니다. 괄호 하나를 절이라고 부르며, 모든 절이 1인 배정이 해입니다. 전체 검사는 0000부터 1111까지 16행을 모두 계산합니다.
가지치기 탐색은 값을 하나씩 정합니다. 예를 들어 x=0, y=0을 정한 순간 첫 절 x∨y가 0으로 확정됩니다. z와 w를 더 정해도 이 절은 되살아나지 않으므로 그 아래 네 행을 만들 필요가 없습니다. 이 활동에서는 선택한 변수 순서대로 가지를 펼치고, 부분 배정만으로 어떤 절이 0이 되면 그 가지를 멈춥니다.
03 · 불의 계산 목표를 현대 탐색으로 확인하기
조건과 고정값을 바꾸며 해와 탐색량을 비교하세요
| 입력 | C₁ | C₂ | C₃ | C₄ | 결과 |
|---|
‘조건 없음’에서는 16행이 모두 해입니다. ‘한 해’는 네 값을 고정하여 해 하나를 남기고, ‘빈 결과’는 고정값과 C₄가 충돌하게 만듭니다. 변수 순서를 바꾸면 해 집합은 그대로이며 방문한 부분 배정 수는 달라질 수 있습니다.
04 · 표에서 얻은 발견
충족 가능성과 탐색 효율은 서로 다른 질문입니다
해가 하나라도 있으면 식은 충족 가능합니다. 해가 몇 개인지, 첫 해를 얼마나 빨리 찾는지, 모든 해를 나열하는지는 별도의 과제입니다. 표의 해 목록은 16개 완전 배정을 모두 비교한 결과이고, ‘가지치기 방문’은 조건 위반이 확정된 부분 가지를 더 펼치지 않은 탐색량입니다.
변수 순서는 식의 뜻을 바꾸지 않습니다. 다만 어떤 조건을 일찍 판정할 수 있는지가 달라져 탐색량이 변합니다. 단서가 많은 변수를 먼저 정하면 큰 가지를 일찍 줄이는 경우가 있지만, 언제나 같은 순서가 최선이라고 말할 수는 없습니다.
“해가 있다”는 통과 행을 제시하고, “탐색이 줄었다”는 방문한 부분 배정 수를 비교해 설명합니다. 행 수와 확률을 섞지 않습니다.
05 · 오늘의 실제 적용
시간표·설정·검증 문제를 0·1 조건으로 바꿉니다
시간표에서 같은 교사가 두 수업에 동시에 배정되지 않게 하거나, 소프트웨어 설정에서 함께 켤 수 없는 기능을 막거나, 회로 입력 가운데 오류 조건을 만드는 배정이 있는지 찾을 때 SAT 모형을 쓸 수 있습니다. 각 선택을 0·1 변수로 두고 필수·선택·충돌 규칙을 절로 바꿉니다.
현대 SAT 해결기는 단순한 전수검사보다 훨씬 많은 기술을 사용합니다. DPLL의 분기와 단위 절 전파, 후대의 절 학습과 휴리스틱이 대표적입니다. 이 회차의 가지치기는 핵심 원리를 작게 보여 주는 교육용 모형이며 실제 해결기의 성능을 대신 측정하지 않습니다.
① 선택 항목을 0·1 변수로 정합니다. ② 자연어 규칙을 절로 옮깁니다. ③ 해가 있으면 실제 배정을 확인합니다. ④ 해가 없으면 충돌하는 조건을 추적합니다. ⑤ 탐색 순서와 성능은 문제 구조에 맞게 따로 평가합니다.
06 · 바르게 쓰는 기준
불의 원전과 SAT 연구의 시대를 구별합니다
불의 1848년 전개 정리는 변수의 0·1 경우에 대응하는 구성항으로 함수를 펼치는 방법을 제시했습니다. SAT라는 문제 이름, CNF 절 표기, DPLL 알고리즘, NP-완전성 이론은 20세기의 발전입니다. 이 연결은 공통된 계산 목표를 보여 주며 직접적인 동일시를 뜻하지 않습니다.
화면의 0은 조건이 거짓이거나 선택되지 않은 것으로 확인된 값입니다. 미확인 입력은 가지치기 과정의 부분 배정으로 다루며 최종 표의 0과 구별합니다. 가상 배정 결과를 실제 행사 운영 자료로 해석하지 않습니다.
불의 문제: 언어의 조건을 기호식으로 바꾸어 가능한 경우를 계산하기. 후대의 제안: SAT 식의 해를 찾고 거짓이 확정된 가지를 줄이기. 오늘의 쓰임: 시간표·설정·회로 검증의 충돌 여부와 가능한 배정을 확인하기.
07 · 자료와 출처
불의 원전과 SAT 원논문
- 조지 불, “The Calculus of Logic”(1848) — 선택 함수의 전개와 방정식 해석 규칙.
- 조지 불, 『An Investigation of the Laws of Thought』(1854) — 논리와 확률 계산의 원전.
- Davis, Logemann, Loveland, “A Machine Program for Theorem-Proving”(1962) — 분기 탐색 절차의 원논문.
- Stephen A. Cook, “The Complexity of Theorem-Proving Procedures”(1971) — 명제식 판정과 계산 복잡도 연구.
- Carnegie Mellon University, SAT & SMT 강의 — DPLL과 현대 SAT 탐색의 교육 자료.
- 조지 불 초상 판화 · Wikimedia Commons — 1865년 1월 21일 게재, 공개 영역.