Navigation

Overview

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.

Download