k-SAT은 NP-hard지만 2-SAT만큼은 다항시간 내에 풀 수 있다.
참고로 k-SAT은 3-SAT으로 대체할 수 있다고 증명됨.

CNF 식 : (x0∨~x1)∧(~x2∨x3)와 같이 and로 묶여있는 식

절(clause) (x0 ∨ x1)이 true가 되려면..
~x0 일때 x1 이어야함 (~x0->x1)
~x1 일때 x0 이어야함 (~x1->x0)

그래프를 구성하고 ~x->x 로 순환이 될 경우 모순

명제를 추가하여 그래프를 구성.
ex) 7535번 문제 경우, XOR관계이므로 서로 같은 값이 될 수 없게 명제를 추가함.

특정 x가 true로 설정하고 싶으면,
(x ∨ x) 라는 절을 추가하여 true가 아니면 CNF가 성립 안되게 하면됨.
ex) 3648번 문제는 1번이 항상 true여야 하므로 (1 ∨ 1) 추가하여 풀수 있다.

sccId랑 dfs_low랑은 다르다!?
같은 그룹 체크할때 dfs_low했을때 틀렸음..

CNF 절이 아닐 경우는 식을 유도해야됨. (1739문제)
(y1 && x2) || (x1 && y2)
(y1 || x1) && (y1 || y2) (x2 || x1) (x2 || y2)
~x -> y 식으로 풀어야함

결과를 출력할때,
DAG 순서로 정점 보면서 정점상태에 반대로 대입(true정점이면 false로 세팅)
~a가 먼저 나왔으면 a가 참,
a가 먼저 나왔으면 ~a가 참(a=false)