二階命題論理の存在量化子を全称量化子で書き換える

TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが… Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply…

ARC152D Halftree

D - Halftree意外とこの解き方している人が少ないように見えたので。例えば入力が7 3の場合は (0,1)(1,2)(2,3) と辺を張れば0~6の線グラフが得られることが分かると思います。 9 3の場合は頂点7, 8が残ってしまいますが、(7,5)と辺を張ることで、線グラフ+α…

2023年の振り返りと2024年目標

修士を修了 特に問題なく、スムーズに卒業できたし、得られた結果も個人的には満足できるものでした。国際会議(といっても査読がすごく厳しいところではない)に出したり、arXivに投稿したりして、当時の自分はそれでいっぱいいっぱいになっていたけど、今見…

yukicoder: No.1062 素敵なスコア

https://yukicoder.me/problems/no/1062 とします。 以下の要素を黒丸、よりも大きい要素を白丸で表すことにすると以下のような状況になります。 このうち操作を行った後も同じ要素になるindexは以下の黒枠で囲った部分になります。 このように両方でswapさ…

Codeforces Round #616 (Div. 1)

https://codeforces.com/contest/1290ダメダメだったため、撤退…あとでちゃんと復習します。A 勘違いして変な条件で考えてしまいました…詰めるのもめちゃくちゃ遅かった。例によって条件を整理しきらずに紙に頼ってしまった。B adhocだと思えば解けたかもし…

AOJ2445: MinimumCostPath

http://judge.u-aizu.ac.jp/onlinejudge/description.jsp?id=2445N N>=400の時は、 左下、右上の100x100領域に注目します。 (0,0)->(左下の領域)->(真ん中の領域)->(右上の領域)->(N-1,N-1)と移動していくことになりますが、 真ん中の領域では必ず右または上…

AOJ2327: Sky Jump

http://judge.u-aizu.ac.jp/onlinejudge/description.jsp?id=2327すげえ〜〜〜〜〜x座標がXに到達した時のYの最大値と最小値を求めてしまえば、そこの間の値はtを連続的に動かすことにより取ることができるのでYes or Noの判定が出来ます。最小値はロケット…

DISCO presents ディスカバリーチャンネル コードコンテスト2020 本戦C: Smaller-Suffix-Free Sequences

https://atcoder.jp/contests/ddcc2020-final/tasks/ddcc2020_final_c本番はさんざんでしたが…良問です。実はiにおける答えはiS[j...N]を満たす最小のindexです。つまり、suffix array順でiがjの後に来るものを 見れば良いです。O(NlogN)となります。証明はe…

ABC128F: Frog Jump

https://atcoder.jp/contests/abc128/tasks/abc128_f超良問。A-B=Cとして場合分けします。(i)(N-1)%C != 0のとき 0, C, 2C, 3C, ..., kC N - 1, N - 1 - C, N - 1 - 2C, N - 1 - 3C, ..., N - 1 - kCと取ることができます。(ii)(N-1)%C==0のとき (i)とだいた…

yukicoder contest 234

https://yukicoder.me/contests/247実装重い~~~~A 偶数でYesを出力しそうになった…B N変数でN個の線形独立な式があるので求められます。対称なので全部足せば良いです。C これ4方向に行けると勘違いして時間を溶かした…dpの更新式が決まります。無駄にdijkst…

Codeforces Round #614 (Div. 1)

https://codeforces.com/contest/1292A 点を共有するおじゃまマスが存在してはいけません。隣接している箇所の個数のみを保持すればいいです。B まずどっかの点に行ってから上or下に順番に取っていくのが最適です。点を全列挙する際にオーバーフロー に注意…

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

https://atcoder.jp/contests/keyence2020A v = max(H, W)として、ceil(N/v)です。B 区間スケジューリング。典型とは言え200はビビりました。C 基本K個のSとN-K個のS+1で良いんですが、S=10^9の時だけN-K個の数を1にします。ギャグ。D 個人的には解きやすか…

KUPC2019

ちょっと気になった問題取り上げます。https://atcoder.jp/contests/kupc2019/tasks/kupc2019_e木ごとにgrundyするのかなと思ったんですが、ゲームが分割されているわけではないので今回では あんまり役に立たないです。木ごとに単なる勝ち負けを求めても、…

初手累積和

