Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the cl-sat.glucose Reference Manual, version 0.1, generated automatically by Declt version 4.0 beta 2 "William Riker" on Wed Jun 15 04:01:16 2022 GMT+0.
Next: Systems, Previous: The cl-sat.glucose Reference Manual, Up: The cl-sat.glucose Reference Manual [Contents][Index]
* Cl-Sat.Glucose
CL-SAT instance to Glucose state-of-the-art SAT solver.
See [[https://github.com/guicho271828/cl-sat][cl-sat]] for details.
This downloads the later 2014 version (2nd in the competition) from http://www.labri.fr/perso/lsimon/glucose/.
** Usage
See also: https://github.com/guicho271828/cl-sat
#+BEGIN_SRC lisp
(cl-sat:solve '(and (or a b) (or a !b c)) :glucose)
;; ->
;; (C A)
;; T
;; T
#+END_SRC
** Dependencies
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 ::
** Installation
** Author
+ Masataro Asai (guicho2.71828@gmail.com)
* Copyright
Copyright (c) 2016 Masataro Asai (guicho2.71828@gmail.com)
* License
Licensed under the LLGPL License.
Next: Modules, Previous: Introduction, Up: The cl-sat.glucose Reference Manual [Contents][Index]
The main system appears first, followed by any subsystem dependency.
CL-SAT instance to Glucose state-of-the-art SAT solver. This downloads the later 2014 version (2nd in the 2014 SAT competition).
Masataro Asai
(GIT https://github.com/guicho271828/cl-sat.glucose.git)
LLGPL
0.1
trivial-package-manager (system).
src (module).
Next: Files, Previous: Systems, Up: The cl-sat.glucose Reference Manual [Contents][Index]
Modules are listed depth-first from the system components tree.
cl-sat.glucose (system).
package.lisp (file).
Next: Packages, Previous: Modules, Up: The cl-sat.glucose Reference Manual [Contents][Index]
Files are sorted by type and then listed depth-first from the systems components trees.
Next: cl-sat.glucose/src/package.lisp, Previous: Lisp, Up: Lisp [Contents][Index]
cl-sat.glucose (system).
Previous: cl-sat.glucose/cl-sat.glucose.asd, Up: Lisp [Contents][Index]
src (module).
Next: Definitions, Previous: Files, Up: The cl-sat.glucose Reference Manual [Contents][Index]
Packages are listed by definition order.
Next: cl-sat.glucose, Previous: Packages, Up: Packages [Contents][Index]
Previous: cl-sat.glucose-asd, Up: Packages [Contents][Index]
Next: Indexes, Previous: Packages, Up: The cl-sat.glucose Reference Manual [Contents][Index]
Definitions are sorted by export status, category, package, and then by lexicographic order.
Previous: Definitions, Up: Definitions [Contents][Index]
Next: Ordinary functions, Previous: Internals, Up: Internals [Contents][Index]
Previous: Special variables, Up: Internals [Contents][Index]
Previous: Definitions, Up: The cl-sat.glucose Reference Manual [Contents][Index]
| Jump to: | F G |
|---|
| Index Entry | Section | ||
|---|---|---|---|
| | |||
| F | |||
Function, glucose-binary: | Private ordinary functions | ||
| | |||
| G | |||
glucose-binary: | Private ordinary functions | ||
| | |||
| Jump to: | F G |
|---|
Next: Data types, Previous: Functions, Up: Indexes [Contents][Index]
| Jump to: | *
S |
|---|
| Index Entry | Section | ||
|---|---|---|---|
| | |||
| * | |||
*glucose-home*: | Private special variables | ||
| | |||
| S | |||
Special Variable, *glucose-home*: | Private special variables | ||
| | |||
| Jump to: | *
S |
|---|
| Jump to: | C F M P S |
|---|
| Jump to: | C F M P S |
|---|