GlueMiniSat 2.2.5: A Fast SAT Solver with An Aggressive Acquiring Strategy of Glue Clauses
スポンサーリンク
概要
- 論文の詳細を見る
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.
- 日本ソフトウェア科学会の論文
日本ソフトウェア科学会 | 論文
- LCDと透明弾性体の光弾性を用いたユーザインタフェース (特集 インタラクティブシステムとソフトウェア)
- Bluetoothによる位置検出
- COINSにおけるSIMD並列化(最新コンパイラ技術とCOINSによる実践)
- データ型を考慮した軽量なXML文書処理系の自動生成(ソフトウェア開発を支援する基盤技術)
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)