TCO R3B Hard

solution.txt

rを根、LCA(h[a],h[b])=cとして、cを寝とする部分木をt、cの子を根とする部分木をt_i(1≦i≦子の数)とする。
以下の新たな変数を置く。
・Ta_i: h[a]が部分木t_iのどこかにある (単にTaならtのどこか)
・Tb_i: h[b]が部分木t_iのどこかにある（単にTbならtのどこか）
・Av: h[a]を頂点vに割り当てる
・Bv: h[b]を頂点vに割り当てる
条件節は以下の通り。＊はbについても同様の条件節を作る。
＊ Ta = true
・ ~Ta_i ∨ ~Tb_i
＊ ~Ta ∨ Ta_i
＊ ~Ta ∨ Ac
下の２式を葉まで再帰的にやると上手く機能する。