| 14:30 〜 16:00 | 研究発表 (English Session) |
|
Towards a New Era of SAT Solvers
[PDF]
Laurent Simon abstract: Since the first complete SAT solvers (DPLL-62, based on classical backtrack-search), major breakthroughs were observed in the practical – and theoretical – study of SAT. Nowadays, SAT solvers can be used in many critical systems, from very hard problems (Formal Verification, Biology, Cryptology) with potentially long runs, to more reactive applications (were a SAT solver can be called many times per second). In this talk, we will review the progresses made since the first breakthrough of 2001, with the introduction of CDCL solvers, called “modern solvers”. We will show how the field is slowly moving from a “complete” vision of Solvers to a more “uncomplete” one. We will end the talk by some open questions on the future of SAT Solvers. |
|
|
Solving Constraint Satisfaction Problems by a SAT Solver
[PDF]
Naoyuki Tamura |
|
| 16:00 〜 16:30 | 休憩 |
| 16:30 〜 18:00 | 研究発表 (English Session) |
|
DNF Hypotheses in Explanatory Induction
[PDF]
[PPT]
Katsumi Inoue |
|
|
Incremental Partition Based Consequence Finding
[PDF]
[PPTX]
Gauvain Bourgne and Katsumi Inoue |
|
|
Predicting Gene Knockout Effects by Minimal Pathway Enumeration
[PDF]
[PPTX]
Takehide Soh and Katsumi Inoue |
|
| 19:00 〜 | 夕食 |
| 10:00 〜 12:00 | 研究発表 (English Session) |
|
A Further Consideration on Equivalence of Non-monotone and Monotone Dualizatation
[PDF]
[PPT]
Yoshitaka Yamamoto |
|
|
Lagrangian Decomposition for DCOP with Complex Local Problems
[PDF]
[PPTX]
Daisuke Hatano and Katsutoshi Hirayama |
|
|
Interactive Algorithm for Multi-objective Constraint Optimization
[PDF]
[PPTX]
Tenda Okimoto, Atsushi Iwasaki and Makoto Yokoo |
|
| 12:00 〜 13:30 | 昼食 |
| 13:30 〜 14:30 | 研究発表 (English Session) |
|
Some Experiments for Restart Strategy using Propagations per Decision
[PDF]
[PPTX]
Takeru Yasumoto |
|
|
An Evaluation of QMaxSAT using MiniSat 2.2.0
[PDF]
Xuanye An |
|
| 14:30 〜 15:00 | 休憩 |
| 15:00 〜 16:30 | 研究発表 |
|
擬似ブール制約のSAT符号化を用いた重みつき部分MaxSATソルバの実現に向けて
[PDF]
本條健吾，番原睦則，田村直之 |
|
|
tデザイン構成問題の制約モデルとそのSAT符号化に向けて
[PDF]
松中春樹，番原睦則，田村直之 |
|
|
基数制約ソルバのその後の発展
[PDF]
山根 裕二 |
|
| 16:30 〜 18:00 | 次回のCSPSAT研究会についての議論 |
| 19:00 〜 | 会食 |
| 10:00 〜 10:30 | 研究発表 |
|
基数制約ソルバを用いたMaxSATについて
[PDF]
[PPTX]
鈴木祥之 |
|
| 10:30 〜 11:00 | 来年度以降のCSPSAT研究会についての議論 |
| 11:00 〜 12:00 | まとめ，閉会 |
