2-SAT (2-Satisfiability)

2-SAT은 충족가능성 문제로, 위의 식과 같이 OR 연산으로 두 변수가 묶인 절들이 각각 AND 연산으로 연결되어 있는 형태에 대해 f가 참인 경우를 만들기 위해 각각의 변수를 참과 거짓 중 무엇으로 설정해야 하는지 계산해야 합니다. 

위와 같이 AND 연산으로만 표현된 식의 형태를 CNF (Closure Normal Form)이라고 합니다. 

두 불린 변수 p와 q가 있을 때, p→q는 “p가 참이면 q도 참이다”라는 명제를 의미합니다. 

다음의 표는 두 불린 변수의 각 경우에는 p→q의 진리값을 나타냅니다. 만약 p가 참일 때 q가 거짓이라면 이 명제는 거짓인 명제가 됩니다. 그리고, p가 거짓이라면 q와 상관없이 이 명제는 항상 참이되는데요, 그 이유는 이 명제는 항상 p가 참일 경우가 전제가 되어야 하기 때문입니다. p가 거짓인 순간부터 q가 참이든 거짓이든 상관이 없어지는 것입니다.

예를 들어 설명하면 다음과 같습니다. 시간이 되었다면 밖에 나가야 하지만, 시간이 되지 않았더라도 밖에 나갈 수 있고 나가지 않을 수도 있습니다. 그래도 이 명제는 훼손되지 않습니다. 시간이 되었을 때 밖에만 나가면 되는 것 입니다.

두 불린 변수 p와 q에 대해, 다음과 같이 p ∨ q 인 조건이 참이 되기 위해서는 p만 참이거나, q만 참이거나 p와 q가 모두 참인 경우여야 합니다. 이 경우를 포함하는 명제를 다음과 같이 만들 수 있습니다. 첫 번째 명제인 ￢p → q을 참으로 만들기 위해서는 p가 거짓이면서 q가 참이여야 합니다. 그러나, 위에서 설명한 바와 같이 전제가 거짓이라면 결론은 참이든 거짓이든 상관없게 됩니다. 즉, p가 참인 상태에서는 q가 참이여도 되고 거짓이여도 됩니다. 

두 번째 명제인 ￢q → p도 마찬가지로, q가 거짓이라면 p는 참이여야 합니다.  그러나, q가 참인 상황에서는 p는 참이여도 되고 거짓이여도 됩니다.

앞서 소개한 f에 포함된 절들의 각 OR 조건들을 명제로 나열하면 다음과 같습니다.

이제, 이 명제들에 존재하는 변수들을 각각 정점으로 하고 각각의 명제들을 간선으로 하는 유향그래프를 만들 수 있습니다. 

이들을 유향그래프로 나타내면 다음과 같습니다.

이전에 설명드린 강한 연결 요소 (SCC)는 그래프에서 한 정점에서 출발하여 자기자신으로 돌아오는 사이클 중에서 가장 많은 정점을 포함하는 사이클을 의미합니다. 

SCC 설명 : https://blog.naver.com/remocon33/221289243302

위의 그래프 같이 각 정점이 불린 변수 x와 ￢x 쌍들로 구성되어 있을 때, 만약 사이클 내에 x와 ￢x가 공존한다면 (x→￢x→x)가 발생하게 되고, 이는 참에서 거짓으로 가는 명제로 인해 모순이 됩니다. 

따라서, 우리는 나타낸 그래프의 각 SCC를 검사하여 하나의 SCC 안에 같은 불린 변수 쌍이 공존하는지 검사함으로써 해당 f 식이 참인지 거짓인지 판별할 수 있습니다. 

만약 SCC내에 같은 불린 변수 쌍이 하나라도 공존한다면 f는 거짓이 되며, 하나도 없으면 f는 참이 됩니다. 

앞서 나타낸 예시의 그래프에서 SCC를 생성하면 다음과 같이 나타낼 수 있습니다. 

이 그래프는 사이클이 존재하지 않기 때문에 각각의 변수가 SCC가 되며, 이 SCC 안에 같은 불린 변수 쌍이 존재하지 않으므로 식 f는 참이 된다고 할 수 있습니다.

요약하자면, 2-SAT 문제를 해결하기 위해, 각 절을 명제로 나타내고 명제들을 다시 유향그래프로 표현한 다음, 유향그래프의 SCC를 구하여 각 SCC 안에 같은 불린 변수 쌍이 존재하는지 검사하여 하나라도 존재하면 거짓, 하나도 없으면 참인 식이라고 할 수 있습니다.

관련 문제

https://algospot.com/judge/problem/read/MEETINGROOM