数列{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…

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

https://atcoder.jp/contests/dwacon6th-prelimsうーんA 後から見ていけばいいです。B 400はすぐわかったんで実装して後はOEIS入れればわかるやろwってなったのでやったんですがsampleが全然合わない。 愚直も書いたんですがそれもバグらせて散々でした。 解…

Educational Codeforces Round 80 (Rated for Div. 2)

https://codeforces.com/contest/1288突然ですがblog再開です。A 凸なので解が小さくなり始めたらbreakすれば良いんですが条件を若干間違えてWA... コンテスト後100000までやるってのを見て賢いと思いました。B bの桁数を固定してしまえばbは9999....のよう…

SAT Solver作ってみた

この記事はhttps://adventar.org/calendars/4520の22日目の記事として書かれました。昨日はRisebbitさんのシークエント計算の自動証明を実装してみたでした。 夏休みなんかノリでSAT Solverを作ったんで、大変だったところとか書いておきます。 SATとは? 論…

TTPC2019参加記

東京工業大学プログラミングコンテスト2019 - AtCoderrisujirohさんJoe先輩とチームを組んで5位(オンサイト2位)でした。最初はrisujirohさんとの2人チームだったんですが、僕がJSC2019の予選で橙から黄に転落したことで、3人でチームを組めることに。会場で…

EDPC Y

https://atcoder.jp/contests/dp/tasks/dp_y座標をpairに格納してソートしたものをPとする。訪れるマスのPのindexをa_1 a_2->a_3->...->a_mの順番でしか訪問できない。なので、最後に訪れる場所で場合分けできて包除できる。 包除の問題で集合ではなく個数で…

SRM700Med

https://community.topcoder.com/stat?c=problem_statement&pm=14266完全に知っているかどうかの問題ですが…問題文がややこしいが、{1,2,...,n}から{1,2,...,n}への関数fを無限回適用したものをgとして、g(1),g(2),...,g(n)がk個の値を取る時のfの個数を求め…

AGC029

https://atcoder.jp/contests/agc029/tasks冷えました…A 結局はWを動かす操作です。 B 面白い。1,2,3,....2^30のグラフを考えると、明らかに木です。問題のグラフは明らかにこのグラフの部分グラフなので森です。 あとはgreedyに取っていけばいいです。ただ…

Codeforces Round #527 (Div. 3)

https://codeforces.com/contest/1092だいぶ調子良かった。A WA on test1やったw B sort C 長さN-1の文字列がほぼ答え。 D1 解いてないけど偶奇は見えた。 D2 一番短いものからやっていって、連結サイズが奇数になったらダメ。 E これとけたのいいねえ。ある…

2018-2019 Russia Open High School Programming Contest, J: Two Prefixes

https://codeforces.com/contest/1090/problem/J考察有りライブラリ使いまくりで楽しい。 まず文字数を固定します。するとTを少しずつずらした時何通り同じ文字列があるかみたいな問題になります。 こんな感じです。 Tを1文字shift S:aadaa | T: aaaaaba| 文…

SRM埋め(4)

わりとeasyうまくなってきたし、easyとmediamともに残っているセットを残しておきたいので、mediam練習します。SRM 732 mediam, hard 2問ともsurreal numberとかいう競プロではあまり馴染みのない道具を使う。知ってる人は一瞬だけど知らない人は絶対解けな…

最小全域木

この記事はhttps://adventar.org/calendars/3598の6日目の記事として書かれました。昨日の記事はsatosさんの独断と偏見による根津/本郷飯事情でした。 19erのomochana2というものです。 最小全域木を扱う際で有効な定理を紹介したいと思います。めっちゃ数学…

SRM埋め(3)

SRM 714 easy easyはこれくらいの難易度が良いよなぁ。何ターン目までに消さないといけないという条件が求まる。SRM 713 easy 難しい。保留->わかったんですけど、easyにしては実装複雑すぎでは?と思ってkmjpさんの解説記事見たら全く同じでおったまげました…

SRM埋め(2)

当分easyで鍛えます。(気分でmedときます)scoreですが目安としては 5分で満点*0.95 10分で満点*0.9 15分で満点*0.8 20分で満点*0.7 36分で満点*0.5 と覚えておけばよいでしょう。早解きは正義。SRM 730 easy 「「「「「non decreasing」」」」コードは1発で…

SRM埋め

最近のSRM無駄にconstructive多いっすね。 SRM 742 easy 1,0.5,0.25,0.125....と1,2,4,8,16....を作って適当に繋げれば良いけどバグった。 SRM 742 med kmpチックにbitdpすればいいSRM 740 easy どういうことやねんと思ったら罠が有りました… SRM 740 medium…

Dwango Programming Contest V / 第5回 ドワンゴからの挑戦状 予選

https://beta.atcoder.jp/contests/dwacon5th-prelimsアーA Nかけましょう。 B なぜかバグらせた…上からbit決めましょう。 C なんで思いつかなかったのかなぁ…ちゃんと順番決めて見ていかないからダメ。DとMの数もってしゃくとりすればいいです。 int N, Q; …

DISCO presents ディスカバリーチャンネル コードコンテスト2017 予選

https://beta.atcoder.jp/contests/ddcc2017-qual/tasks去年の予選です。ばちゃコンしました。ABはい C set D とりあえず、対称な4マスずつに分けて考えれば良いことがわかります。 すると縦に対称、横に対称、3マス塗られている、4マス塗られているの4パタ…