OverviewGlueMiniSat 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 at the latest SAT competition. GlueMiniSat uses a slightly restricted concept of LBD, called strict LBD, and a dynamic restart strategy based on local averages of decision levels and LBDs of learnt clauses. Download- GlueMiniSat 2.2.10-193 introduced in the following paper:
- Nabeshima H., Inoue K. (2017) Coverage-Based Clause Reduction Heuristics for CDCL Solvers. In: Gaspers S., Walsh T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science, vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_9
- GlueMiniSat 2.2.10-81 (submitted to the SAT 2016 Competition, System description)
- GlueMiniSat 2.2.10, GlueMiniSat 2.2.10-5 (submitted to the SAT Race 2015, System description)
- GlueMiniSat 2.2.8 (submitted to the SAT 2014 Competition, System description)
- GlueMiniSat 2.2.7 (submitted to the SAT 2013 Competition, System description)
- GlueMiniSat 2.2.5 (submitted to the SAT 2011 Competition, System description)
|
|
