{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00028759","sets":["1164:2240:2247:2250"]},"path":["2250"],"owner":"1","recid":"28759","title":["SAT ソルバ MiniSat の並列化とそのチューニング手法"],"pubdate":{"attribute_name":"公開日","attribute_value":"2007-08-01"},"_buckets":{"deposit":"b78bccb3-0f89-418f-84de-8f5323cdbf62"},"_deposit":{"id":"28759","pid":{"type":"depid","value":"28759","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"SAT ソルバ MiniSat の並列化とそのチューニング手法","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"SAT ソルバ MiniSat の並列化とそのチューニング手法"},{"subitem_title":"Parallelization of SAT Solver MiniSat and the tuning technique","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"2007-08-01","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"早稲田大学大学院基幹理工学研究科情報理工学専攻"},{"subitem_text_value":"早稲田大学大学院理工学研究科情報・ネットワーク専攻"},{"subitem_text_value":"早稲田大学大学院理工学研究科情報・ネットワーク専攻　現在，特許庁"},{"subitem_text_value":"早稲田大学理工学術院"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Waseda University","subitem_text_language":"en"},{"subitem_text_value":"Waseda University","subitem_text_language":"en"},{"subitem_text_value":"Waseda University","subitem_text_language":"en"},{"subitem_text_value":"Waseda University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"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/28759/files/IPSJ-HPC07111006.pdf"},"date":[{"dateType":"Available","dateValue":"2009-08-01"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-HPC07111006.pdf","filesize":[{"value":"564.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"14"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"b45f191d-4fb3-480a-b808-1427c51711a3","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2007 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"大村, 圭"},{"creatorName":"渋谷, 健介"},{"creatorName":"稲垣, 良一"},{"creatorName":"上田, 和紀"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Kei, OHMURA","creatorNameLang":"en"},{"creatorName":"Kensuke, SHIBUYA","creatorNameLang":"en"},{"creatorName":"Ryoichi, INAGAKI","creatorNameLang":"en"},{"creatorName":"Kazunori, UEDA","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN10463942","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"本論文では、充足可能性問題（SAT）の逐次ソルバである MiniSat の lemma 共有を用いた並列化とそのチューニング手法について述べる。SAT ソルバは特定の探索域には解がないということを lemma と呼ばれる clause として学習する。この lemma は探索木の枝刈りに非常に有効であるが、全ての lemma を各 PE 間で共有するためには膨大な通信コストがかかってしまうため、効率の良い学習と通信が必要である。lemma の渡し方や各パラメタをチューニングし、24PE のクラスタで実行したところ、逐次版では解けなかった問題のうち、27 題を新たに解くことができた。","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"This paper describes parallelization of the SAT solver MiniSat based on lemma sharing and its tuning techniques. When an SAT solver finds that a specific branch of the search space does not have a solution, it learns new clauses called lemmas. Lemmas are very useful for pruning search space. However, since sharing lemmas between PEs can take enormous communication cost, developing efficient learning and communication techniques is very important. Using parameters obtained by various experiments on lemma sharing, our parallel MiniSAT solved many more SAT competition problems than the original MiniSAT on a PC cluster with 24 PEs.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"36","bibliographic_titles":[{"bibliographic_title":"情報処理学会研究報告ハイパフォーマンスコンピューティング（HPC）"}],"bibliographicPageStart":"31","bibliographicIssueDates":{"bibliographicIssueDate":"2007-08-01","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"80(2007-HPC-111)","bibliographicVolumeNumber":"2007"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"id":28759,"updated":"2025-01-22T17:54:11.027708+00:00","links":{},"created":"2025-01-18T22:58:47.295828+00:00"}