A Study of Advanced and Effective SAT Planning and Scheduling

先进有效的SAT规划与调度研究

• 批准号: 19700135
• 负责人: NABESHIMA Hidetomo
• 金额: $ 2.44万
• 依托单位: University of Yamanashi
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19700135/
• 关键词: 充足可能性問題; プランニング; スケジューリング; 分散協調

Propositional satisfiability (SAT) problems and its high performance solvers are used for solving various problems, such as planning and scheduling, which are encoded into SAT instances. Generally, SAT encoding approaches need to solve multiple SAT instances. In order to solve such multiple SAT instances, we have developed a distributed and cooperative SAT solver SatCube, which reuse lemmas, hypotheses and models during the search process and can solve multiple SAT instances efficiently. We have studied SAT planning to extend the application area based on ordered encoding, and proposed various speed-up techniques for SAT scheduling.

命题满意度（SAT）问题及其高性能求解器用于解决各种问题，例如计划和调度，这些问题已编码为SAT实例。通常，SAT编码方法需要解决多个SAT实例。为了解决这样的多个SAT实例，我们开发了一个分布式和合作的SAT求解器Satcube，该索引在搜索过程中重复使用引理，假设和模型，并且可以有效地解决多个SAT实例。我们已经研究了SAT计划，以根据有序编码扩展应用程序区域，并提出了针对SAT计划的各种加速技术。

项目成果

マルチコア環境に向けた高速並列SATソルバの開発

开发适用于多核环境的高速并行 SAT 求解器

• 发表时间: 2007
• 作者: Koichi Shinoda;Kazuki Ishihara;Sadaoki Furui and Takahiro Mochizuki;鍋島英知
• 通讯作者: 鍋島英知

並列分散型SATソルバにおける探索空間の分割手法の提案

并行分布式SAT求解器搜索空间划分方法的提出

• 发表时间: 2009
• 作者: 高見明秀;鍋島英知;岩沼宏治
• 通讯作者: 岩沼宏治

A SAT-based Method for Solving the Two-dimensional Strip Packing Problem

• DOI: 10.3233/fi-2010-314
• 发表时间: 2010-08
• 期刊: Fundam. Informaticae
• 作者: Takehide Soh;Katsumi Inoue;Naoyuki Tamura;Mutsunori Banbara;Hidetomo Nabeshima

SOLAR: An automated deduction system for consequence finding

• DOI: 10.3233/aic-2010-0465
• 发表时间: 2010-04
• 期刊: AI Commun.
• 作者: Hidetomo Nabeshima;K. Iwanuma;Katsumi Inoue;O. Ray

マルチコア環境向け並列SATソルバの開発

多核环境下并行SAT求解器的开发

• 发表时间: 2007
• 作者: 高見明秀;鍋島英知;岩沼宏治
• 通讯作者: 岩沼宏治