Chocolate Cookie 解説 - 更新日時で差をつけろ

バレンタインの直前に思いついたので、チョコレートのパッケージに混入させてURL渡したりTwitterに投げてみたりしたんですが結局誰も解けなかった・解かなかったみたいです…難易度が高すぎただけなのか、はたまたエスパーだったのか…

CSSに関するクソクイズを出すッピ〜！！
コンリテ追試組もこれで満点٩(๑❛ᴗ❛๑)۶https://t.co/7QtobIQRuD
— ←これで合格 (@sei0o) 2018年2月20日

問題

想定解法

開発者ツールなどでページのHTMLを見てみます。
まず<div id='message'>があり、<input type='checkbox'> が7x7のマスを構成しています。
その後に<span> が大量に配置されています。そしてその間に{が１つ配置されています。
checkboxをオンにすると色が濃くなってチョコチップっぽくなります。
適当にオンオフしていくと下の文字が変化したりしなかったりします。

しかし、ここには<script>が見当たりません。どのようにして<span>の文字を変えているのでしょうか？また、Here's a chocolate cookie...という文字列もHTMLファイルには記述されていません。どこから来ているのでしょうか？

ページタイトルに「CSS: Chocolate Sugoku Suki」とあることですし、CSSを見てみましょう。
style.cssとrules.cssを読み込んでいるようです。

まずは前者から。先頭にいきなりFLAGの形式が書かれています。FLAG{s.........}ですね。
<div id='message'>の内容もここから来ています。
CSSは--name: valueの形で変数を作ることができます。他のプロパティで参照するときはvar(--name)のようにして参照します。#0099ffなどだいたい何でも入れられます。

:root {
  --message: "Here's a chocolate cookie for you, find FLAG" /* FLAG{s.................} */ "!";
  --cacao: "C";
  --ushio: "h";
  --banana: "1";
}
 
...
 
#message::after {
  content: var(--message); 
}

続きを見てみましょう。

span:first-of-type::after {
  content: counter(f, upper-alpha);
}
 
span:first-of-type+*::after {
  content: counter(v, upper-alpha);
}
 
span:first-of-type+*+*::after {
  content: counter(j, upper-alpha);
}
 
span:first-of-type+*+*+*::after {
  content: counter(y, upper-alpha);
}
 
...
 
span:first-of-type+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*::after {
  content: counter(e, lower-alpha) var(--banana);
}
 
...
 
span:first-of-type+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*::after {
  content: '}';
}

span:first-of-typeでページ内の一番最初の<span>を選択し、隣接セレクタ+とユニバーサルセレクタ*を組み合わせて次の要素を取っています。
span:first-of-typeなら1番目、span:first-of-type+*なら2番目、span:first-of-type+*+*なら3番目…という感じです。
そしてそれの::after疑似要素・contentプロパティを使って何らかの文字を表示しています。実際に表示される文字はここで決定されるようです。

通常はcontent: "new!";のように文字列を使用することが多いですが、ここではcounter()を用いています。カウンタは、主に<li>でリスト表記をするときに番号を自動で割り振るために使われるものです。MDNが詳しいです。
デモも置いておきます。

たとえば１番目ではfカウンタの数値をupper-alpha、つまりアルファベットの大文字にして表示しています。何も指定しない場合は数字が出力されます。
途中でvar()を使ってはじめに定義した変数を表示している部分もあります。

これらを読んでいくと、<span>で表示されるそれぞれの文字は以下のカウンタの値と固定値で出来上がることになります。'で囲っているのが固定値です。

f v j y '{'(spanの間) g q(数値) h n l k(数値) c 'h'(--ushio) i o r 'C'(--cacao) p t d e '1'(--banana) s u(数値) '}'

fvjy{g.....}のカウンタの値を先程のFLAG{s......}と対応させることができればFLAGがわかるということです。

ゴールがわかったので、次にrules.cssを見てみましょう。
似たようなコードが繰り返されています。

input:nth-of-type(3):checked ~
input:nth-of-type(8):not(:checked) ~
input:nth-of-type(34):checked {
  counter-increment: h 3 g 1 r 3 f 1 k 2;
}
 
...

input:nth-of-type(N)でN番目のcheckboxを選択し、それぞれがON(:checked)かOFFかでスタイル（もはやスタイルではない）を適用するか決めています。
~はその要素以降の兄弟要素に対して適用されます。

この場合だと、「ONになっている3番目のcheckbox」の後ろに「OFFになっている8番目のcheckbox」があり、さらに後に「ONになっている34番目のcheckbox」がある場合に適用されます。
つまり、「3番目がON」かつ「8番目がOFF」かつ「34番目がON」ならば適用するという意味だとわかります（以降これをルールと呼びます）。

counter-incrementはその名の通りカウンタをインクリメントするのですが、後ろに数値を指定することで増加数を自由に変えられます。ここではh += 3, g += 1, r += 3, f += 1, k += 2という感じです（カウンタの中身はあくまで数値で、表示するときにアルファベットにしているだけです）。
試しに問題ページで3,8,34番目を操作してみると変化がわかりやすいと思います。

このrules.cssのすべてのルールに合うようにすればFLAGが出てくるのでしょうか？

