3-SAT 2
시간 제한2초메모리 제한512 MB
N개의 변수와 M개의 절로 이루어진 3-CNF 논리식이 주어질 때, 이 식을 참으로 만드는 변수 배정이 존재하는지 판정하고 존재하면 그 배정을 출력한다.
문제
3-SAT은 (N)개의 불리언 변수 (x_1, x_2, \dots, x_n)가 있을 때, 3-CNF 식을 true로 만들기 위해 (x_i)를 어떤 값으로 정해야 하는지를 구하는 문제이다.
3-CNF 식은 ( ( x \lor y \lor \lnot z ) \land ( x \lor \lnot y \lor z ) \land ( \lnot w \lor x \lor \lnot z ) \land ( x \lor z \lor y ) )와 같은 형태이다. 여기서 괄호로 묶인 식을 절(clause)이라고 하는데, 절은 3개의 변수를 (\lor)한 것으로 이루어져 있다. (\lor)는 OR, (\land)는 AND, (\lnot)은 NOT을 나타낸다.
변수의 개수 (N)과 절의 개수 (M), 그리고 식 (f)가 주어졌을 때, 식 (f)를 true로 만들 수 있는지 없는지를 구하는 프로그램을 작성하시오.
예를 들어, (N = 3), (M = 4)이고 (f = ( \lnot x_1 \lor x_2 \lor x_3 ) \land ( \lnot x_1 \lor \lnot x_2 \lor x_3 ) \land ( x_1 \lor \lnot x_2 \lor x_3 ) \land ( x_3 \lor \lnot x_2 \lor \lnot x_1 ))인 경우, (x_1)을 false, (x_2)를 false, (x_3)를 true로 정하면 식 (f)를 true로 만들 수 있다. 하지만 (N = 1), (M = 2)이고 (f = ( x_1 \lor x_1 \lor x_1 ) \land ( \lnot x_1 \lor \lnot x_1 \lor \lnot x_1 ))인 경우에는 (x_1)에 어떤 값을 넣어도 식 (f)를 true로 만들 수 없다.
입력
첫째 줄에 변수의 개수 (N) (1 ≤ (N) ≤ 1,000)과 절의 개수 (M) (1 ≤ (M) ≤ 10,000)이 주어진다. 둘째 줄부터 (M)개의 줄에는 절이 주어진다. 절은 세 정수 (i, j, k) (1 ≤ (|i|, |j|, |k|) ≤ (N))로 이루어져 있으며, (i, j, k)가 양수인 경우에는 각각 (x_i, x_j, x_k)를 나타내고, 음수인 경우에는 (\lnot x_{-i}, \lnot x_{-j}, \lnot x_{-k})를 나타낸다.
출력
첫째 줄에 식 (f)를 true로 만들 수 있으면 1을, 없으면 0을 출력한다.
(f)를 true로 만들 수 있는 경우에는 둘째 줄에 식 (f)를 true로 만드는 (x_i)의 값을 (x_1)부터 순서대로 출력한다. true는 1, false는 0으로 출력한다.