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

Decrypt history, Encrypt future™

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

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

イメージは任天堂のスーパーマリオブラザーズ(ファミコン版)が分かりやすい。クリボーやノコノコにぶつかってリセットされながら進み、同じ落とし穴へ戻らないように覚え、最後に旗を取る。CDCLでも同じである。一度ぶつかった失敗パターンを「同じ道を通るな」という短い禁止として覚え、次の試行ではその道を通らない。

系譜として、João P. Marques-Silva(ジョアン・P・マルケス=シルヴァ)と Karem A. Sakallah(カレム・A・サカラ)による衝突駆動の学習(1990年代後半)がある。以下では、カフェの週末出店を例に、0か1かの決定を一つずつ進めながら衝突・学習・戻りを追う。

例題:週末カフェ出店

目的は、週末のポップアップカフェを開き、現金下限を守りつつ売上を十分にすることである。決めることは四つだけとする。各変数は Yes=1、No=0 である。

変数 意味 仮の初期案
A 駅前の高い場所を借りる 1
B 限定メニューを値下げする 1
C 仕入れを通常の2倍にする 1
D チラシ広告を出す 1

破れば棄却する条件(reject条件/必須条件)を二つ置く。

  1. 現金残高 ≥ 30万円(下限)
  2. 食の安全基準を満たす(ここは常に1とする)

調整可能な条件(充足条件/希望条件)として、「週末売上 ≥ 20万円」を置く。これが受入閾値である。充足条件は破れても棄却ではないが、満たせなければ採用しない。

費用の目安を次のように置く。

選択 現金への影響
A=1(高賃料) −18万円
B=1(値下げ) 粗利が薄くなる(後述)
C=1(仕入2倍) −12万円
D=1(チラシ) −4万円
手元資金 50万円から開始

1周目:Decision と衝突

最初の Decision(仮決め)は A=B=C=D=1 とする。マリオで言えば、いつもと同じ道を全力で走る選択である。

現金の計算は次になる。

50 − 18 − 12 − 4 = 16万円

下限は30万円なので、reject条件に衝突する。これが Conflict(矛盾)である。旗の手前でクリボーに当たってリセットされた状態に近い。

ここで議事録に「なぜ失敗したか」を長く書くだけでは、次も同じ道を走りやすい。CDCLがやるのは、同じ失敗へ戻らないための短い禁止を作ることである。

分析すると、今回の現金割れに効いたのは「高賃料・仕入増・チラシ」の同時実行である。値下げ B は粗利の話で、この1周目の現金割れの主因ではない。そこで学習節として次を覚える。

学習節1:A=1 かつ C=1 かつ D=1 を禁止する(少なくとも一つは 0 にする)

以後、この三つの同時 Yes には戻らない。これが Learn(学習)である。

2周目:戻って別の道へ

Backtrack(戻り)では、「最後に触った D だけをやめる」ではなく、衝突を作った分岐まで戻る。ここでは A・C・D の同時実行を崩す。試しに D=0(チラシなし)へ戻す。

A=1, B=1, C=1, D=0

現金:50 − 18 − 12 = 20万円

まだ下限30万円を下回る。再び Conflict である。学習節を更新する。

学習節2:A=1 かつ C=1 を禁止する

チラシの有無に関係なく、高賃料と仕入2倍の同時実行が現金を割る、と分かったからである。

3周目:必然の連鎖(Unit Propagation)

次の Decision で A=1(駅前)を残し、学習節2から C は必然的に 0 になる。これが Unit Propagation(単位伝播)である。一つ決めると、禁止条件から次が自動で決まる。

A=1, C=0(仕入は通常量), D=1, B=?

現金:50 − 18 − 4 = 28万円

まだ下限30に届かない。そこで A 自体を見直す。A=0(賃料の安い場所)へ戻す。

A=0, C=1, D=1, B=1

現金:50 − 12 − 4 = 34万円

reject条件の現金下限は満たす。安全基準も満たす。ここまでが「死なずに進めた」状態である。

残るのは充足条件、つまり売上20万円を満たせるかである。安い場所でも、値下げ B=1 と仕入増 C=1 とチラシ D=1 なら来客が見込める、と置いて充足条件を満たしたとする。すると採用して停止(Halt)できる。

結果 割当 現金 判定
1周目 A=B=C=D=1 16万 reject衝突。学習節1
2周目 A=B=C=1, D=0 20万 reject衝突。学習節2
3周目 A=0, B=C=D=1 34万 reject充足。充足条件も満たし採用

この例で見えるCDCLの要点

段階 例題での意味
Decision A〜D を仮に Yes/No で決める
Unit Propagation 学習節から「A=1 なら C=0」などと必然が決まる
Conflict 現金下限などの reject条件を破る
Analyze / Learn 同じ失敗組合せを再訪禁止の短い条件にする
Backtrack 原因の分岐まで戻り、別の割当を試す
Halt reject条件を守り充足条件の閾値を満たしたら止める

重要なのは、失敗のルートを棄却し同じ落とし穴へ再度陥らない禁止条件を発見することである。マリオが「あそこのクリボーで落ちた」と覚えるのに近い。毎回ステージ1から同じ事故を繰り返さないようにする。そして現実の適用については一度決定すると後戻りするコストが高い決定もある。例えば、賃料の高い立地を借りるというアクションは後戻りコストが高い。その場合はPOPUPストアで検証する、現地を散歩して、周辺を通る顧客層をチェックするなど、より後戻りコストが低い検証を繰り返し、充足可能性を上げていく。kがなるべく少ない回数で検証を完了させられるようにするのがBMC(Bounded Model Checking)的考え方である。

経営へ応用するなら、「値下げする」「在庫を増やす」「広告費を固定する」の組合せが資金下限と衝突したとき、その組合せを再訪しない節を学習することである。これは計算量クラスの定理ではなく、手続の写像である。

SATとの関係

この例題は、結局のところ SAT(Boolean Satisfiability Problem/ブール充足可能性問題)として解けている。変数 A〜D に 0/1 を入れ、reject条件の論理条件をすべて満たす割当があるかを問う。ある場合を SAT(Satisfiable/充足可能)、無い場合を UNSAT(Unsatisfiable/充足不能)と呼ぶ。

CDCLは、その SAT を解くための代表的な手続の一つである。経営者が SAT ソルバそのものになる必要はない。目的、reject条件、充足条件の閾値、探索の上限(Bound:期間・試行回数・予算)を先に固定する外部主体であればよい。途中で目的を都合よく差し替えると、結果は検証不能になる。

Bound 内で充足条件を満たせなければ、そのラウンドは未決または UNSAT として閉じ、賃料・仕入・広告のどれを変えるかを次ラウンドで決める。事業全体の終了ではない。局所探索の終了である。

チェックリスト

  1. 失敗を、再訪禁止の短い条件へ圧縮したか
  2. その条件は短く、次の試行で使えるか
  3. reject条件(破れば棄却)と充足条件(重み付きの目標)を分けたか
  4. 目的と棄却条件を探索前に固定したか
  5. Bound → Conflict → Learn → Halt の順でラウンドを閉じたか
  6. 採用、UNSAT、未決、再起動のいずれかを明示したか

CDCLの有効性は、「失敗談を共有すれば学習になる」ことではなく、同じ失敗領域へ戻らない禁止条件への圧縮であり、有限資源の探索を検証可能な手続へ変える点にある。

『P vs NP経営』の詳細はこちら https://link.amazon/B04IEdYsn