2-SAT 배정 구하기

2-SAT은 불리언 변수 $x_1, x_2, \dots, x_N$의 값을 정해서 주어진 2-CNF 식을 참으로 만들 수 있는지 판정하는 문제다.

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$를 참으로 만들 수 있는지 판정하고, 만들 수 있으면 변수의 값도 함께 구하는 프로그램을 작성하시오.

$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$을 거짓, $x_2$를 거짓, $x_3$을 참으로 두었을 때 $f$가 참이 된다. 반대로 $N = 1$, $M = 2$, $f = (x_1 \lor x_1) \land (\lnot x_1 \lor \lnot x_1)$이면 $x_1$에 무슨 값을 넣어도 $f$는 거짓이다.

첫째 줄에 변수의 개수 $N$ ($1 \le N \le 20$)과 절의 개수 $M$ ($1 \le M \le 100$)이 주어진다.

둘째 줄부터 $M$개의 줄에 절이 한 줄에 하나씩 주어진다. 각 절은 두 정수 $i$와 $j$ ($1 \le |i|, |j| \le N$)로 이루어진다. 양수 $i$는 리터럴 $x_i$를, 음수 $i$는 리터럴 $\lnot x_{-i}$를 뜻한다. 한 절에 같은 변수가 두 번 나올 수 있고, 같은 절이 여러 번 주어질 수도 있다.

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

참으로 만들 수 있으면 둘째 줄에 $x_1$부터 $x_N$까지의 값을 순서대로 공백 하나로 구분해 출력한다. 참은 1, 거짓은 0으로 적는다.

$f$를 참으로 만드는 배정이 여럿이면 수열 $(x_1, x_2, \dots, x_N)$이 사전순으로 가장 작은 것 하나만 출력한다. 즉 앞에서부터 차례로, 이미 정한 값을 그대로 둔 채 남은 변수로 $f$를 참으로 만들 수 있으면 그 변수를 0으로 정하고, 그럴 수 없을 때만 1로 정한다.