05月12日(Mon) 15:20〜17:00 D会場(48人-ひめぎんホール 第3会議室)
| 演題番号 | 1D4-OS-11a-4 |
|---|---|
| 題目 | 基数制約のSAT符号化を用いたMaxSATソルバーの試作 |
| 著者 | 越村 三幸(九州大学大学院システム情報科学研究院情報学部門) 有村 寿高(九州大学工学部電気情報工学科) |
| 時間 | 05月12日(Mon) 16:30〜16:45 |
| 概要 | 重み付きMaxSAT問題を解くQwMaxSATの実装法とその評価を述べる． QwMaxSATは重み無しMaxSAT問題用のQMaxSATを拡張したもので， 基数制約のSAT符号化とSATソルバーを組合わせて実装されている． 重み付きMaxSAT問題では，巨大基数を扱うのでそのSAT符号化も巨大になる． 幾つかのSAT符号化による比較実験により，問題に適した符号化を明らかにする． |
| 論文 | PDFファイル |