2-SAT은 불리언 변수 x1,x2,…,xN이 있을 때 2-CNF 식을 true로 만드는 값을 각 xi에 정하는 문제다.
2-CNF 식은 (x∨y)∧(¬y∨z)∧(x∨¬z)∧(z∨y) 같은 형태다. 괄호로 묶은 부분을 절(clause)이라 하고, 절은 변수 두 개를 ∨로 이은 것이다. ∨는 OR, ∧는 AND, ¬은 NOT을 뜻한다.
변수의 개수 N과 절의 개수 M, 그리고 식 f가 주어진다. 식 f를 true로 만들 수 있는지 판정하는 프로그램을 작성하시오.
예를 들어 N=3, M=4, f=(¬x1∨x2)∧(¬x2∨x3)∧(x1∨x3)∧(x3∨x2)이면 x1을 false, x2를 false, x3을 true로 정해서 f를 true로 만들 수 있다. 반면 N=1, M=2, f=(x1∨x1)∧(¬x1∨¬x1)이면 x1에 어떤 값을 넣어도 f는 true가 되지 않는다.
첫째 줄에 변수의 개수 N (1≤N≤10000)과 절의 개수 M (1≤M≤100000)이 주어진다. 둘째 줄부터 M개의 줄에 절이 한 개씩 주어진다. 절은 두 정수 i와 j (1≤∣i∣,∣j∣≤N)로 이루어진다. i가 양수면 xi를, 음수면 ¬x−i를 뜻하고, j도 같은 방식으로 읽는다.
첫째 줄에 식 f를 true로 만들 수 있으면 1을, 없으면 0을 출력한다.