基数制約に対応するクラスタ向け並列SATソルバとその評価

摘要

実問題から生成される構造的な問題に含まれる基数制約は，真理値のみを扱うSATソルバにとってボト ルネックとなる．そこで，基数制約を表し高速な伝播が可能な特殊節を加えた拡張CNFを提案する．標準的なSAT ソルバのMiniSat2.2の推論フェーズと衝突による学習フェーズを改訂し特殊節に対応させ，より大規模な問題を解 くために並列化を行った．評価実験として，基数制約を含む時間割作成問題をベンチマークとしてMiniSat2.2との 比較を行った．%Cardinality constraints generated from real-world problems are often a bottleneck of SAT solving. This paper proposes an extended CNF that can express cardinality constraints and allows high-performance unit propagation. We have implemented it on MiniSat 2.2 which is one of the most popular SAT solvers, by improving deduction and propagation mechanisms to handle the extended CNF. Furthermore, we have parallelized it for larger-scale CNFs. To evaluate the performance improvement over the original MiniSAT, we made an experiment on our parallel extented solver using the ITC2007 benchmark set that contains cardinality constraints problems.