2-SAT Assignment

2-SAT asks whether the boolean variables $x_1, x_2, \dots, x_N$ can be assigned values that make a given 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. A clause joins two literals with $\lor$, and a literal is a variable or the negation of a variable. 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$, decide whether $f$ can be made true, and give the values of the variables when it can.

For $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$ false, $x_2$ false, and $x_3$ true makes $f$ true. For $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 contains 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 holds one clause as two integers $i$ and $j$ ($1 \le |i|, |j| \le N$). A positive $i$ means the literal $x_i$, and a negative $i$ means the literal $\lnot x_{-i}$. The same variable may appear twice in one clause, and the same clause may be given more than once.

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

If it can, print the values of $x_1$ through $x_N$ in order on the second line, separated by single spaces. Write 1 for true and 0 for false.

When several assignments make $f$ true, print only the one whose sequence $(x_1, x_2, \dots, x_N)$ is lexicographically smallest. That is, walk the variables in order: keeping the values already fixed, set the current variable to 0 if the remaining variables can still make $f$ true, and set it to 1 only when they cannot.