[Bug 812681] New: Review Request: GlueMiniSat - Boolean SAT solver that implements literal blocks distance (LBD)

[bugzilla@xxxxxxxxxx]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.

Summary: Review Request: GlueMiniSat - Boolean SAT solver that implements literal blocks distance (LBD)

https://bugzilla.redhat.com/show_bug.cgi?id=812681

           Summary: Review Request: GlueMiniSat - Boolean SAT solver that
                    implements literal blocks distance (LBD)
           Product: Fedora
           Version: rawhide
          Platform: All
        OS/Version: Linux
            Status: NEW
          Severity: medium
          Priority: unspecified
         Component: Package Review
        AssignedTo: nobody@xxxxxxxxxxxxxxxxx
        ReportedBy: jcp@xxxxxxxxxx
         QAContact: extras-qa@xxxxxxxxxxxxxxxxx
                CC: notting@xxxxxxxxxx,
                    package-review@xxxxxxxxxxxxxxxxxxxxxxx
    Classification: Fedora
      Story Points: ---
              Type: ---
        Regression: ---
        Mount Type: ---
     Documentation: ---


Spec URL: http://www.eskimo.com/~jcp/glueminisat.spec
SRPM URL: http://www.eskimo.com/~jcp/glueminisat-2.2.5-1.fc16.src.rpm
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.

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.
_______________________________________________
package-review mailing list
package-review@xxxxxxxxxxxxxxxxxxxxxxx
https://admin.fedoraproject.org/mailman/listinfo/package-review