問題

背景

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

課題

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

配点

200

入力

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

n m
cnf
a1a2...an

n は変数の数，m は節の数を表す． a₁a₂...a_n は変数の割当を表し，a_i=T ならば変数 i の割当がtrueであり，a_i=F ならば変数 i の割当がfalseであることを意味する．2-CNFは以下のBNFで与えられる．

• "^" は論理積，"v" は論理和，"~" は否定演算子を表す
• 各変数は 1,2,...,n-1,n で表される

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

制約

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

• 1 \leq n \leq 10000 (=10⁴)
• 1 \leq m \leq 100000 (=10⁵)
• BNF中の <var> の値は 1 から n である

出力

割り当てが充足解となるために必要な変数の割り当ての変更回数の最小値を一行に出力せよ．ただし，答えが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を充足させることはできない．