Bounded Model Checkingとは何か｜探索範囲を有限に固定する
Bounded Model Checking（BMC）とは、状態遷移を深さ k まで展開し、その範囲内に望ましくない状態が存在するかをSATとして検査する手法である。全期間の安全性を証明する手続ではない。有限の探索境界を置き、その内側で反例経路を探す。
経営へ援用するときの要点は、期間・資本・試行回数・在庫量などの上限を Bound k として計算開始前に固定し、そのラウンドで何が分かったかを明確にすることである。
BMCが解く問い
BMCは次を同時に満たす割当を探す。
- 初期状態 I(s₀) が成立する
- 各ステップで遷移関係 T(sᵢ, sᵢ₊₁) が成立する
- どこかの深さ i ≤ k で違反条件 B(sᵢ) が成立する
結果の読み方は次のとおりである。
| 結果 | 意味すること | 意味しないこと |
|---|---|---|
| SAT | 深さ k 以内に反例経路がある | 事業全体が破綻している |
| UNSAT | 深さ k 以内に反例がない | 全期間の安全性が証明された |
UNSATは「いま置いた境界の内側では見つからなかった」という情報である。k を広げれば別の結果になり得る。したがって、BMCの価値は無限探索の代替ではなく、探索範囲を有限に固定して検証可能にすることにある。
なぜ有限境界が必要か
事業の状態空間は、予約、在庫、価格、人員、法令、設備の組合せで容易に爆発する。全探索で最適解を得ることは、多くの場合現実的でない。
第4章の目的は、全探索で最適解を得ることではない。有限の探索境界を置き、Conflictから再利用可能な禁止条件を学習し、外部主体が定めた充足水準で計算を止めることである。BMCはその最初の固定点を与える。
Bound k の候補には次がある。
- 日数：今後7日、30日、四半期
- 投入額：広告費、在庫投資、試作費の上限
- 試行回数：A/Bテスト、営業接触、出荷ロット数
- 在庫量：保有上限、欠品許容、安全在庫
重要なのは、探索の途中で都合よく k を伸ばさないことである。境界を変えるなら、新しい計算ラウンドとして記録する。
経営における違反条件 B
違反条件 B は「起きてほしくない状態」である。例を挙げる。
- 現金残高が下限を下回る
- 法令・安全基準を破る
- 品質のHard条件を満たさない
- 納期を固定した場合の遅延
- 顧客への約束と在庫の不一致
BMCは、これらの違反が Bound 内に到達する経路があるかを問う。経路が見つかれば、どのDecisionの列が原因かを追跡できる。見つからなければ、少なくともその Bound 内では違反経路が無い。
7日プロトコルとの関係
短期間に独立した検証機会を複数置く設計は、BMCの Bound と相性が良い。たとえば今後7日を k とし、各日で現金下限、在庫欠品、法令違反の有無を検査する。
ただし、PCP定理から「7日間」や「1/128」という事業上の数値が自動的に導かれるわけではない。各回の見逃し確率や独立性の仮定を満たさない場合、単純な掛け算は使えない。BMCが与えるのは、有限深さでの反例の有無であり、確率的検証の通過確率そのものではない。
検証項目、サンプリング方法、偽陽性・偽陰性を事前に定義したうえで、Bound 内の反例探索として使う。
組織検証への適用
FMEA（故障モード影響解析）とBMCは構造が近い。故障モードを違反条件 B として定義し、直近の k ステップで純利益の下限やサービス継続条件を下回るかを検査する。
例を挙げる。
- 「全営業が即日退職する」を故障モードとして置く
- 直近 k 日で受注・回収・サポートが下限を下回るかを BMC で見る
- 下回る経路があれば、自動フォームとAI追客など代替遷移を事前に用意する
ここでも、k 内に反例が無いことは全期間の安全証明ではない。有限境界付きの耐故障設計である。
SAT Solver実行の位置づけ
BMC単体では、反例の有無しか分からない。実務では次の手続と接続する。
- BMCで Bound を固定する
- 候補を実行し、Hard clauseとのConflictを記録する
- CDCLでConflictを再訪禁止の学習節へ変換する
- Hardを守り Soft が受入閾値へ達したら停止する
この停止は事業全体の終了ではない。局所探索ラウンドの終了である。上限までに達しなければ、そのラウンドをUNSATまたは未決として閉じ、目的・制約・Boundのどれを変更するかを外部主体が決める。
HardとSoftを分けてからBoundを置く
BMCの前に、破ってはならない条件と調整可能な条件を分ける。
| 種別 | 例 | 扱い |
|---|---|---|
| Hard clause | 法令、現金下限、安全性、品質下限 | 一度でも破れば棄却 |
| Soft clause | 納期、表現、品揃え、局所利益率 | 重み付きで最大化・緩和 |
「99%なら常に十分」という普遍閾値は存在しない。何をHardとし、どの重みと充足水準で止めるかを外部主体が宣言する。Boundだけを先に決めてHardを曖昧にすると、SAT/UNSATの解釈が崩れる。
よくある誤解
| 誤解 | 正しい理解 |
|---|---|
| UNSATなら安全が証明された | k 以内に反例が無いだけである |
| k を大きくすれば必ず良い | 計算コストが増え、停止不能になり得る |
| BMCは最適解を出す | 反例探索であり、最適性の保証ではない |
| 途中でBoundを伸ばしてよい | ラウンドを分けて記録しないと検証不能になる |
実行チェックリスト
- 期間・資本・試行回数などの Bound k を計算開始前に固定したか
- 初期状態、遷移、違反条件を明示したか
- Hard clause と Soft clause を分けたか
- SAT/UNSATの読み方を事前に合意したか
- Bound変更時に新しいラウンドとして記録したか
- 局所探索の停止条件を採用・UNSAT・未決・再起動のいずれかで閉じられるか
BMCから得られる実務上の示唆は、「すべてを長く見れば安全になる」ではない。検証可能な有限境界を置き、その内側で反例を探し、見つからなければ境界付きの知見として次のDecisionへ渡すことである。
『P vs NP経営』の詳細はこちら https://link.amazon/B04IEdYsn