충족 가능성 문제

위키백과 ― 우리 모두의 백과사전.

충족 가능성 문제(充足可能性問題, satisfiability problem, 줄여서 SAT)는 곱셈 표준형 (CNF)으로 표현된 논리식이 주어졌을 때, 이 식에 포함되는 모든 변수의 값을 참, 거짓으로 정하여 이 식을 참이 되게 수 있는지 여부를 묻는 문제이다. 한국어로는 만족성 문제, 만족도 문제, 만족 문제라고도 한다. 이 문제는 스티븐 쿡이 최초로 NP-완전성을 증명한 문제로 유명하고 수많은 학자들이 이 문제에 관심을 가지고 있다. 이 문제는 불린 충족 가능성 문제(boolean satisfiability problem)라고도 한다.

[편집] 기본 정의

진리값을 취하는 논리 변수 $x_1, x_2 \dots$ 및 논리 연산자에 의해 논리식이 이루어진다.

논리 부정 $(\bar{x_1}) \dots x_1$ 이 참이면 거짓, 거짓이면 참
논리합 $(x_1 \lor x_2) \dots x_1$ 이 참이면 $x_1\,$ 거짓이면 $x_2\,$
논리곱 $(x_1 \land x_2) \dots x_1$ 이 참이면 $x_2\,$ 거짓이면 $x_1\,$

리터럴 -- 논리 변수 $(x_1)\,$ 또는 그 부정 $(\bar{x_1})$
클로저 -- 리터럴의 논리합 $(x_1 \lor \bar{x_2} \lor ...)$

[편집] 변형

[편집] 3-충족 가능성

3-충족 가능성 문제는 3-SAT이라고도 하며, 논리식을 CNF로 나타낼 때 한 절에 들어가는 리터럴 개수를 3개 이하로 제한하는 문제이다. 이 문제 역시 NP-완전 문제이다. 리터럴 개수를 정확히 3개로만 제한하는 문제는 EXACT 3-SAT이라고 하며, 모든 SAT 문제는 다항 시간에 3-SAT 또는 EXACT 3-SAT로 환산될 수 있다.