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

摘要

実問題から生成される構造的な問題に含まれる基数制約は，真理値のみを扱うSATソルバにとってボトルネックとなる．そこで，基数制約を表し高速な伝播が可能な特殊節を加えた拡張CNFを提案する．標準的なSATソルバのMiniSat2.2の推論フェーズと衝突による学習フェーズを改訂し特殊節に対応させ，より大規模な問題を解くために並列化を行った．評価実験として，基数制約を含む時間割作成問題をベンチマークとしてMiniSat2.2との比較を行った．