GlueMiniSat 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.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014)
- Martins, Ruben; Manquinho, Vasco; Lynce, In^es: Open-WBO: a modular MaxSAT solver (2014)