Research and Development of a New SAT Solving Technologies for Constraint Satisfaction Problems

约束满足问题新型SAT求解技术的研究与开发

• 批准号: 22K11973
• 负责人: 田村 直之
• 金额: $ 2.66万
• 依托单位: Kobe University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11973/
• 关键词: 制約充足問題; 制約プログラミング; 制約ソルバー; SAT技術; SATソルバー; 充足可能性問題

本研究の目的は，制約充足問題に対する新しいSAT解法技術を研究開発し，さらに開発したシステムを実用的な問題に応用し，既存技術では解けなかった問題の解決を目指すとともに研究開発した技術を評価することである．研究遂行のため(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマを設定し，研究開発を分担して進めている．(WG1)では，研究代表者らが考案した順序符号化を用いて整数係数を持つ線形制約をSAT符号化した場合に，どのような変数順序で符号化アルゴリズムを実行すると良いかについて実験を行い，結果を評価した．また，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法について検討を進めた．(WG2)では，ベースとなるSAT型制約ソルバーFun-sCOPで2022年XCSP3競技会 (http://xcsp.org/competitions/)に参加し，Main CSPトラックで準優勝という結果を得た．(WG3)では，システム生物学の分野で用いられている非同期多値ネットワークの解析を行うためのSAT型手法を考案し，そのシステムを開発した(雑誌論文1)．具体的には，非同期オートマタネットワークとして表現されている遺伝子ネットワークについて，そのアトラクターをSATソルバーを利用して発見することにより，元の遺伝子ネットワークの定性的な分析を可能にした．次に，複数の車種からなる車を製造する場合に，全体の平均燃費がCAFE規制値を満たす範囲内で総販売予想金額を最大にする組み合わせを探索するための手法を考案し，ASPソルバーを用いたシステムを開発した(雑誌論文2)．さらに，グラフの支配集合や独立集合をSAT型手法で効率良く求める方法について研究を行い結果を学会で発表した．

The purpose of this study is to research and develop new SAT solution technologies for constraint problems, and to evaluate the application of existing technologies to solve these problems. (WG1) SAT Symbolization Method Research Development,(WG2) SAT Type Restriction Method Research Development,(WG3) Application Evaluation Method 3 Research Development Method Setting, Research Development Sharing. (WG1)In this paper, the author studies the representative of the case, the order of symbolization, the integer coefficient, the linear constraint, the SAT symbolization, the order of symbolization, the implementation, the results, and the evaluation.また，接头和を用いた符号化法，剰余记数法を用いた符号化法，MDDを用いた符号化法について検讨を进めた. (WG2)The 2022 XCSP3 Games (http://xcsp.org/competitions/) will be held in Beijing. (WG3)A study of SAT type techniques for the identification of different systems in biology was carried out (Paper 1). Specific, non-synchronous transmission of data, data transmission of data, data transmission of data transmission. Second, in the case of multiple types of vehicles, the average fuel cost of the whole vehicle is CAFE regulation value, the total sales amount is maximum, the combination is explored, and the method of ASP solution is developed (Paper 2). In addition, the dominant set and independent set are SAT type methods, the efficiency is good, the method is studied, the results are learned, and the expression is displayed.

项目成果

A ZDD-Based Method for Exactly Enumerating All Lower-Cost Solutions of Combinatorial Problems

基于 ZDD 的组合问题所有低成本解的精确枚举方法

• 发表时间: 2022
• 作者: Shin-Ichi Minato;Mutsunori Banbara;Takashi Horiyama;Jun Kawahara;Ichigaku Takigawa and Yutaro Yamaguchi
• 通讯作者: Ichigaku Takigawa and Yutaro Yamaguchi

解集合プログラミングを用いた独立集合遷移問題の解法に関する考察

用解集规划求解独立集转移问题的思考

• 发表时间: 2022
• 作者: 山田悠也;加藤聖人;小菅脩司;竹内頼人;番原睦則
• 通讯作者: 番原睦則

Solving Vehicle Equipment Specification Problems with Answer Set Programming

通过答案集编程解决车辆设备规格问题

• DOI: 10.1007/978-3-031-24841-2_15
• 发表时间: 2023
• 期刊: Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages (PADL 2023)
• 作者: Raito Takeuchi;Mutsunori Banbara;Naoyuki Tamura;and Torsten Schaub
• 通讯作者: and Torsten Schaub

解集合プログラミングを用いたハミルトン閉路遷移問題の解法

使用解集规划求解哈密顿循环转移问题

• 发表时间: 2023
• 作者: 平手貴大;番原睦則;井上克巳;盧暁南;鍋島英知;宋剛秀;田村直之
• 通讯作者: 田村直之

Solving Rep-tile by Computers

用计算机解决爬虫问题

• 发表时间: 2022
• 作者: Mutsunori Banbara;Kenji Hashimoto;Takashi;Horiyama;Shin-ichi Minato;Kakeru Nakamura;Masaaki Nishino;Masahiko Sakai;Ryuhei Uehara;Yushi Uno;Norihito Yasuda
• 通讯作者: Norihito Yasuda