2 Sat

AC一覧

Problem Statement
問題文

Given 2-Sat with $N$ variables and $M$ clauses. Check the satisfiability and if satisfiable, construct the assignment of variables.

$N$ 変数 $M$ 節の 2 Sat が与えられる。充足可能か判定し、可能ならば割り当てを一つ求めてください。

Constraints
制約

Input
入力

2-Sat is given as DIMACS format. Please see the samples.

DIMACS 標準形式 で与えられる。 サンプルも参考にせよ

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:

$x_i$ は、$i$ 番目の変数が真ならば $i$、偽ならば $-i$

充足不可能な場合は以下

s UNSATISFIABLE

Sample
サンプル

# 1

p cnf 5 6
1 2 0
-3 -1 0
-4 -3 0
2 -5 0
5 -2 0
1 4 0
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) $$

を表す

# 2

p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0
s UNSATISFIABLE

Forum


Timelimit: 5 secs

Before submitting, please confirm terms and conditions