충족 가능성 문제

충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다.

기본 정의

논리식은 기본적으로 진리값을 취하는 논리 변수 $x_{1},x_{2}\cdots$와 몇몇 논리 연산자 결합에 의해 만들어지는 유한한 길이의 식을 가리킨다. 여기에서 사용되는 연산자는 다음과 같다.

• 논리 부정, $({\overline {x_{1}}})$: $x_{1}$ 이 참이면 거짓, 거짓이면 참
• 논리합, $(x_{1}\lor x_{2})$: $x_{1}$이나 $x_{2}$ 중 적어도 하나가 참이면 참, 나머지 경우는 거짓
• 논리곱, $(x_{1}\land x_{2})$: $x_{1}$과 $x_{2}$가 모두 참이면 참, 나머지 경우는 거짓

또한, 논리식에서 각각의 $x_{i}$, ${\overline {x_{i}}}$ 식을 리터럴(literal)이라고 부른다. 여러 리터럴의 논리합, 즉 $x_{1}\lor x_{2}\lor \cdots \lor x_{i}$ 꼴로 이루어진 식을 클로저(clause), 절이라고 정의한다. 클로저들의 논리곱으로 표현되어 있는 논리식을 논리곱 표준형(CNF)이라고 부른다.

계산 복잡도

충족 가능성 문제의 결정 문제는 NP-완전에 속한다. 이것은 스티븐 쿡이 증명했으며(쿡-레빈 정리), 이 문제는 NP-완전이라는 것이 증명된 최초의 문제이기도 하다. 또한, 논리식이 논리곱 표준형으로 이루어진 경우에도 역시 NP-완전에 속한다.

k-충족 가능성 문제, k-SAT는 각 클로저에 들어있는 리터럴의 개수가 k개 이하로 구성된 CNF 논리식만 입력으로 받는 문제이다. 예를 들어 3-SAT는 한 절에 들어가는 리터럴 개수를 3개 이하로 제한하는 문제이다. 3-SAT도 마찬가지로 NP-완전 문제이다. 리터럴 개수를 정확히 3개로만 제한하는 문제는 EXACT 3-SAT이라고 하며, 모든 SAT 문제는 다항 시간에 3-SAT 또는 EXACT 3-SAT로 환산(Reduction)될 수 있다.

반면, 2-SAT, CNF에서 한 절에 들어가는 리터럴 개수가 2개 이하인 문제는 P에 속한다. 즉, 다항 시간에 풀 수 있다.

같이 보기

• 불 대수