SATにおける高度な制約伝播と並列マルチエージェントプラニング

SAT 中的高级约束传播和并行多智能体规划

基本信息

批准号：
11F01743
负责人：
平山勝敏
金额：
$ 0.32万
依托单位：
Kobe University
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2011
资助国家：
日本
起止时间：
2011 至 2012
项目状态：
已结题

项目摘要

SATアルゴリズムに関しては、all-different制約のSAT符号化に関する研究を進めた。all-different制約をSAT符号化する際、通常、任意の2変数間にdifferent制約が存在するものとして符号化することが一般的だが、その場合、符号化後の問題が対称構造をもつことになり、特にUNSATな問題例に対してSATアルゴリズムの性能が著しく劣化することが分かっている。そこで本研究では、順序付けされた補助変数を利用することにより対称構造を排除できる新しい符号化方法を考案した。実験で評価した結果、新しい符号化法に基づくSATアルゴリズムは、相転移領域付近のUNSATな問題例に対して従来の符号化法に基づくSATアルゴリズムよりも効率的に動作することが分かった。一方,並列マルチエージェントプランニングに関しては、協調経路発見問題において、ある固定した最大経路長をもつプランが存在するか否かをSATアルゴリズムで判定し、これを、最大経路長を変えながら最適解を求めるという方法を提案した。また、SAT問題として記述する際に、2つの符号化法を提案した。一つはall-different符号化法とよばれ、その基本アイデアは、あるエージェントがある時刻において取り得る可能な状態を値域とする変数を導入するというものである。一方、もう一つの符号化法はinverse符号化法とよばれ、ある状態のある時刻においてそれを占める可能なエージェントを値域とする変数を導入するというものである。実験で評価した結果、両方の符号化法とも、SATPLANやSASEのような汎用プランナーよりもサイズおよび速度の面で優れていることが分かった。

关于SAT算法，我们对所有不同约束下的SAT编码进行了研究。当 SAT 对所有不同的约束进行编码时，通常将它们编码为任意两个变量之间存在不同的约束，但在这种情况下，编码后的问题具有对称结构，众所周知，SAT 算法的性能会恶化。显着，特别是对于 UNSAT 问题示例。因此，在本研究中，我们设计了一种新的编码方法，可以通过使用有序辅助变量来消除对称结构。实验评估结果发现，对于相变区域附近的 UNSAT 问题实例，基于新编码方法的 SAT 算法比基于传统编码方法的 SAT 算法效率更高。另一方面，对于并行多智能体规划，在协作路径发现问题中，利用SAT算法判断是否存在固定最大路径长度的规划，然后在改变最大路径长度的同时找到最优解提出了一个方法。当将其描述为 SAT 问题时，我们还提出了两种编码方法。一种称为全异编码方法，其基本思想是引入一个变量，其范围是某个智能体在某个时刻可能采取的状态。另一方面，另一种编码方法称为逆编码方法，它引入一个变量，其范围是在某个时间占据某个状态的可能代理。实验评估表明，两种编码方法在大小和速度方面均优于 SATPLAN 和 SASE 等通用规划器。