A
v = max(H, W)として、ceil(N/v)です。

B
区間スケジューリング。典型とは言え200はビビりました。

C
基本K個のSとN-K個のS+1で良いんですが、S=10^9の時だけN-K個の数を1にします。ギャグ。

D
個人的には解きやすかった。indexの距離の偶奇でAとBどちらを取るか決まります。あとはbitdpで前から順番に決めていけばよいです。
popcountすれば偶奇の判定も簡単です。

int N;
int dp[(1 << 18)][18];
int A[18], B[18];

void solve() {
	cin >> N;
	rep(i, 0, N) cin >> A[i];
	rep(i, 0, N) cin >> B[i];

	rep(bit, 0, (1 << 18)) {
		rep(i, 0, N) dp[bit][i] = inf;
	}

	dp[0][0] = 0;

	rep(bit, 0, (1 << N)) {
		rep(i, 0, N) {
			if(dp[bit][i] == inf) continue;
			int cnt = 0;
			rep(j, 0, N) {
				if(bit & (1 << j)) continue;
				int v = (__builtin_popcount(bit) - j + 50) % 2 == 0 ? A[j] : B[j];
				int pv = bit == 0 ? -1 : (__builtin_popcount(bit) - 1 - i + 50) % 2 == 0 ? A[i] : B[i];
				if(pv <= v) MIN(dp[bit | (1 << j)][j], dp[bit][i] + cnt);


				cnt += ((bit & (1 << j)) == 0);
			}
		}
	}
	int res = inf;
	rep(i, 0, N) MIN(res, dp[(1 << N) - 1][i]);
	if(res == inf) cout << -1 << "\n";
	else cout << res << "\n";
}

