CNF-satisfiability
- 괄호 안에서는 or만 사용 밖에서는 and 연산자로만 연결 되어있다
- 이러한 형식을 conjunctive normal form(CNF)
- 괄호로 묶인 부분을 절(clause)라고 한다
EX) satisfiable한가?
x1,x2의 경우를 넣어본다 1,1일 떄 해당하므로 satisfiable하다
당파 판단 문제가 NP-complete임을 증명
- 같은 절, 긍정과 부정은 연결하지 않는다.
- 절만큼의 당파가 있으면 yes이다