本論文は、古典的な計画問題の表現形式である因子化タスク（Factored Tasks）をSAT（充足可能性問題）ソルバーを使って解くための新しいアプローチを提案しています。因子化タスクはSAS+を拡張した表現形式であり、選言的前提条件、条件付き効果、天使的非決定性の限定的な形式をサポートしており、STRIPS やSAS+といった従来の形式よりもコンパクトなタスク表現を実現できます。 これまで因子化タスクに対するアプローチは、主にヒューリスティック探索法に限定されていました。本研究では、因子化タスクをSATでエンコードする複数の方法を提案しており、特に因子化遷移関係を命題論理に変換する異なる戦略に焦点を当てています。研究チームは、このエンコーディング過程でさまざまなレベルの並列性をどのように活用するかを分析し、計画問題を簡略化するための一般的なタスク変換がSATベースのプランナーの性能にどのような影響を与えるかを調査しました。 この研究の意義は、SAT解法という強力な技術を計画問題に適用することで、これまでヒューリスティック探索に限定されていた因子化タスクの解法に新たな可能性をもたらす点にあります。どのエンコーディング戦略が効果的で、どのタスク変換が性能向上につながるのかを詳細に分析することで、より効率的で実用的なSATベースの計画アルゴリズムの開発に貢献します。