E
まず辺にどちらの頂点が大きいかで不等式をつけてみたところ、ある1点のみに小なりの符号が集中しているとできないことが
わかりました。逆に小なりの符号が集中しているのが、2点以上の等号による連結成分ならうまく行くだろうとなり、
構成法を色々考えていたんですが、コストの大きい頂点から辺を張っていくことを
ずっと考えていたせいでわかりませんでした。(小さい方からなら簡単です)でも偶然max(D_u,D_v)みたいなコストの辺で最小全域木を作る問題を
思い出したので、(https://atcoder.jp/contests/arc098/tasks/arc098_d)
それで全域木を作ってみた所、木上で2色彩色するだけになり簡単に構成できました。
1WA出したんですがこれは一箇所MとNを入れ替えていたためです…なんか木の場合を入力に入れたら都合よくバグってくれました。

2020-01-18

KUPC2019

ちょっと気になった問題取り上げます。

https://atcoder.jp/contests/kupc2019/tasks/kupc2019_e

木ごとにgrundyするのかなと思ったんですが、ゲームが分割されているわけではないので今回では
あんまり役に立たないです。木ごとに単なる勝ち負けを求めても、最適moveではわざと負けるみたいな
ことをする可能性もあります。なので、(i)「手番が必ず変わらない」(ii)「手番が必ず変わる」(iii)「手番が変わるかを先手が選べる」
(iv)「手番が変わるか後手が選べる」の4パターンに分類すると良いです。
すると複数の木を見て回った後の勝敗も上の4パターンに分類できます。しかし(i)は無視できるので実質3パターンです。
(iii)が一つでもあるなら、残りのN-1の勝敗パターンを見てから先手が決められるので先手の勝利です。
(iii)がないなら、(iv)を先に選んでしまうと後手が残りの木の勝敗を見て勝利するように行動できるので負けです。
よって(ii)を順番に選んでいくゲームになり、(ii)が偶数個なら後手勝ち、奇数個なら先手勝ちとなります。

https://atcoder.jp/contests/kupc2019/tasks/kupc2019_f

まず区間ではモンスターを一点集中させるのが良いことを証明できます。これは簡単で、
区間でb_l,...,b_rとモンスターを配置したなら、argmin(A_i-b_i)に集中させても解は小さくなりません。
事前にどの地点にモンスターを配置するか決めてしまえば、解は(区間のうち配置地点を含むものの和)-(配置地点の勇者の数)
となります。ここで
dp(i):=0~i地点まで見てi地点にはモンスターを配置すると決めた時のコストの最大値とすれば、
dp(i)からdp(j)への遷移は(始点が(i,j]でjを含むような区間の和)-A_jとなり、これはjで平面走査すればO(NlogN)で行えます。
全てのiについて見ていっても合計でO(N^2logN)です。

https://atcoder.jp/contests/kupc2019/tasks/kupc2019_g

abca
bcab
cabc
abca

これが思いつけるかが全てです。あとは端を延長することによって達成できます。

2020-01-17

初手累積和

数列{a_i}に対して区間addの操作をする時、
b_i=a_i-a_{i-1}(a_{-1}=0とする)と{b_i}を定義すると以下のように言い換えられます。

「{a_i}で[l, r)の範囲の値を+a」 <=> 「{b_i}でlを+a、rを-a」

こうすると、区間の操作が1点操作になって見やすい形になります。{a_i}を復元するには累積和を取ればいいです。
{a_i}を微分したものが{b_i}になっていると見ることも出来ます。よって{a_i}についてΣf(x)を区間で足す時は
{b_i}でf(x)を足し引きすると言い換えられる可能性が高いです。

imos法はまさにこれをやっているわけですが、imos法を陽に使わない場合でもこのテクニックを使う問題があります。
https://atcoder.jp/contests/cf17-final/tasks/cf17_final_e
https://atcoder.jp/contests/agc010/tasks/agc010_b ([l, r)に含まれるjにΣ_{i=1}^{j-l+1} 1 を足すと見れます)
https://atcoder.jp/contests/arc080/tasks/arc080_d

微分ではなく積分を取る問題も有ります。
https://atcoder.jp/contests/dwacon5th-final/tasks/dwacon5th_final_b

でもこのパターンは流石にXOR位しか出ないんじゃないかなと思っています。

いかにもこのパターンなのに逆に見づらくなる問題も存在します。
https://atcoder.jp/contests/jsc2019-qual/tasks/jsc2019_qual_c

微分をすると、操作を通して同じマスを2回以上選ぶことが出来ない条件がわかりにくくなります。
このような問題は区間を左端sortして順番に見て行ったり、iterationを回すことが肝となることが多いです。
実際上で挙げた
https://atcoder.jp/contests/cf17-final/tasks/cf17_final_e
はiterationを回しても解けます。

2020-01-15

第6回ドワンゴからの挑戦状予選

https://atcoder.jp/contests/dwacon6th-prelims

うーん

A
後から見ていけばいいです。

B
400はすぐわかったんで実装して後はOEIS入れればわかるやろwってなったのでやったんですがsampleが全然合わない。
愚直も書いたんですがそれもバグらせて散々でした。
解法ですが、各n-1区間で掛ける係数がわかればいいです。区間[x_i,x_i+1)のうち、スライムj(<=i)由来のものは
(n-1)!/(i-j+1)と求まるので、あとは簡単な足し算で求まります。400はiを削除してnが一つ減った場合に帰着するdpです。
ちなみに係数をOEISに入れても出てきません(絶望)

C
積の期待値をtupleの数に言い換える典型です。しかしABDみた後に着手したので遅かった。

D
あきらかに条件がゆるゆるなので適当に貪欲にやって、最後の6要素だけは全探索すればいいと思ったんですが嘘でした。
800点なんだからなんか非自明な条件が存在するだろうと思えればよかったんですがね…
ある頂点に集中するのがヤバイのでそうなってないかを確認しながら先頭から決めていけばよいです。

2020-01-15

Educational Codeforces Round 80 (Rated for Div. 2)

https://codeforces.com/contest/1288

突然ですがblog再開です。

A
凸なので解が小さくなり始めたらbreakすれば良いんですが条件を若干間違えてWA...
コンテスト後100000までやるってのを見て賢いと思いました。

B
bの桁数を固定してしまえばbは9999....のようにしかなりえません。Aは範囲内ならなんでもいいです。

C
数列内の不等式が成り立っていればあとはa_m <= b_mであればいいです。
a_mとb_mを固定して数列ごとに独立に場合の数をdpで求めました。
しかし長さ2mの数列に見立てれば一つのdpで済んだ上に、経路数に帰着してしまえばO(1)で済みます。

D
maxと見えたのでにぶたんしたら出来ました。2つの値のorを取ったら全bitが埋まっているという条件になるので前計算で
そのような値のpairを全て求めておきます。

E
最大が本質パートです。数列の先頭にn n-1 n-2 ... 1を追加すると、同じ数の間に入っている数の種類数を求めればいいことになります。
例えば5 4 3 2 1 3 5 1 4 1なら1同士の間には{3, 5}と{4}が含まれるので、max(|{3,5}|, |{4}|)+1=3を答えにすればいいです。
最初計算量を下げられる気がしなかったんですが(というか種類数を扱うので平方分割だと思った)、2次元座標で可視化したらあっさりでした。indexが小さい順から見ていって、同じ数内では一番最後に見たものだけ管理していけば良いです。これはBITで実装できます。

F
なんか線形計画問題にしてみたんですがよくわからなかったです…

2019-12-23

SAT Solver作ってみた

この記事は
https://adventar.org/calendars/4520
の22日目の記事として書かれました。昨日はRisebbitさんのシークエント計算の自動証明を実装してみたでした。

夏休みなんかノリでSAT Solverを作ったんで、大変だったところとか書いておきます。

SATとは?

論理式充足問題と言います。例えば $(b_1 \rightarrow b_2) \land(b_2 \land (\lnot b_3 \lor \lnot b_1))$ を充足する変数 $b_1, b_2, b_3$ の真偽の割り当ては存在するか?みたいな感じです。この場合なら、 $b_1=false, b_2=true, b_3=true$ が条件を満たしますね。通常はCNF形式という形に変換してから解きます。上の例なら $(\lnot b_1 \lor b_2) \land (b_2) \land (\lnot b_3 \land \lnot b_1)$ となります。このように $\lor$ で結合された"節"を更に $\land$ で結合した形で表されます。全ての論理式がCNFに変換できることは示せます。

SATが解けて何か嬉しいんか?

SATは単純ゆえ高速化の技術が進歩しています。NP完全問題にかかわらず変数の数が10⁵オーダーの問題も解けるというから驚きです。解きたい問題がSATに帰着さえできれば解ける可能性があるということでもあります。実際以下のような問題で成功を収めているようです。

プランニング (SATPLAN, Blackbox) [Kautz+, 1992]
自動テストパターン生成 [Larrabee, 1992]
ジョブショップスケジューリング [Crawford+, 1994]
有界モデル検査 [Biere, 2009]
ソフトウェア検証 (Alloy) [Jackson, 2006]
書換えシステム (AProVE) [J¨urgen+, 2004]
インテル社の i7 プロセッサの検証 [Kaivola+, 2009]
Eclipse のコンポーネント間の依存解析 [Le Berre+, 2009] 
解集合プログラミング (clasp) [Gebser+, 2012]
Linux のパッケージマネージャである DNF の依存性解決
制約充足問題 (Sugar) [Tamura+, 2009]
　▶ オープンショップスケジューリング問題の未解決問題の求解[Tamura+, 2009]
　▶ パッキング配列問題の未解決問題の求解 [則武+, 2013]

まあこういうのは建前でなんかNP完全問題を解いてるってだけで興奮しませんか…?

SATの高速化技術

ベースにCDCLというアルゴリズムがあり、実装技術、経験的に良いとわかっているヒューリスティックスがたくさんあります。その中から実装したものを紹介します。詳しくは参考資料を見てください。

DPLL

簡単に言ってしまえばバックトラックアルゴリズムです。変数の真偽を決めていって、失敗したら真偽値を変えて続行という感じです。ある変数の真偽を固定した時、他の変数の真偽がどれだけ決まるか計算することを単位伝播と呼んだりします。SAT Solverで一番最初に出てきたアルゴリズムであり、CDCLの礎にもなっています。

CDCL

CDCLに関してはとてもわかりやすいスライドがあるのでこちらをご覧ください。

How a CDCL SAT solver works from Masahiro Sakai

簡単に何をやっているか説明していると、DPLLの要領で順番に真偽を決め単位伝播し、矛盾したらその原因となった割り当てを特定し、その割り当ての真偽を反転させたものを新しく追加する感じです。新しく足された節を学習節と呼びます。学習節のおかげで同じような論理式の割り当てをした時に矛盾が早期の段階で起こるようになり、効率的な探索が行えるようになります。

VSIDS

Variable State Independent Decaying Sumの略です。変数に得点をつけておき、得点の高い順番から真偽割り当てを行うようにします。Decayingとあるように、定期的に全変数の得点を割合で減らします。(0.5倍とか)

学習節の削除

CDCLを回すと大量の学習節が生まれます。それらにも序列があって、論理の肝になるやつと、ただただ(速度面で)単位伝播の邪魔になるものもあります。それらを区別するために学習節にも得点をつけ、その得点が低い順から定期的に削除するようにします。得点は真面目にやるとLBD(Literal Blocks Distance)などの方式がありますが、自分の実装ではVSIDSのようなスコアを使っています。実装が楽なんでね。

リスタート

文字通り今までの変数割り当てを解除して最初からやり直すことです。すると探索範囲が変わって今までとは違うタイプの学習節が獲得できるのではないかというアイディアです。

監視リテラル

VSIDS、学習節の削除、リスタートはヒューリスティックですが、これは実装面での改善です。
実は節の中で常に見ておく必要がある変数は2つだけです。2つ真の変数を見ておき、どちらかが偽になったら真の変数を節中で探します。もし2つ見つからなかったら、もうひとつの変数は必ず真である必要があるので真の割り当てをします。2つ見つかったら、監視中ではない方を新たに監視すればいいです。これにより単位伝播の速度がだいぶ改善されます。
これは実装が辛いです。いろんなパターンがあって結構バグりました。資料はたくさん上がってるんですが全てのパターンを網羅できているものは少なかったです。

実測

Minisatという軽実装で実用的なsat solverがあるのでそれと比較しました。

	CNFのタイプ	自作sat	Minisat
case1	数独(変数729個,節3257個)	120.6s	2.942s
case2	変数60個,節937個のUNSAT	10.82s	7.096s
case3	変数41個,節224個のSAT	4.647s	1.376s

変数が3000個とかになると、Minisatでは一瞬、自作satでは永遠に解けないみたいな問題がたくさんありました。

1sあたりのバックトラック回数	Case1	case2	case3
自作sat	$1.731 \times 10^4$	$2.586 \times 10^4$	$8.749 \times 10^4$
Minisat	$1.505 \times 10^5$	$1.345 \times 10^5$	$4.409 \times 10^5$

ちなみにcase1の数独は

9 0 0 0 0 0 1 8 0
0 0 0 4 0 0 0 0 0
7 0 0 0 0 3 0 0 0
0 4 0 1 0 0 0 0 0
0 0 0 0 8 0 0 2 0
0 3 6 0 0 0 0 0 0
0 0 0 0 2 0 0 0 0
0 0 0 6 0 0 0 0 3
0 5 0 0 0 0 4 0 0

をCNFに変換したものを使いました。0が空白マスです。一応難易度:難となっていたので難しいはず?

改善点

バックトラック回数からわかるようになんか遅い。何がボトルネックになっているのかよくわからないが特定する。制作期間中の後半ずっと考えてたんですけどわかりませんでしたね…データ構造が悪いのかな…

リスタート戦略、学習節の得点のヒューリスティックスがあんまり良くない気がするのでそこら辺を改善する。リスタート戦略に関しては実装していない可能性すらある。(!?)(4ヶ月前なので忘れてしまった)

明日はiojjooさんのゲームの話です。楽しみですね。

コード

https://github.com/omosan0627/sat_solver

参考資料

https://www.slideshare.net/sakai/satsmt
http://www-erato.ist.hokudai.ac.jp/docs/seminar/nabeshima.pdf
http://minisat.se/
超自己流！競プロ解説記事の書き方 - Mister雑記 (この記事はここの方法で書かれました)

2019-09-02

TTPC2019参加記

東京工業大学プログラミングコンテスト2019 - AtCoder

risujirohさんJoe先輩とチームを組んで5位(オンサイト2位)でした。

最初はrisujirohさんとの2人チームだったんですが、僕がJSC2019の予選で橙から黄に転落したことで、3人でチームを組めることに。会場でもう1人拾うかとなった時にJoe先輩が加入してくれました。

戦略

というとオーバーですが、開幕はrisujirohさんがBDF、Joe先輩がACEを担当し、僕がG以降の問題を読んでました。AからFはコンテストのなかで一番簡単な問題だということが事前に公表されていたので、僕よりも速解きが得意な2人に担当してもらうのが良さそうということになりました。

G以降の所見の感想

G:これは解けるタイプの10^9+7だなぁ。
H:問題分が長いW
I:なんだこれ。制約がでかい数学はやめてくれ。
J:操作が謎すぎる。数学だし飛ばし。
K:AGCっぽさを感じた。解けるかも。
L:構文解析はまだしも多項式に関する問題はNG
M:全ての根について求めるんだから全方位木DPじゃないですか。
N:問題文が長くてよく読みませんでした。でも後から見返すと無理数を使ってゲームをしていて無理を極めてる。
O:構築ということしか把握してなかった。

なので解けそうなGKMの中でもGは簡単そうだったので着手しました。

ABD
問題文を読んでいるうちになんか2人が爆速で通してました。

E
これも知らない間にJoe先輩が通してました。

C
Joe先輩に問題と実装内容を説明してもらったんですが、どうやらa_i<=Xを忘れていただけっぽかったです。そのままAC。
あと__builtin_clzの仕様(0を代入された時の挙動は未定義)でハマっていたっぽいんですが、オセロのbitboardを実装したこともあって偶然知っていたので、伝えられればよかったなぁとちょっぴり後悔しました。

I
risujirohさんがlogを2つつけたものを提出したんですがTLE。WAもあってよくわからない。ここで一旦Iから離れたのは英断だと思います。

G
どうやら本質的には3つの値しかなくて、K回の操作である回文を作れたら、その回文はK+1回でも作れることはわかって、あとは1つの値を固定してコンビネーション+累積和で通るなぁと思って実装したんですがサンプルが1つ合わない。そのサンプルを精査したところKが2未満の時はコーナーケースっぽいことがわかったのでそれを除いてAC。(しれっと1WA出しているのは内緒)

F
risujirohさんがわからんと言っていたので僕も見たんですがわからない。Joe先輩がひらめいて、risujirohさんと解法を共有してからACしてました。ここからチームプレイ感が高まってきます。

M
Gの次に解けそうなのがMだったので、risujirohさんにも読んでもらって相談しました。僕は全方位木DPでしかないと思ってたんですが、risujirohさんに「ここは一旦全方位木DPから離れて部分木に足したり引いたりすればできるのでは」と言われてからあぁ…なるほど…となりました。実装で複雑になりそうなところがあったのでJoe先輩に問題概要から説明することに。なんかうまく日本語がでなかったり説明が飛んでしまったりしたんですが、簡単な実装方法を教えてもらい書き始めました。書き終えるのにはそんな時間がかからなかったのですがサンプルが合わない。手計算でやっても出力結果と同じになったので、ここで解法が間違っていたことに気づきます。一瞬青ざめましたが少し修正するだけで済んだので良かったです。

O
risujirohさんがマジックナンバーが大量に入ったコードを書いててデバッグやばそうとなりましたが、すんなり通しててウケました。正確すぎる。

O，相当面倒なことをしてたっぽいなhttps://t.co/FbtyT9cJA5 pic.twitter.com/YUHBhMGsEe
— 自朗 (@risujiroh) August 31, 2019

ぱっと見てもロジックがわからなくててどうやって思いついたんだという感じです。

H
Joe先輩がsegtreeのモノイド付きpriority_queueで二分探索すればできるとか言ってて、流石にそんなヤバ問なわけがないだろうと思って読み始めたら本当にそうでした(絶望)でもJoe先輩がAdvent Calendarですごい二分平衡木を書いていたことは知っていたのでそれを使えば出来ないことはないだろうくらいに思っていたんですが、知らない間に実装完了していてそのままACしてました。すごすぎる。二分探索パートはその場で書いたと言っててそれもヤバイ。

K
あんまり通されていなかったんですが、残ったIJKLNはそもそもどの問題もAC数が少なかったので考え始めました。操作を末尾の要素を好きな要素と入れ替えてから、shiftすると言い換えられることはすぐわかって、もうちょっと考えると必要十分っぽい条件が生えました。実装はfftになりそうだし、実行時間が2.5sなのもそれっぽいなぁと思い、risujirohさんに説明した所、そもそも値が0or1なのでbitsetで行けそうとなりました。risujirohさんに実装してもらい提出した所順調にjudgeが進んでACになりました。

J
最後の1時間risujirohさんと相談していましたが解けませんでした。畳み込みっぽい式が出てきてちょっといけるかもとなりましたが、解説を読んでみるとそもそも発想が間違っていました。残念。

スタバ
慰労会の後、会場の近くのスタバでChokudai Contest 004に参加しました。マラソンはおそらく初めてなのでなにをすれば良いのかわからず、めちゃめちゃな山登りを実装していました。全くスコアが伸びなかったので上のマスから順番に貪欲したものを提出したところ128万出て、あとはマスを埋める順番を変えてみたりしたんですが改善されませんでした。かなしぃ。

感想
うまくいって楽しかったです。risujirohさん、Joe先輩、慰労会で話してくれた人たち、運営さんありがとうございました。

omochan's diary

キーエンスプログラミングコンテスト 2020