Fedora 15 Update: glueminisat-2.2.5-3.fc15

[updates at fedoraproject.org]

--------------------------------------------------------------------------------
Fedora Update Notification
FEDORA-2012-7001
2012-05-01 00:21:21
--------------------------------------------------------------------------------

Name        : glueminisat
Product     : Fedora 15
Version     : 2.2.5
Release     : 3.fc15
URL         : http://glueminisat.nabelab.org/
Summary     : Boolean SAT solver that implements literal blocks distance (LBD)
Description :
GlueMiniSat is a boolean, propositional satisfiability (SAT) problem
solver. 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.

The underlying concepts of literal blocks distance were first introduced
in the paper "Predicting learnt clauses quality in modern SAT solvers"
by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009, pages
399-404, 2009. 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.

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.

GlueMiniSat supports the same command line options as MiniSat 2.2 (see the
documentation from the minisat2 package). It 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.

--------------------------------------------------------------------------------
Update Information:

Description: GlueMiniSat is a boolean, propositional satisfiability (SAT) problem solver. 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.

The underlying concepts of literal blocks distance were first introduced in the paper "Predicting learnt clauses quality in modern SAT solvers" by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009, pages 399-404, 2009. 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.

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 supports the same command line options as MiniSat 2.2 (see the documentation from the minisat2 package). It 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.
--------------------------------------------------------------------------------
References:

  [ 1 ] Bug #812681 - Review Request: glueminisat - Boolean SAT solver that implements literal blocks distance (LBD)
        https://bugzilla.redhat.com/show_bug.cgi?id=812681
--------------------------------------------------------------------------------

This update can be installed with the "yum" update program.  Use 
su -c 'yum update glueminisat' at the command line.
For more information, refer to "Managing Software with yum",
available at http://docs.fedoraproject.org/yum/.

All packages are signed with the Fedora Project GPG key.  More details on the
GPG keys used by the Fedora Project can be found at
https://fedoraproject.org/keys
--------------------------------------------------------------------------------