Hard Clique Formulas for Resolution

巨大で、信じられないほど複雑な論理規則で作られた巨大なパズルを想像してみてください。コンピュータサイエンスの世界では、これは「3-CNF論理式」と呼ばれます。これらのパズルのなかには、解くことが不可能なもの（充足不能）もあれば、あまりにも巧妙すぎて、最も強力な標準的な解法（「分解法（Resolution）」と呼ばれます）を用いても、それが不可能であることを証明するのに永遠に時間がかかってしまうものもあります。

この論文は、それら特定の、超難解な論理パズルを、別の種類のゲームである「$k$-クリーク問題」へと作り変えることについて述べています。

比喩： 「仲良しグループ」探し

$k$-クリーク問題を、パーティーゲームのようなものだと考えてみてください。あなたには、部屋の中にいる人々（頂点）がいて、誰と誰が友達であるか（エッジ）という情報があります。目標は、$k$ 人の特定のグループを見つけることです。ただし、そのグループ内の全員が、グループ内の他の全員と友達である必要があります。

• もし $k$ が小さい場合（例えば3の場合）、互いに友人である3人組を見つけるのは簡単です。
• もし $k$ が非常に大きい場合（例えば部屋の人数半分くらいの場合）、その完璧な輪を見つけることは信じられないほど困難になります。

研究者たちが成し遂げたこと

研究者たちは、「壊れた」論理パズル（解が存在しないもの）を、「仲良しグループ」のマップへと変換する方法を見つけ出しました。

1. 翻訳（変換）： 彼らは、難しい論理パズルを「パーティーのマップ」へと変換するレシピを作成しました。もし元の論理パズルが解けないものであったなら、生成されたパーティーマップには、決して完璧な $k$ 人の友人グループは存在しません。
2. 難易度： この魔法のような手法の肝は、その難易度を維持することにあります。もし元の論理パズルが、それが不可能であることを証明するために指数関数的な時間を要するほど難しかったならば、新しく作られた「仲良しグループ」のパズルもまた、不可能であることを証明するのに指数関数的な時間を要することになります。
3. 規模： これは、友人グループの人数（$k$）が、全体の人数に対して極端に少なすぎたり、あるいは不可能と言えるほど大きすぎたりしない限り、どのようなサイズに対しても機能します。

なぜこれが重要なのか（「なぜ関心を持つべきか？」の部分）

コンピュータサイエンスには、「指数時間仮説（ETH）」と呼ばれる有名な推測があります。これは基本的には、「どんなに賢いアルゴリズムを使っても、解決するのが本質的に遅い問題というものが存在する」というものです。

• 従来の方法： この論文が出る前は、「もしETHが正しいならば、これらの友人グループを見つけることは難しい」と言うことしかできませんでした。これは、ある推測が正しいという前提に基づいた条件付きの記述でした。
• 新しい方法： この論文は、特定の種類のコンピュータ証明システム（分解法）に対して、その推測を取り除きました。つまり、「私たちは推測する必要はない。これらの『友人グループ』のパズルが難しいことを、無条件に証明できる」と言っているのです。

彼らがこれを実現できたのは、コンピュータの証明システム（分解法）が、彼らが発明した翻訳の論理を辿るのに十分なほど賢いためです。コンピュータはその繋がりを「理解」できるため、手抜きをして素早く答えに辿り着くことができないのです。

大きな成果

この論文は、他の科学者たちが長い間取り組んできた問題（これまでに文献の中で少なくとも2回は言及されてきた問題）を解決しました。彼らは、未証明の理論に頼ることなく、これらの「友人グループ」のパズルがコンピュータにとって極めて困難であることを保証する、明示的で現実的な例をついに作り出したのです。

要約すると： 彼らは、「不可能な論理の謎」を「不可能な社交圏のパズル」へと変える機械を作り上げました。そして、どれほど時間を費やして探し回ったとしても、あまりに複雑すぎて見つけ出すことができない社交圏が確実に存在するのだということを、決定づけたのです。