9001: [yosupo] Other - 2 Sat
[Creator : ]
Description
Given 2-Sat with $N$ variables and $M$ clauses. Check the satisfiability and if satisfiable, construct the assignment of variables.
Input
2-Sat is given as [DIMACS format](http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf). Please see the samples.
p cnf $N$ $M$
$a_1$ $b_1$ 0
$a_2$ $b_2$ 0
:
$a_M$ $b_M$ 0
p cnf $N$ $M$
$a_1$ $b_1$ 0
$a_2$ $b_2$ 0
:
$a_M$ $b_M$ 0
Output
If the input is satisfiable, print as follows:
s SATISFIABLE
v $x_1$ $x_2$ ... $x_N$ 0
If $i$-th variable is true, $x_i = i$, and is false, $x_i = -i$.
If the input is not satisfiable,print as follows:
s SATISFIABLE
v $x_1$ $x_2$ ... $x_N$ 0
If $i$-th variable is true, $x_i = i$, and is false, $x_i = -i$.
If the input is not satisfiable,print as follows:
s UNSATISFIABLE
Constraints
$1 \leq N \leq 500,000$
$1 \leq M \leq 500,000$
$1 \leq M \leq 500,000$
Sample 1 Input
p cnf 5 6
1 2 0
-3 -1 0
-4 -3 0
2 -5 0
5 -2 0
1 4 0
Sample 1 Output
s SATISFIABLE
v -1 2 -3 4 5 0
This sample means as follows:
$(x_1 \lor x_2) \land\ (\lnot x_3 \lor \lnot x_1) \land\ (\lnot x_4 \lor \lnot x_3) \land\ (x_2 \lor \lnot x_5) \land\ (x_5 \lor \lnot x_2) \land\ (x_1 \lor x_4)$
$(x_1 \lor x_2) \land\ (\lnot x_3 \lor \lnot x_1) \land\ (\lnot x_4 \lor \lnot x_3) \land\ (x_2 \lor \lnot x_5) \land\ (x_5 \lor \lnot x_2) \land\ (x_1 \lor x_4)$
Sample 2 Input
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0
Sample 2 Output
s UNSATISFIABLE