2-SAT 만족 가능성

2-SAT은 불리언 변수 $x_1, x_2, \ldots, x_N$이 있을 때, 2-CNF 식을 true로 만드는 값 배정이 있는지 판정하는 문제이다.

2-CNF 식은 $(x \lor y) \land (\lnot y \lor z) \land (x \lor \lnot z) \land (z \lor y)$와 같은 형태이다. 괄호로 묶인 각 부분을 절이라고 하며, 절은 변수 두 개를 $\lor$로 묶은 것이다. $\lor$는 OR, $\land$는 AND, $\lnot$은 NOT을 뜻한다.

변수의 개수 $N$과 절의 개수 $M$, 그리고 식 $f$가 주어졌을 때, 식 $f$를 true로 만들 수 있는지 없는지를 판정하는 프로그램을 작성하시오.

예를 들어 $N = 3$, $M = 4$이고 $f = (\lnot x_1 \lor x_2) \land (\lnot x_2 \lor x_3) \land (x_1 \lor x_3) \land (x_3 \lor x_2)$인 경우, $x_1$을 false, $x_2$를 false, $x_3$을 true로 정하면 식 $f$가 true가 된다. 반면 $N = 1$, $M = 2$이고 $f = (x_1 \lor x_1) \land (\lnot x_1 \lor \lnot x_1)$인 경우에는 $x_1$에 어떤 값을 넣어도 식 $f$를 true로 만들 수 없다.

첫째 줄에 변수의 개수 $N$ ($1 \le N \le 20$)과 절의 개수 $M$ ($1 \le M \le 100$)이 주어진다. 둘째 줄부터 $M$개의 줄에 절이 한 줄에 하나씩 주어진다. 절은 두 정수 $i$와 $j$ ($1 \le |i|, |j| \le N$)로 이루어지며, 양수는 각각 $x_i$와 $x_j$를, 음수는 각각 $\lnot x_{-i}$와 $\lnot x_{-j}$를 뜻한다.

첫째 줄에 식 $f$를 true로 만들 수 있으면 1을, 없으면 0을 출력한다.