개발일지

개념 충족 가능성 문제 중 하나로써 아래와 같은 형태를 2-SAT 문제라 한다. * 충족 가능성 문제 : Boolean으로 이루어진 식이 있을 때 해당 식이 True인 경우를 찾는 문제 f=(¬x1∨x2)∧(¬x2∨x3)∧(x1∨x3)∧(x3∨x2) 인 경우에 f를 true로 만드는 경우 ¬ : NOT ∨ : OR ∧ : AND 괄호 안의 OR 연산으로 이루어진 것을 절(Clause)이라고 표현하고 AND와 절로 이루어진 식을 CNF(Conjunctive Normal Form)라고 한다. 각 절의 변수의 개수가 2개면 2-SAT이라 하고 N개면 N-SAT이라고 한다. 2개 같은 경우 SCC 알고리즘을 사용하여 쉽게 해결할 수 있지만, 3개 이상의 SAT 문제에서는 NP-Hard 문제이다. 작동원리 1. ..