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

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

• 批准号: 11F01743
• 负责人: 平山 勝敏
• 金额: $ 0.32万
• 依托单位: Kobe University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11F01743/
• 关键词: SAT符号化; マルチエージェント; プランニング; all-different制約; 協調経路計画問題; 配置変更問題

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

The study of SAT symbology based on all-different constraints is progressing. All-different constraints exist between SAT symbolization, normal, arbitrary, and 2 numbers. Symbolized problems exist between SAT symbolization, normal, and symbolic problems. Symbolized problems exist between SAT symbolization, normal, and symbolic problems. In this paper, we investigate the new symbolic method of structural exclusion. The result of this evaluation is that the new symbolization method is based on the SAT loss and the phase shift field is close to the UNSAT problem. The new symbolization method is based on the SAT loss and the phase shift field. On the one hand, parallel circuit design is related to coordination of circuit detection problems, such as fixed maximum circuit length, existence, non-existence, SAT failure, determination, maximum circuit length, optimal solution, and method proposal. 2. Symbolization of SAT problems A. All-different Symbolization Method A. Basic Symbolization Method B. Basic Symbolization Method C. Basic Symbolization Method D. Basic Symbolization Method D. A square, a symbol, an inverse symbol, a state, a time, a possibility, a field, a number, an introduction, a time, a time, The results of the evaluation, the symbolization of the square, the SATPLAN and the SASE are generally used to optimize the speed of the surface.

项目成果

Relocation Tasks and a Hierarchical Subclass

重定位任务和分层子类

• DOI: 10.1109/icmlc.2012.6359004
• 发表时间: 2012
• 期刊: Proceedings of the International Conference on Machine Learning and Cybernetics (ICMLC 2012)
• 作者: Tomas Balyo;Roman Bartak;Pavel Surynek;Pavel Surynek;Pavel Surynek
• 通讯作者: Pavel Surynek

Towards Optimal Cooperative Path Planning in Hard Setups through Satisfiability Solving

• DOI: 10.1007/978-3-642-32695-0_50
• 发表时间: 2012-09
• 作者: Pavel Surynek

An Alternative Eager Encoding of the All-Different Constraint over Bit-Vectors

位向量全差约束的另一种热切编码

• 发表时间: 2012
• 期刊: Proceedings of the 20th European Conference on Artificial Intelligence (ECAI 2012)
• 作者: Tomas Balyo;Roman Bartak;Pavel Surynek;Pavel Surynek
• 通讯作者: Pavel Surynek

On Improving Plan Quality via Local Enhancements

关于通过局部改进提高计划质量

• 发表时间: 2012
• 期刊: Proceedings of the 5th Annual Symposium on Combinatorial Search (SoCS 2012)
• 作者: Tomas Balyo;Roman Bartak;Pavel Surynek
• 通讯作者: Pavel Surynek

Near Optimal Cooperative Path Planning in Hard Setups through Satisfiability Solving

通过可满足性求解在硬设置中进行近乎最优的协作路径规划

• 发表时间: 2012
• 作者: Tomas Balyo;Roman Bartak;Pavel Surynek;Pavel Surynek;Pavel Surynek;Pavel Surynek;Pavel Surynek
• 通讯作者: Pavel Surynek