cl-sat.glucose

2022-04-01

CL-SAT instance to Glucose state-of-the-art SAT solver. This downloads the later 2014 version (2nd in the 2014 SAT competition).

Upstream URL

github.com/cl-model-languages/cl-sat.glucose

Author

Masataro Asai

License

LLGPL
README

1Cl-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/.

1.1Usage

See also: https://github.com/guicho271828/cl-sat

  (cl-sat:solve '(and (or a b) (or a !b c)) :glucose)
  ;; ->
  ;; (C A)
  ;; T
  ;; T

1.2Dependencies

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
cl-sat

1.3Installation

1.4Author

  • Masataro Asai (guicho2.71828@gmail.com)

2Copyright

Copyright (c) 2016 Masataro Asai (guicho2.71828@gmail.com)

3License

Licensed under the LLGPL License.

Dependencies (6)

  • alexandria
  • cl-sat
  • fiveam
  • iterate
  • trivia
  • trivial-package-manager

Dependents (0)

    • GitHub
    • Quicklisp