…答えはNOです。
もういくつか見てみると以下のinput:nth-of-type(2)のように、互いに矛盾しているルールがあります。FLAG{sという文字列にするために使うルールと使わないルールがあり、その組み合わせを求める必要があります。

input:nth-of-type(2):not(:checked) ~
input:nth-of-type(39):checked ~
input:nth-of-type(44):not(:checked) {
  counter-increment: n 3 s 3 f 1 d 3;
}
 
input:nth-of-type(2):checked ~
input:nth-of-type(6):checked ~
input:nth-of-type(16):not(:checked) {
  counter-increment: p 2 f 1 k 2 j 3;
}

でもどうやって求めるのでしょうか？
全探索？ O(2⁴⁹) = 562949953421312通りなので厳しいですね。

制約充足問題 で検索してみましょう！ wikipediaを引用します。

制約充足問題（せいやくじゅうそくもんだい、英: Constraint satisfaction problem, CSP）は、複数の制約条件を満たすオブジェクトや状態を見つけるという数学の問題を指す

これの例としてよく挙げられるのは数独です。それぞれのマスを変数として、「ヨコの行・タテの列・3x3の正方形に1~9を1回ずつしか使えない」という制約を満たすような数字の入れ方を求める制約充足問題になります。
この数字を求める、つまり問題を解いてくれるスゴイものがSAT/SMTソルバと呼ばれるものです。
代表的なSATソルバにminisatがあります。SAT ソルバー入門がわかりやすいのでおすすめです。

ただ、SATソルバでは真偽の制約（aがtrue, bがfalse, かつcがfalse…）しか扱えないので直接扱うには大変な場合があります。対してSMTソルバは内部でSATソルバを呼び出しますが、整数の大小・「AならばB」などを制約として扱う構文を備えているのでSATよりもシンプルに書くことができます。
パズルをSugar制約ソルバーで解くも見てみると雰囲気がつかめると思います。

さて、それではこの問題にはどのような制約があるでしょうか？

３つすべてのcheckboxが条件を満たしてはじめて、ルールが有効になり、それに応じてそれぞれのカウンタに加算する
- 逆に、「ルールを使わないときは加算しない」「ルールで指定されていないカウンタには加算しない」（見落としがちです）
f v j y gカウンタの値はそれぞれF L A G sに対応する数値になる

この2つです。
1番目の制約は、たとえば以下のルールがあったとき

 input:nth-of-type(2):not(:checked) ~
 input:nth-of-type(39):checked ~
 input:nth-of-type(44):not(:checked) {
   counter-increment: n 3 s 3 f 1 d 3;
 }

このように変換できます（擬似コードです）。

rule_satisfied ← not(input[2]) and input[39] and not(input[44])
if rule_satisfied then n += 3, s += 3, f += 1, d += 3, (それ以外) += 0
if not rule_satisfied then (すべてのカウンタ) += 0

…と言いたいところですが、SMTソルバはtrue/falseで表現される制約を解くためのものなので、n += 3のように「変数に逐次値を足していってから比較する」ということができません。私もここで詰まり2日ほど考えた末「あとから全部まとめて和をとって比較する」ようにすればうまくいくことに気づきました。

具体的には以下のようにルールごとの増分を記録する配列を作り、制約をかけます（普通の代入とそっくりです）。

rule_satisfied ← not(input[2]) and input[39] and not(input[44])
if rule_satisfied then
  table[rule1][n] == 3, table[rule1][s] == 3, table[rule1][f] == 1, table[rule1][d] == 3,
  table[rule1][それ以外] == 0
if not rule_satisfied then table[rule1][すべてのカウンタ] == 0

そして、これを用いれば2番目の制約が表現できます。fカウンタの値はそれぞれのルールでの増分の和になるので、table[rule1][f] + table[rule2][f] + table[rule3][f] ... table[ruleN][f]として表現できます。

table[rule1][f] + table[rule2][f] + table[rule3][f] ... table[ruleN][f] == 'F'
table[rule1][v] + table[rule2][v] + table[rule3][v] ... table[ruleN][v] == 'L'
table[rule1][j] + table[rule2][j] + table[rule3][j] ... table[ruleN][j] == 'A'
table[rule1][y] + table[rule2][y] + table[rule3][y] ... table[ruleN][y] == 'G'
table[rule1][g] + table[rule2][g] + table[rule3][g] ... table[ruleN][g] == 's'

あとはこの2つをプログラムに落とし込むだけです！
私はz3というSMTソルバを使って解きました。GitHubにRubyでのコード例を載せています（あんまりきれいじゃないね…）。

実行するとFLAG{sという文字が現れるようなルールの組み合わせと、それらを満たすcheckboxのオンオフ、計算されたFLAGが出力されます。
実際のページでやってみると…うまくできました！ FLAG{s0rry4Ch3apCh0co1at3}がFLAGです。

その他

最初のバージョンではルールの数が20しかなく、O(2²⁰)で組み合わせるルールの全探索が可能でした
ルールを増やしたところ解が複数になってしまい削減できなかったため苦肉の策としてFLAGの１文字目を指定しました
- これのせいで全探索の計算量減っちゃうかも？誰かおしえて
Xmas Contest 2017 I問題を解くために調べているときに思いつきました
CSSはチューリング完全