eb924c41bc
See the full description here: http://www.labri.fr/perso/lsimon/glucose/ Patches and build warnings were reported to the authors. Submitted by: myself Approved by: adamw (mentor) Differential Revision: https://reviews.freebsd.org/D14156
13 lines
545 B
Plaintext
13 lines
545 B
Plaintext
Glucose is based on the MiniSat solver, and extends it by preserving
|
|
the so-called "glue clauses" and using new scoring scheme.
|
|
|
|
Glucose is a SAT solver based on a particular scoring scheme for the clause
|
|
learning mechanism, based on the paper Laurent Simon and Gilles Audemard
|
|
presented at IJCAI'09. Solver's name is a contraction of the concept of
|
|
"glue clauses", a particular kind of clauses that glucose detects and preserves
|
|
during search.
|
|
|
|
Glucose accepts SAT problems in the DIMACS format.
|
|
|
|
WWW: http://www.labri.fr/perso/lsimon/glucose/
|