|
ポートフォリオ型並列SATソルバーでは異なる探索戦略を持つ複数の逐次SATソルバーを競争的に実行させることで様々なSAT問題に対して頑健な性能を達成する．さらに各逐次ソルバーが獲得した探索の枝刈り情報（学習節）を交換するとこで探索の重複を抑制し協調的に動作する．特に充足不能な問題においては，この学習節交換が性能向上のための重要な役割を果たす．
本年度はこの学習節交換戦略に焦点を当て検討を行った．並列SATソルバーでは，長さやLBD値などの学習節評価尺度に基づき交換する学習節を選別する手法が一般的である．しかしSAT問題によって獲得される学習節の長さや数，質は大きく異なるため，その基準を事前に決定することは難しい．
そこで我々は，非決定的並列SATソルバーHordeSATが採用している常に一定量のリテラルを交換する戦略について検討を行った．この戦略では，輸出したい学習節のリテラル数が基準値を上回る場合に学習節の選別基準を厳しくし，逆の場合には緩くすることでどのような問題においても常に一定量の学習節を交換することが可能になる．
この学習節交換戦略を我々が開発した決定的並列SATソルバーのための汎用フレームワークDPSに導入した．このフレームワークは逐次SATソルバーを少ない手間で並列ソルバーに拡張するものであり，新しい学習節交換戦略もフレームワークの機能として提供されるため，個々の逐次ソルバー側で実装する必要はない．このDPSに最新の逐次ソルバーであるMapleCOMSPSやKissatなどの導入も行った．我々の開発した並列SATソルバーDPS-Kissatは，決定的挙動を担保しつつもSAT2022競技会の並列トラックにおける複数部門において２位・３位に入賞する成果を収めている．
|
