2-SAT

问题描述

给定一个含 $N$ 个变量和 $M$ 个子句的 2-SAT 实例。判断其是否可满足；若可满足，构造一组变量赋值。

约束条件

• $1 \leq N \leq 500\,000$
• $1 \leq M \leq 500\,000$

输入

2-SAT 实例以 DIMACS 格式给出，格式如下：

p cnf N M
a₁ b₁ 0
a₂ b₂ 0
:
a_M b_M 0

其中每个子句形如 a b 0，表示文字 $a$ 与 $b$ 的析取（OR）。正数表示对应变量为真，负数表示为假，每行以 0 结尾。

输出

若输入可满足，输出如下：

s SATISFIABLE
v x₁ x₂ … x_N 0

其中：若第 $i$ 个变量为真，则 $x_i = i$；若为假，则 $x_i = -i$；末尾必须有 0。

若不可满足，输出：

s UNSATISFIABLE

样例

样例 1

输入：

p cnf 3 4
-1 2 0
-2 3 0
-3 1 0
-1 -3 0

输出：

s SATISFIABLE
v -1 -2 -3 0

解释：
该 2-SAT 实例包含 3 个变量和 4 个子句，等价于以下逻辑公式：

$$(\neg x_1 \lor x_2) \land (\neg x_2 \lor x_3) \land (\neg x_3 \lor x_1) \land (\neg x_1 \lor \neg x_3)$$

当 $x_1 = \text{false}, x_2 = \text{false}, x_3 = \text{false}$ 时，所有子句均为真，因此可满足。输出中 -1 -2 -3 表示三个变量均取假值。

样例 2

输入：

p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0

输出：

s UNSATISFIABLE