CONTENTS

Decrypt history, Encrypt future™

公理とは何か|証明の前提を選ぶ操作

公理とは、絶対的な真理そのものではなく、命題を宣言し証明するための前提条件の集合である。数学の歴史は、最も少ない記号で最も広範な概念を説明する試みだと定義すると、公理は最小のツールキットで最大の説明をするための関係性のセ…
Read more

コルモゴロフ複雑性とは何か|最短記述としての既約さ

コルモゴロフ複雑性(Kolmogorov Complexity)とは、対象を出力する最短プログラムの長さである。記述が短いほど、その対象は既約に近い。冗長な合成は、より短い生成手続へ分解できる。 名称は Andrey N…
Read more

coNPとは何か|Noであることの短い証拠

coNPとは、「属さない(Noである)」ことを短い証拠で多項式時間検証できる問題のクラスである。形式的には、補集合がNPに属するとき、元のクラスはcoNPに入る。 NPがYesの短い証明書を扱うのに対し、coNPはNoの…
Read more

2-SATとは何か|2点間の矛盾発見を多項式時間で検証する

2-SATとは、各節が2個以下のリテラルからなるCNF(Conjunctive Normal Form/連言標準形)の充足可能性問題である。Implication Graph(含意グラフ)と強連結成分(SCC/Stron…
Read more

Satisficingとは何か|最適解ではなく充足水準で止める

Satisficing(満足化)とは、最適解を探し続けるのではなく、外部主体が定めた充足水準を満たした時点で計算を止める意思決定の枠組みである。Herbert A. Simon(ハーバート・A・サイモン、1916–200…
Read more

CDCLとは何か|失敗を再訪禁止の学習節へ変換する

CDCL(Conflict-Driven Clause Learning/衝突駆動型節学習)とは、候補を仮に決め、そこから必然的に決まる割当を進め、矛盾したら原因を短い禁止条件(学習節)にまとめ、戻って別の候補を試す、と…
Read more

Bounded Model Checkingとは何か|探索範囲を有限に固定する

Bounded Model Checking(BMC/有界モデル検査)とは、未来を無限に調べるのではなく、先の k ステップまでに区切って、『まずい状態にたどり着く道があるか』を調べる手法である。全部の未来について安全だ…
Read more

3-SATとは何か|事業の制約を変数と節で構造化する

3-SATとは、各節がちょうど3個のリテラルからなる連言標準形(CNF/Conjunctive Normal Form)の充足可能性問題である。与えられた論理式を真にする真偽割当が存在するかを問う。CNFは「節(OR)の…
Read more

ナノメートルセンサーの限界|ロボットと人間はどこまで細かく観測できるか

ナノメートルセンサーの限界を考えるとき、最初に分けるべきなのは、装置の部品をどこまで小さく作れるかと、散乱やスペクトルからどこまで小さな構造を推定できるかである。 原子より小さな構造を調べる実験は存在する。しかしそれは、…
Read more

粗視化とは何か|巨大な状態空間を目的に合わせて圧縮する

粗視化(coarse-graining)とは、世界のすべてを同じ細かさで扱うのではなく、目的に必要な違いだけを残して状態をまとめることである。経営へ応用するなら、追跡する状態変数を目的に合わせて間引く手続である。 情報を…
Read more