神戸大学附属図書館デジタルアーカイブ
https://hdl.handle.net/20.500.14094/90006800

このアイテムのアクセス数:217件（2025-04-28 17:53 集計）

閲覧可能ファイル 

ファイル フォーマット サイズ 閲覧回数 説明
90006800 (fulltext) pdf 2.11 MB 92

メタデータ

ファイル出力

メタデータID
90006800
アクセス権
open access
出版タイプ
Version of Record
タイトル
SATソルバーの最新動向と利用技術
著者
宋,剛秀 ; 番原,睦則 ; 田村,直之 ; 鍋島,英知
著者ID
A0011
研究者ID
1000000625121
KUID
https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=be19a5fd36bdbe87520e17560c007669
著者名
宋,剛秀
Soh, Takehide
ソウ, タケヒデ
所属機関名
情報基盤センター
著者ID
A1730
研究者ID
1000080290774
著者名
番原,睦則
Banbara, Mutsunori
バンバラ, ムツノリ
所属機関名
情報基盤センター
著者ID
A0899
研究者ID
1000060207248
KUID
https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=64672be7ad29e33a520e17560c007669
著者名
田村,直之
Tamura, Naoyuki
タムラ, ナオユキ
所属機関名
情報基盤センター
著者名
鍋島,英知
言語
Japanese (日本語)
収録物名
コンピュータ ソフトウェア
巻(号)
35(4)
ページ
72-92
出版者
日本ソフトウェア科学会
刊行日
2018
公開日
2020-02-27
抄録
命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは，2000年以降その性能面において飛躍的に進化した．それに伴い，解きたい問題をSAT符号化によりSAT問題へと変換し，SATソルバーを用いて解くSAT型システムが，プランニング，ソフトウェア・ハードウェア検証，スケジューリング問題など様々な分野で成功を収めるようになった．本稿では，まずSATソルバーの最新動向として，性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う．次に SAT ソルバーの利用技術の視点から，SAT ソルバーの機能面の進化と符号化技術を組み合わせることで，複雑な問題を解くことが可能になることの説明を行う．そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する．
Since 2000, SAT solvers that are programs solving SAT instances has enormously progressed in performance. Due to the performance improvement, SAT-based systems that encode problems into SAT instances and solve them by SAT solvers have succeeded in various research fields such as planning, software/hardware verification, scheduling problems, etc .In this paper, as recent advances in SAT solvers, we first explain the progress of their performance and functions from the viewpoint of the international competition of SAT solvers which is a factor of their progress. Then, from the viewpoint of utilization technologies, we explain that we can solve more complex problems by combining progressive functions of SAT solvers with encoding methods. As an example, we explain a solving method for the multiobjective optimization problems by using SAT solvers.
カテゴリ
情報基盤センター
学術雑誌論文
権利
All Rights Reserved, Copyright (C) Information Processing Society of Japan. Notice for the use of this material: The copyright of this material is retained by the Japan Society for Software Science and Technology(JSSST). This material is published on this web site with the agreement of the JSSST. Please comply with Copyright Law of Japan if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof.
ここに掲載した著作物の利用に関する注意 本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．
関連情報
DOI
https://doi.org/10.11309/jssst.35.72
NAID
130007552525　CiNiiで表示