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