불리언 충족 가능성 문제 (Boolean satisfiability problem)
쉽게 풀면
참과 거짓만 가지는 변수들로 이루어진 긴 논리식이 있을 때, 변수에 어떤 값을 넣어도 식 전체가 참이 될 수 없는지 아니면 참이 되게 하는 방법이 있는지를 묻는 문제입니다. 변수가 n개면 경우의 수가 2의 n제곱이라 전부 시험하기는 불가능하므로, 똑똑하게 가지를 쳐 나가는 알고리즘이 필요합니다.
왜 중요한가
NP-완전이라는 개념이 처음 증명된 문제로, 계산 복잡도 이론의 출발점이자 기준점입니다. 동시에 현대 SAT 해결기는 수백만 개의 변수를 가진 실제 문제를 자주 풀어내기 때문에, 하드웨어 검증·소프트웨어 모델 체킹·일정 수립 등에서 범용 엔진으로 쓰입니다. 이론적 어려움과 실용적 성공이 공존하는 대표 사례입니다.
논문에서는 이렇게 쓰입니다
검증 문제를 논리식 만족 문제로 바꿔 전용 해결기로 풀었다는 뜻입니다.
조금 더 깊게 보면
입력은 보통 절들의 논리곱인 논리곱 표준형으로 주어지며, 절마다 변수가 3개인 3-SAT도 여전히 NP-완전입니다. 실용 해결기의 뼈대는 단위 전파와 순수 리터럴 제거를 갖춘 DPLL이며, 여기에 모순이 발생한 원인을 새 절로 학습해 같은 실수를 반복하지 않게 하는 절 학습과 비시간순 백점프를 더한 CDCL이 현재의 표준입니다. 정수 산술이나 배열 같은 이론을 함께 다루는 SMT 해결기로 확장되어 형식 검증에 널리 쓰입니다.
주의할 점
쿡-레빈 정리가 이 문제의 NP-완전성을 증명한 정리이므로, 문제 자체와 정리를 혼동하지 않아야 합니다. 최악의 경우가 지수 시간이라는 이론적 사실과 실제 문제들이 대개 빨리 풀린다는 경험적 사실은 모순이 아니라 문제 구조의 차이에서 비롯됩니다.