06月12日(Tue) 15:30〜20:00 E会場(-山口県教育会館／第四研修室(72))
| 演題番号 | 1E3-OS-4-6 |
|---|---|
| 題目 | 効率的なSMTソルバの実現を目指した等号組み合わせの削減 |
| 著者 | 福田 寿志(山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻) 岩沼 宏治(山梨大学大学院医学工学総合研究部コンピュータ・メディア工学専攻担当) 山本 泰生(山梨大学大学院医学工学総合研究部) |
| 時間 | 06月12日(Tue) 17:30〜17:50 |
| 概要 | SMTは決定可能な一階の背景理論をSAT技法に組み込む技術であり，実用問題では背景理論は通常，複数の部分理論が組み合わされた理論となる．Nelson-Oppen（NO）法はそれらの複数理論の個々の決定手続きを組み合わせる手法ではあるが，決定手続き間の矛盾を防ぐため大量の等号制約を作成する。本稿ではNO法を実装したSMTソルバを試作し，併せて等号制約の削減手法を組み込んだので，その報告を行う． |
| 論文 | PDFファイル |