05月23日(Tue) 15:50〜17:30 M会場(ウインクあいち-10F 1005会議室)
| 演題番号 | 1M2-OS-02b-5 |
|---|---|
| 題目 | CDCL SATソルバにおける貪欲論理制約伝播 |
| 著者 | 楢崎 修二(長崎大学 大学院 工学研究科) |
| 時間 | 05月23日(Tue) 17:10〜17:30 |
| 概要 | CDCLアルゴリズムは論理制約伝播を繰り返し、矛盾が起きた場合には学習節を獲得しつつ、非時間順バックトラックを実行する探索手法である。多くの高速SATソルバで用いられ、様々な高速化の研究がなされている。 本発表においては、最初の矛盾を発見しても直ちにバックトラックを起こさず、矛盾の検出を続けるという変更手法を提案する。現在我々が開発中のSATソルバに実装して行った実験結果について報告する。 |
| 論文 | PDFファイル |