誤読

文字通りくそコード

2-SAT (ARC069-F)

ARC069-Fがすごく解きたかった

2-SATは知ってた(以前minisatとか触った関連)ので書くのにはそんなに困らなかった。

解の構築は普通にできそうだけど、どこにも書いてないのが怖い(今度書いてみるよ)

さらっと探してみても使う問題を見ないし、実はだるかったりするんかな

・ARC069-F Flag

にぶたんはそれはそうで、判定部に2-SATを使う。

普通に2-SATを組むとすると、

候補2つのうちどちらか1つだけを使う ( ( ¬ A ) ∨ ( ¬ B )) ∧ ( A ∨ B ) に加えて、

各旗候補地についてmid以内にある旗と共存できないっていうのを

¬ ( A ∧ B ) → ( ¬ A ) ∨ ( ¬ B )と書き換えられることを使って表すことになる。

しかし、これだとImplicationグラフでの辺の数がO(V^2)とかになってやばいので減らす努力をしなければならない。


各旗候補地について、共存できないとして論理式につっこむのは連続してる旗たちなので

区間をセグ木っぽく表してあげて、 旗と共存できない ではなく 区間と共存できない として論理式を作ってあげるとO(VlogV)の辺で抑えられる。


また、親の区間が偽なら子の区間はかならず偽(その逆はない)なので ( ( ¬子 ) ∨ 親 ) を加える

f:id:akihiro1001:20170327122002j:plain:w500

僕のソース
Submission #1180258 - AtCoder Regular Contest 069 | AtCoder

bool TWO_SAT(int n, vector<pii> clause, vector<int> &ans) {
	DGraph g(n * 2);
	for (auto itr : clause) {
		g.con(itr.first + n, itr.second);
		g.con(itr.first, itr.second + n);
	}
	vector<int> scc;
	SCC(g, scc);

	REP(i, n) {
		if (scc[i] == scc[i + n]) {
			return 0;
		}
	}

	return 1;
}

  
・備考

TWO_SATってめちゃくちゃダサくないか

必要十分な論理式を考えるのがほんと難しい

論理式を考えるのがすごく楽しい