Study of SAT-based constraint optimization problem solving and its parallel distributed processing

基于SAT的约束优化问题求解及其并行分布式处理研究

• 批准号: 20240003
• 负责人: TAMURA Naoyuki
• 金额: $ 30.37万
• 依托单位: Kobe University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20240003/
• 关键词: SAT; 制約最適化問題; 並列処理・分散処理; 計算機システム

We conducted the research on SAT technologies for Constraint Satisfaction and Optimization Problems and their parallel/distributed implementations, and published 105 refereed papers and made 67 presentations. In addition, world's leading softwares were developed including a SAT-based CSP/COP solver Sugar which won at the 2008 and 2009 CSP Solver Competitions in global constraint categories, a CDCL type SAT solver GlueMiniSat which won at the 2011 SAT Competition in Applications UNSAT category, and a partial Max-SAT solver QMaxSAT which won at the 2010 and 2011 Max-SAT evaluation in Application category.

我们开展了约束满足和优化问题的SAT技术及其并行/分布式实现的研究，发表了105篇参考论文，并进行了67次演讲。此外，还开发了世界领先的软件，包括在2008年和2009年CSP Solver Competition中获得全球约束类别冠军的基于SAT的CSP/COP求解器Sugar，在2011年SAT Competition中获得应用UNSAT类别冠军的CDCL型SAT求解器GARM-MiniSat，部分Max-SAT求解器QMaxSAT在2010年和2011年Max-SAT应用类别评估中获胜。

项目成果

Characterizing false-name-proof allocation rules in combinatorial auctions

• DOI: 10.1145/1558013.1558049
• 发表时间: 2009-05
• 作者: Taiki Todo;Atsushi Iwasaki;M. Yokoo;Y. Sakurai

人工知能学会全国大会プログラム自助作成ツールの開発

为日本人工智能学会全国会议开发自助创作工具

• 发表时间: 2008
• 作者: Bei Yu;Sheqin Dong;Song Chen;Satoshi Goto;西村直史
• 通讯作者: 西村直史

組合せオークションのための架空名義操作不可能なメカニズムの特性

组合拍卖的虚构非操纵机制的特征

• 发表时间: 2008
• 作者: Kishi;K.;van Vugt;M.A.;Okamoto;K.-I.;Hayashi;Y.;Yaffe;M.B.;M. Nomura;東藤大樹
• 通讯作者: 東藤大樹

SAT変換に基づく制約ソルバーSugar

基于SAT变换的约束求解器Sugar

• 发表时间: 2009
• 作者: V. Ramamoorthy;M-Calin. Silaghi;T.Matsui;K.Hirayama;M. Yokoo;番原睦則
• 通讯作者: 番原睦則

論理プログラミングから解集合プログラミングへ

从逻辑编程到解集编程

• 发表时间: 2008
• 期刊: コンピュータソフトウェア Vol. 25, No. 3
• 作者: 嶋田倫博;吉川雄一郎;浅田真奈;石黒浩;才脇直樹;井上克巳
• 通讯作者: 井上克巳