This page is still under construction.

Parts of this page are still being built. What you see may change.

3-SAT 2

Time limit2sMemory limit512 MB

Summary
Given a 3-CNF formula with N variables and M clauses, decide whether it is satisfiable and, if so, output a satisfying assignment.
Level

Hard8 of 10

Topics
Graph, DFS, Implementation, Math
Solved
No attempts yet

Problem

3-SAT is the problem of, given (N) Boolean variables (x_1, x_2, \dots, x_n), deciding which values to assign to (x_i) to make a 3-CNF formula true.

A 3-CNF formula has the form ( ( 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 ) ). Each parenthesized expression is called a clause, and a clause consists of three variables joined with (\lor). (\lor) denotes OR, (\land) denotes AND, and (\lnot) denotes NOT.

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

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

Input

The first line gives the number of variables (N) (1 ≤ (N) ≤ 1,000) and the number of clauses (M) (1 ≤ (M) ≤ 10,000). The next (M) lines give the clauses. A clause consists of three integers (i, j, k) (1 ≤ (|i|, |j|, |k|) ≤ (N)); a positive (i, j, k) denotes (x_i, x_j, x_k) respectively, and a negative (i, j, k) denotes (\lnot x_{-i}, \lnot x_{-j}, \lnot x_{-k}) respectively.

Output

On the first line, print 1 if (f) can be made true and 0 otherwise.

If (f) can be made true, then on the second line print the values of (x_i) that make (f) true, in order from (x_1). Print true as 1 and false as 0.

Examples4

  1. Example 1

    Input
    3 4
-1 2 3
-1 -2 3
1 -2 3
3 -2 -1
    Expected output
    1
0 0 1

  2. Example 2

    Input
    6 8
1 6 2
3 -4 5
2 -2 3
5 -1 4
-4 6 -2
1 -6 -3
2 -3 4
6 -4 -1
    Expected output
    1
0 1 0 0 1 1

  3. Example 3

    Input
    6 8
-1 6 2
-3 -4 5
2 -2 -3
5 -1 -4
-4 -6 -2
1 -6 -3
2 -3 4
6 -4 -1
    Expected output
    1
0 1 0 0 1 0

  4. Example 4

    Input
    1 2
1 1 1
-1 -1 -1
    Expected output
    0