サットプラン

Satplan (満足度としての計画としてよく知られています) は、自動化された計画手法です。計画問題インスタンスをブール満足度問題のインスタンスに変換し、 DPLL アルゴリズムやWalkSATなどの満足度を確立する方法を使用して解決します。

計画における問題インスタンスが、与えられた初期状態、与えられた一連のアクション、目標、および期間の長さとともに与えられると、与えられた期間の長さの計画がある場合にのみ式が満足できるような式が生成されます。これは、クックの定理の証明における満足可能性問題を伴うチューリング マシンのシミュレーションに似ています。異なる期間の長さに対する式の満足可能性をテストすることで、計画を見つけることができます。これを行う最も簡単な方法は、期間の長さを 0、1、2 と順番に調べていくことです。

• グラフプラン

• HA Kautz および B. Selman (1992)。満足度としての計画。第 10 回ヨーロッパ人工知能会議 (ECAI'92) の議事録、359 ～ 363 ページ。
• HA Kautz および B. Selman (1996)。限界を押し広げる: 計画、命題論理、確率的探索。第 13 回全国人工知能会議 (AAAI'96) の議事録、1194 ～ 1201 ページ。
• J. Rintanen (2009) 「計画と SAT」 A. Biere、H. van Maaren、M. Heule、Toby Walsh 編『Handbook of Satisfiability』483～504 ページ、IOS Press。