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가 참일 경우가 전제가 되어야 ..