@techreport{oai:ipsj.ixsq.nii.ac.jp:00028759,
 author = {大村, 圭 and 渋谷, 健介 and 稲垣, 良一 and 上田, 和紀 and Kei, OHMURA and Kensuke, SHIBUYA and Ryoichi, INAGAKI and Kazunori, UEDA},
 issue = {80(2007-HPC-111)},
 month = {Aug},
 note = {本論文では、充足可能性問題（SAT）の逐次ソルバである MiniSat の lemma 共有を用いた並列化とそのチューニング手法について述べる。SAT ソルバは特定の探索域には解がないということを lemma と呼ばれる clause として学習する。この lemma は探索木の枝刈りに非常に有効であるが、全ての lemma を各 PE 間で共有するためには膨大な通信コストがかかってしまうため、効率の良い学習と通信が必要である。lemma の渡し方や各パラメタをチューニングし、24PE のクラスタで実行したところ、逐次版では解けなかった問題のうち、27 題を新たに解くことができた。, 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.},
 title = {SAT ソルバ MiniSat の並列化とそのチューニング手法},
 year = {2007}
}