Satisfiability Problem 문서 원본 보기

[[분류:알고리즘 설계와 분석]]
[[분류:컴퓨터 공학]]
상위 문서: [[NP-Completeness#Satisfiability Problem|NP-Completeness]] 

==개요==
SAT(Satisfiability Problem)는 컴퓨터 과학 이론에서 가장 유명한 NP-complete 문제이며, 전 세계의 알고리즘 전문가들이 빠른 알고리즘(다항시간)을 찾으려 했지만 실패했다. SAT를 빠르게 풀 수 있으면 P = NP가 되어버리며, NP 문제들이 전부 빠르게 풀려 암호 시스템 대부분이 붕괴한다. 

==Definition of SAT==
SAT는 아래와 같은 문제 정의를 가진다: 
 입력: 변수들의 집합 <math>V</math> 
     변수들로 이루어진 절(clause)<ref>여러 개의 리터럴(literal)들을 OR로 묶은 하나의 조건식이다. 예를 들면, <math>(v_1 \lor \bar{v_2} \lor v_3)</math>이 있다.</ref><ref>리터럴(literal)이란, 변수 <math>v</math>또는 그 부정 <math>\bar{ V}</math>을 의미한다.</ref>들의 집합 <math>C</math>
 질문: 변수들에 true/false 값을 적절히 넣어 모든 절(clause)이 동시에 참이 되도록 하는 방법이 존재하는가? 
아래는 SAT 문제에 대한 예시 인스턴스이다: 
 입력: <math>V=\{v_1, v_2\}</math>
     <math>C=\{\{v_1,\bar{v_2}\},\{\bar{v_1},v_2\}\}</math>
위와 같은 인스턴스에 대한 답은 모든 절을 참으로 만들 수 있다는 것이다. <math>v_1=v_2=true</math>로 놓으면 두 절이 모두 만족되기 때문이다. 반면, 아래와 같은 인스턴스는 만족 불가능하다: 
 입력: <math>V=\{v_1, v_2\}</math>
     <math>C=\{\{v_1,v_2\},\{v_1,\bar{v_2}\},\{\bar{v_1}\}\}</math>	

==3-Satisfiability Problem==	
3-SAT(3-Satisfiability)은 SAT 문제의 특수한 버전으로, 각 절(clause)에 정확히 3개의 literal이 들어간 형식이다. 이는 SAT의 특수한 버전이기 때문에(<math>3-SAT \subseteq SAT</math>), 만약 reduction에 따라 3-SAT이 NP-complete이면 SAT도 NP-complete이다. 

===SAT to 3-SAT Reduction===
SAT의 절의 길이는 <math>k=1,2,3,4,..</math>으로 일반적인 길이를 가지기 때문에, 어떤 인스턴스의 각 절 <math>C_i</math>를 독립적으로 길이가 3인 절로 바꾸어 전체 식을 3-SAT 인스턴스로 변환하여 reduction을 수행할 수 있다. 

먼저 <math>C_i=\{z_1\}</math>과 같이 <math>k=1</math>인 경우, 리터럴이 3개인 절로 만들기 위해서 새로운 변수 <math>v_1, v_2</math> 2개를 만들어야 한다. 이 경우 아래와 같이 네 개의 절이 생성된다:
 <math>\{v_1,v_2,z_1\}</math>
 <math>\{v_1,\bar{v_2},z_1\}</math>
 <math>\{\bar{v_1},v_2,z_1\}</math>
 <math>\{\bar{v_1},\bar{v_2},z_1\}</math>
위 네 절이 동시에 만족되기 위해서는 무조건 <math>z_1=true</math>여야 하므로 원래의 의미가 보존된다.

그리고 <math>C_i=\{z_1,z_2\}</math>과 같이 <math>k=2</math>인 경우, 리터럴이 3개인 절로 만들기 위해서 새로운 변수 <math>v_1</math>을 만들어야 한다. 이 경우 아래와 같이 두 개의 절이 생성된다:
 <math>\{v_1,z_1,z_2\}</math>
 <math>\{\bar{v_1},z_1,z_2\}</math>
위 두 절이 모두 만족되기 위해서는 <math>z_1</math> 또는 <math>z_2</math> 중 하나가 true여야 하므로 원래 절의 의미가 유지된다.

마지막으로 <math>C_i=\{z_1,z_2,z_3,...,z_n\}</math>과 같이 <math>k=n>3</math>인 경우, 리터럴이 3개인 절로 만들기 위해서는 새로운 변수들 <math>v_1, v_2,\cdots,v_{n-3}</math>를 만들고 아래와 같이 사슬형(chain) 절들을 만들어야 한다. 
 <math>\{z_1,z_2,v_1\}</math>
 <math>\{\bar{v_1}, z_3,v_2\}</math>
 <math>\{\bar{v_2}, z_4, v_3\}</math>
 ...
 <math>\{\bar{v_{n-3}},z_{n-1}, z_n\}</math>
위 절들은 각 절이 3개의 리터럴을 포함하도록 분해한 구조이다. 이를 통해서 원래의 절의 의미들을 보존할 수 있다. 또한 이를 통해서 <math>k</math>가 자연수일 때 모든 절들을 길이가 3인 절로 변환할 수 있다는 것이 증명되었다. 따라서 SAT <math>\le</math> p 3-SAT이며, SAT는 NP-complete 이므로 3-SAT도 NP-complete이다. 

이때, 절이 4개, 5개 … literal로 구성되어 있어도 조금 조정하면 동일한 방식으로 3-SAT으로 변환할 수 있기 때문에 4-SAT, 5-SAT, … 도 모두 NP-complete이다. 하지만 사실, 2-SAT 자체는 NP-complete이 아니며, 다항시간 내에 해결된다. 

또한 어떤 문제에 대해 NP-complete 증명을 할 때 일반 SAT 대신 3-SAT를 기준 문제로 사용할 수 있다. 이때 3-SAT를 기준으로 사용하는 이유는 모든 절의 길이가 3으로 균일하여 구조가 더욱 규칙적이기 때문이다. 이때 reduction의 방향성은 아래와 같다:
 SAT <math>\le</math> 3-SAT <math>\le</math> X
즉, SAT 문제를 3-SAT로 바꿀 수 있으므로, 3-SAT를 증명하고자 하는 X라는 새로운 문제로 reduction하여야 X가 NP-complete임을 증명할 수 있다. 예를 들면, [[Vertex Cover]] 혹은 [[Independent Set]] 문제는 3-SAT을 이용하여 NP-complete임을 증명할 수 있다.

==각주==