@article{oai:ipsj.ixsq.nii.ac.jp:00011221,
 author = {瀬戸, 謙修 and 藤田, 昌宏 and 浅田, 邦博 and Kenshu, Seto and Masahiro, Fujita and Kunihiro, Asada},
 issue = {5},
 journal = {情報処理学会論文誌},
 month = {May},
 note = {充足可能性判定（SAT）を利用した最適なコード生成手法を提案する．まずコード生成問題を有限状態機械（FSM）を利用して定式化する（瀬戸ほか，2002）．次にFSMを組合せ回路へと展開し（Biereほか，1999），最適コード生成問題を充足可能性判定（SAT）問題として解く．最新のSATソルバ（Moskewiczほか，2001）を使用した実験結果から，SATベースのコード生成手法がBDDベースのコード生成（瀬戸ほか，2002）よりも効果的であることが示される．, We present a method for optimal code generationbased on Boolean satisfiability (SAT).First, code generation is formulated based on a finite statemachine (FSM) (Seto, et al., 2002). Next, we unroll the FSM to a combinational circuit (Biere, et al., 1999),so that optimal code generation problem is solved as a SAT problem.Experimental results using a state-of-the-art SATsolver (Moskewicz, et al., 2001) demonstrate that SAT-based optimalcode generation is more effective than BDD-based symbolic approach (Seto, et al., 2002).},
 pages = {1202--1205},
 title = {充足可能性判定を利用した最適コード生成手法},
 volume = {44},
 year = {2003}
}