SCC, SAT.(boolean satisfiability problem)

설명 잘된 블로그 : http://blog.qwaz.io/problem-solving/scc%EC%99%80-2-sat (설명보면 힐링..)

위의 블로그에서 가져와서 정리해왔습니다.

SCC.

scc는 strongly connected component로 강한 연결 요소를 뜻한다.

강한 연결 요소는 다음 조건을 만족한다.

1. 같은 scc안의 임의의 두 정점은 서로 도달 가능하다.

2. 어떤 정점이나 간선도 1의 조건을 만족하면서 scc에 추가될 수 없다.

임의의 방향 그래프가 주어졌을때 scc를 찾는 알고리즘으로 코사라주의 알고리즘과 타잔의 알고리즘이

있다고 한다. 둘 모두 시간복잡도는 O(V+E)라고 하지만 쉬운 코사라주의 알고리즘만 가져옴.

1. 방향 그래프 G, 빈 스택 S, G의 간선 방향을 뒤집은 역방향 그래프 G’를 준비합니다.

2. G에서 아직 방문되지 않은 정점들에 대해 DFS를 시행하고, 각 정점의 탐색이 끝나는 순서대로 S에 넣습니다.(위상정렬) 스택에 모든 정점이 들어갈 때까지 반복합니다.

3. S가 빌 때까지 다음을 반복합니다.

4. S의 가장 위쪽에 있는 정점 v를 뽑습니다. v가 G’에서 이미 방문된 정점이라면 정점을 다시 뽑습니다.

6. G’에서 v에서 DFS를 시행해 이번 시도에 처음 방문한 정점들을 v와 같은 SCC로 묶습니다.

2-SAT.

sat문제는 논리 변수와 논리식이 주어질때 식을 참으로 만드는 논리 변수의 조합이 존재하는지 찾는 

문제다. 2-sat는 sat문제들중 특수한 형태로, 하나의 논리식(아래의 괄호안) 안에서 변수가 두개만 

쓰일때 2-sat라고 부른다고 한다. 예로 아래의 식이 있다고 하자.

(!x1 || x3) && (!x2 || !x3) && (x1 || x2) && (!x1 || x4) && (x2 || !x4)

(!는 not, ||는 or ,&&는 and.  c언어 연산자라고 보면된다.)

이러한 식의 값을 참으로 하는 변수의 조합이 있는지 찾는게 목표다.

답을 찾기 위해 식을 그래프로 바꿔야 한다. 그래프로 바꾸는 방법.

1. 각각의 변수 x에 대해 x와 !x를 만든다.

2. a||b에 대해 !a->b간선과 !b->a간선을 만든다.

위의 식은 x1->x3, !x3->!x1, x2->!x3, x3->!x2.... 등으로 만들어지는데 이걸 표현하면

아래 그림처럼 된다고 한다. (위의 블로그에서 그림 그대로 가져왔습니다.)

이렇게 그래프를 그리면 ||관계에 있는 것들을 이었기 때문에 a가 참일경우 a->b로 가는 간선도 

참이라는걸 뜻하게 된다. 따라서 같은 컴포넌트(위의 파란색 원)에 있는 것들중 하나가 참이면

그 컴포넌트 전체가 참이라는 뜻도 된다. (하나가 거짓이면 모두 거짓이라는 뜻도 된다.)

x와 !x는 세가지중 한가지 관계를 가진다고 한다.

1. x와 !x가 같은 컴포넌트에 있는 경우. -> 답이 존재하지 않음.

2. x에서 !x로 가는 경로만 있는 경우 -> 뒤쪽에 있는것만이 참.

3. x와 !x의 경로가 존재하지 않는 경우 -> 둘중 하나가 참임.

이것을 더 확장해서 x와 !x뿐만이 아니라 a와 b의 관계로도 확장시킬수 있습니다.

이 성질들을 이용해 변수의 값을 다음과 같이 찾을 수 있습니다.

1. 그래프를 만듬

2. 그래프에서 scc알고리즘을 적용해서 scc번호를 매김.

3. x와 !x의 scc번호가 같으면 답이 존재하지 않음(위의 1번경우)

4. 번호가 다르면 x의 scc번호가 !x보다 작은 경우에 x가 참.