計量時相回答セットプログラミングの実装

TL;DR（結論）

• 回答セットプログラミング（ASP）において、期間や締め切りといった定量的な時間制約を扱う際、時間の精度を上げると接地（グラウンディング）の負荷が爆発的に増大する問題がありました。
• 本研究では、差分制約という簡略化された線形制約を導入して時間処理を外部化することで、時間の粒度に依存しないスケーラブルな計算手法を提案し、その論理的な正当性を証明しました。
• 具体的には、メトリック論理プログラムを通常の論理プログラムや差分制約付きプログラムへ変換する二つの翻訳手法を開発し、時間の最大値や精度に関わらず、プログラムの規模をトレースの長さに比例する範囲に抑えることを可能にしました。

なぜこの問題か

回答セットプログラミング（ASP）は、複雑な制約充足問題を解くための強力な宣言型プログラミングの枠組みですが、時間的な要素、特に「何分かかるか」や「いつまでに終えるか」といった定量的な制約を扱う際に大きな課題に直面します。従来のASPでは、時間を離散的なステップとして扱い、各ステップに対して論理的な状態を割り当てる手法が一般的でした。しかし、このアプローチでは、時間の精度（粒度）を細かくすればするほど、生成されるルールや事実の数が膨大になる「接地のボトルネック（grounding bottleneck）」が発生します。例えば、1分単位のスケジュールを1秒単位に変更するだけで、処理すべきデータ量が指数関数的に増加し、計算が実用的な時間内に終わらなくなってしまいます。 具体的な例として、論文内で挙げられている「歯科医院のシナリオ」を考えます。主人公のラムはオフィスにいて、1時間後に歯科医院の予約がありますが、自宅にある保険証とATMで下ろす現金が必要です。オフィスからATMまで20分、自宅からオフィスまで15分といった具体的な移動時間が設定されている場合、これらの数値を正確に計算に組み込む必要があります。…

核心：何を提案したのか

本研究の核心的な提案は、メトリックASPを「差分制約（difference constraints）」と呼ばれる形式と組み合わせることで、時間に関連する数値処理を論理エンジンの外部で処理する手法です。これにより、メトリック論理プログラムの論理構造を時間の粒度から完全に切り離す（デカップリングする）ことに成功しました。具体的には、メトリック論理プログラムを、既存のソルバーで処理可能な形式に変換するための二つの主要な翻訳手法を提案しています。 第一の翻訳手法は、時間をブール原子として表現する標準的なアプローチです。これは理解しやすい一方で、時間の範囲や精度に応じてプログラムの規模が拡大するという従来の欠点を抱えています。これに対し、本研究の主要な貢献である第二の翻訳手法は、整数変数と差分制約を利用して時間を直接表現します。…

続きはログイン/プランで閲覧できます。