Cl-Sat.Glucose - CL-SAT instance to Glucose state-of-the-art SAT solver.
See cl-sat for details.
This downloads the later 2014 version (2nd in the competition) from http://www.labri.fr/perso/lsimon/glucose/.
See also: https://github.com/guicho271828/cl-sat
(cl-sat:solve '(and (or a b) (or a !b c)) :glucose) ;; -> ;; (C A) ;; T ;; T
Requires cURL and Make to download & build the binary.
This library is at least tested on implementation listed below:
- SBCL 1.3.5 on X86-64 Linux 3.19.0-59-generic (author’s environment)
Also, it depends on the following libraries:
- trivia by Masataro Asai
- NON-optimized pattern matcher compatible with OPTIMA, with extensible optimizer interface and clean codebase
- alexandria by
- Alexandria is a collection of portable public domain utilities.
- iterate by
- Jonathan Amsterdam’s iterator/gatherer/accumulator facility
- Masataro Asai (firstname.lastname@example.org)
Copyright (c) 2016 Masataro Asai (email@example.com)
Licensed under the LLGPL License.