2-SAT Satisfiability

2-SAT asks whether boolean variables $x_1, x_2, \ldots, x_N$ can be assigned values that make a 2-CNF formula true.

A 2-CNF formula looks like $(x \lor y) \land (\lnot y \lor z) \land (x \lor \lnot z) \land (z \lor y)$. Each parenthesized part is a clause, and a clause is two variables joined by $\lor$. Here $\lor$ is OR, $\land$ is AND, and $\lnot$ is NOT.

Given the number of variables $N$, the number of clauses $M$, and the formula $f$, write a program that decides whether $f$ can be made true.

For example, take $N = 3$, $M = 4$, and $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)$. Setting $x_1$ to false, $x_2$ to false, and $x_3$ to true makes $f$ true. With $N = 1$, $M = 2$, and $f = (x_1 \lor x_1) \land (\lnot x_1 \lor \lnot x_1)$, no value of $x_1$ makes $f$ true.

The first line has the number of variables $N$ ($1 \le N \le 20$) and the number of clauses $M$ ($1 \le M \le 100$). Each of the next $M$ lines has one clause, given as two integers $i$ and $j$ ($1 \le |i|, |j| \le N$). A positive integer means $x_i$ or $x_j$, and a negative integer means $\lnot x_{-i}$ or $\lnot x_{-j}$.

Print 1 on the first line if $f$ can be made true, and 0 otherwise.