GlueMiniSat 2.2.5: 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー  [in Japanese] GlueMiniSat 2.2.5: A Fast SAT Solver with An Aggressive Acquiring Strategy of Glue Clauses  [in Japanese]

Access this Article

Author(s)

Abstract

命題論理の充足可能性判定問題(SAT問題)を解くソルバーは,その飛躍的な性能向上に伴い,システム検証やプランニング・スケジューリング問題,制約充足・最適化問題等の様々な分野において活躍している.GlueMiniSat 2.2.5は,単位伝搬を促し矛盾の発生を促進する学習節を積極的に獲得する戦略に基づくSATソルバーである.学習節の評価尺度には,AudemardとSimonが開発したSATソルバーGlucoseで導入されたリテラルブロック距離を改良した尺度を用い,単位伝搬を促進する学習節を獲得・保持する.また良い学習節の獲得を促すため,非常に積極的なリスタート戦略を採る.我々は代表的SATソルバーであるMiniSat 2.2を基にこれらの手法を実装し,GlueMiniSat 2.2.5を開発した.GlueMiniSat 2.2.5は充足不能性の証明に強く,SAT 2011競技会のApplication部門において逐次型ソルバーとしてUNSATクラスで1位,SAT+UNSATクラスで2位を獲得している.また並列型ソルバーを含めても同部門UNSATクラスで2位を獲得している.

The state-of-the-art SAT solvers have many successful results in the research of software and hardware verification, planning, scheduling, constraint satisfaction and optimization, and so on. GlueMiniSat 2.2.5 is a SAT solver based on literal blocks distance (LBD) proposed by Audemard and Simon which is an evaluation criteria to predict learnt clauses quality in CDCL solvers. The effectiveness of LBD was shown in their SAT solver Glucose 1.0 at SAT 2009 competition. GlueMiniSat uses a slightly modified concept of LBD, called pseudo LBD, and has an aggressive restart strategy to promote the generation of good learnt clauses. GlueMiniSat shows good performance for unsatisfiable SAT instances. In SAT 2011 competition, GlueMiniSat took the first and second places in sequential SAT solvers for UNSAT and SAT+UNSAT classes of the application category, respectively. Moreover, GlueMiniSat won the second place for UNSAT class in the category including parallel SAT solvers.

Journal

  • Computer Software

    Computer Software 29(4), 4_146-4_160, 2012

    Japan Society for Software Science and Technology

Codes

Page Top