[알고리즘] SAT(Satisfiability Problem)

 

N개의 불리언 값 변수로 구성된 논리식을 참으로 만드는 변수 값들의 조합을 찾는 문제이다.

 

들어가기 앞서

P문제 : 문제의 해답을 다항 시간 내에 도출할 수 있는 문제의 집합
NP문제 : 답이 주어졌을 때 이것이 정답인지를 다항 시간 내에 확인할 수 있는 문제의 집합
NP-hard : 다항 시간내에 해답을 구할 수 없는 문제 (대표적으로 P=NP 문제)
NP-complete : NP-hard 이면서 NP인 문제

 

 

SAT-2

두 논리변수의 논리곱 및 논리합 연산식을 주어질 때, 식을 참으로 만드는 조합을 찾거나, 그런 조합이 없음을 찾는 것이 목표이다.

 

SAT-2 문제에서 제시되는 식을 함의 그래프(implication graph)로 나타낼 수 있다. 

 

 

각 논리변수(a, ~b, ~a 등등)는 그래프의 노드에 대응되며, 간선은 변수 간의 관계를 표현한다.

 

(a V b)에 대해 (~a → b)와 (~b → a) 두 간선을 만든다. 이는 'a가 참이 아닐 경우 b가 참이어야 한다'와 'b가 참이 아닐 경우 a가 참이어야 한다'를 의미한다.

 

 

 

위 식을 함의 그래프로 표현하면 다음과 같다.

 

 

수식이 참이 되도록 모든 변수에 값을 할당하는 게 가능한지 여부는 함의 그래프의 구조에 따라 결정된다. 

 

 

 

가능한 경우는 A와 ~A가 같은 강결합 컴포넌트에 속하는 일이 없을 때와 동치이다.

예시의 그래프는 위와 같이 SCC를 형성한다. 어떠한 SCC도 변수와 변수의 역이 같은 컴포넌트에 속하지 않는 것을 볼 수 있다. 

 

 

 

해가 존재하는 경우, 변수의 값은 컴포넌트 그래프의 모든 노드를 위상 정렬 역순으로 방문하면서 찾을 수 있다.

해를 찾기 위해 컴포넌트 D를 처리하면, c값은 거짓이다. 다음으로 컴포넌트 C를 처리하면 a는 거짓, b도 거짓이다. 모든 변수에 값이 할당되었으므로 나머지 컴포넌트는 확인하지 않는다. 

 

 

이 방법이 성립하는 이유는 함의 그래프가 특별한 구조이기 때문이다.

x→y 경로와 x→~x 경로 가 있다면 x는 참이 될 수 없다. 그 이유는 ~y→~x 경로가 있어서 x,y 모두 거짓이 되기 때문이다.

 

 

 

 

+)

https://cp-algorithms.com/graph/2SAT.html#algorithm

SAT-3은 NP-hard 문제이다.