An Introduction to GlueMiniSat

Boolean, Propositional SAT Solvers

The development of boolean, propositional satisfiability (SAT) solvers has been an active and fluid area of research since the 1990's. Most of the contemporary SAT solvers that are efficient, and complete are still based on the now 50 year old Davis, Putnam, Logemann, Loveland (DPLL) algorithm with some unique constraint learning algorithm. Many of the new ideas in the area of conflict-driven clause learning (CDCL) solvers are implemented using the open source MiniSat solver as a starting point. There is an active MiniSat developers forum on Google groups. Given the fluid nature of the research, detailed documentation is sometimes hard to come by. This document will hopefully be of some help to users that have just recently become acquainted with the community.

About GlueMiniSat

GlueMiniSat is a boolean, propositional satisfiability (SAT) problem solver developed by Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue of the University of Yamanashi, Japan. It is a derivative work of the open source MiniSat 2.2 solver, and implements a form of the literal blocks distance (LBD) evaluation criteria to predict the quality of clauses learned when conflicts are encountered in the search process.

Background Theory

The underlying concepts of literal blocks distance were first introduced in reference [1]. The authors' implementation of LBD, the Glucose 1.0 SAT solver, performed admirably by placing 2-nd at the International 2009 SAT competition in the Applications (UNSAT) category. Further information can be found at the Glucose Home Page.

GlueMiniSat uses a slightly restricted concept of LBD, called strict LBD, and a dynamic restart strategy based on local averages of the decision levels and the LBDs of learned clauses. Experimental results show that GlueMiniSat also performs very well on SAT instances that are unsatisfiable. GlueMiniSat earned 1-st place at the International 2011 SAT competition in the Applications (UNSAT) category, solving 126 of 142 problem instances. A more detailed discussion of the author's variation of LBD in GlueMiniSat can be found in reference [2].

Using GlueMiniSat

Since GlueMiniSat is based on the open source MiniSat 2.2 SAT solver, it supports all of the command line options that are supported by MiniSat 2.2. David Wheeler has written a short User Guide for MiniSat (reference [3])) that is accordingly applicable to GlueMiniSat. The document also provides a simple introduction to the boolean satisfiability problem making it useful to readers looking for a SAT tutorial.

Note that GlueMiniSat can also run as a "clone" of the MiniSat 2.2 or Glucose 1.0 SAT solvers by specifying the command line options -minisat or -glucose, respectively. A brief overview of the command line options that provide more detailed control of GlueMiniSat's implementation of LBD can be obtained by executing glueminisat with the --help-verb option.

References, Resources

  1. "Predicting learnt clauses quality in modern SAT solvers" by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009, pages 399-404, 2009. [PDF]
  2. "System description of GlueMiniSat 2.2.5" by Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue, Mar 2011. From the GlueMiniSat Home Page. [PDF]
  3. User Guide for MiniSat by David Wheeler.