東京大学プログラミングコンテスト2013

E - 2-SAT


Time limit時間制限 : 2sec / Memory limitメモリ制限 : 256MB

問題

背景

うなぎ王国の王子様は,CNFが大好きだ.毎日,充足解を求め遊んでいた.そんな王子様もそろそろ充足可能性問題に飽きてきた.そこで王子様は,王様に変わった問題を出してもらうことにした.今度の問題は論理式だけでなく,変数の割り当ても入力されるようだ.

課題

2-SAT(satisfiability)とは,節の長さが(高々)2の乗法標準形で表された論理式(2-CNF)が与えられた時に,各変数にtrue/falseに適切に割り当てることで,論理式が充足可能であるかを判定する問題である.今,あなたは2-CNFと各変数へのtrue/falseの割り当てが与えられる.しかし,残念ながらこの変数割り当ては充足解ではないかもしれない.割り当てが充足解となるために必要な変数の割り当ての変更回数の最小値を求めよ.ただし,答えが11以上であるか論理式が充足不可能である場合には "TOO LARGE" と出力せよ.

配点

200

入力

入力は以下の形式で与えられる.

n m
cnf
a1a2...an

n は変数の数,m は節の数を表す. a1a2...an は変数の割当を表し,ai=T ならば変数 i の割当がtrueであり,ai=F ならば変数 i の割当がfalseであることを意味する.2-CNFは以下のBNFで与えられる.

<cnf> ::= <clause> | <clause>"^"<cnf>
<clause> ::= "("<literal>"v"<literal>")"
<literal> ::= <var> | "~"<var>
<var> ::= [1-9] | <var>[0-9]

制約

入力中の各変数は以下の制約を満たす.

出力

割り当てが充足解となるために必要な変数の割り当ての変更回数の最小値を一行に出力せよ.ただし,答えが11以上であるか論理式が充足不可能である場合には "TOO LARGE" と出力せよ.

入力例1

4 2
(~1v2)^(3v~4)
TTFF

入力例1に対する出力例

0

この割り当てはすでに与えられた2-CNFを充足している.

入力例2

3 4
(~1v~2)^(1v3)^(2v~1)^(~3v1)
FFT

入力例2に対する出力例

TOO LARGE

この2-CNFは充足解を持たない.

入力例3

22 11
(1v2)^(3v4)^(5v6)^(7v8)^(9v10)^(11v12)^(13v14)^(15v16)^(17v18)^(19v20)^(21v22)
FFFFFFFFFFFFFFFFFFFFFF

入力例3に対する出力例

TOO LARGE

最低でも11個の変数の割当を変更しなければ,この2-CNFを充足させることはできない.


Submit提出する