{"id":222481,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00222481","sets":["6164:6805:6807:11061"]},"path":["11061"],"owner":"44499","recid":"222481","title":["SATソルバーの使い方---問題をSATに符号化する方法---"],"pubdate":{"attribute_name":"公開日","attribute_value":"2017-01-06"},"_buckets":{"deposit":"db8fbab6-04d8-43a6-8800-177f123a6c88"},"_deposit":{"id":"222481","pid":{"type":"depid","value":"222481","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"SATソルバーの使い方---問題をSATに符号化する方法---","author_link":["583823"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"SATソルバーの使い方---問題をSATに符号化する方法---"},{"subitem_title":"How to use SAT solvers---How to encode problems to SAT---","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"SATソルバー，SAT符号化，制約モデル","subitem_subject_scheme":"Other"}]},"item_type_id":"29","publish_date":"2017-01-06","item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_29_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"神戸大学 情報基盤センター;;神戸大学 情報基盤センター;;神戸大学 情報基盤センター"}]},"item_29_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Information Science and Technology Center, Kobe University;;Information Science and Technology Center, Kobe University;;Information Science and Technology Center, Kobe University","subitem_text_language":"en"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/222481/files/IPSJ-WPRO2017023.pdf","label":"IPSJ-WPRO2017023.pdf"},"date":[{"dateType":"Available","dateValue":"2022-11-17"}],"format":"application/pdf","filename":"IPSJ-WPRO2017023.pdf","filesize":[{"value":"366.3 kB"}],"mimetype":"application/pdf","accessrole":"open_date","version_id":"a862189c-93ac-46b6-b4fe-260c3eaa757f","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2017 by the Information Processing Society of Japan"}]},"item_29_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"田村, 直之  宋 剛秀  番原 睦則","creatorNameLang":"en"},{"creatorName":"Naoyuki, Tamura  Takehide Soh  Mutsunori Banbara","creatorNameLang":"ja-Kana"}],"nameIdentifiers":[{}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_5794","resourcetype":"conference paper"}]},"item_29_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"SATソルバーは，与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである．Knuthによる著名な教科書 The Art of Computer Programming の最新分冊では，300ページ以上もの分量がSATソルバーとその応用の説明に割かれ，最近のホットなトピックの一つとなっている．このようなSATソルバーの発展を背景とし，解きたい問題をCNF式に変換(SAT符号化)しSATソルバーで解を求める手法が注目されている．しかし，解きたい問題が複雑な場合，それを直接SAT符号化することはかなり面倒な仕事だ．代わりに，まず与えられた問題を整数変数上の制約モデルとして定式化し，次にその制約モデルのSAT符号化を考える方法が有効である．そこで，本発表では上記のKnuthの教科書でも取り上げられている例題を題材とし，制約モデル・SAT符号化の選択肢について説明・比較を行い，SATソルバーをより有効に利用する方法を紹介する．","subitem_description_type":"Other"}]},"item_29_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"172","bibliographic_titles":[{}],"bibliographicPageStart":"165","bibliographicVolumeNumber":"2017"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"updated":"2025-01-19T13:44:04.716945+00:00","created":"2025-01-19T01:22:26.102366+00:00","links":{}}