The cl-sat.glucose Reference Manual

Table of Contents

The cl-sat.glucose Reference Manual

This is the cl-sat.glucose Reference Manual, version 0.1, generated automatically by Declt version 3.0 "Montgomery Scott" on Wed Oct 13 10:06:42 2021 GMT+0.

1 Introduction

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

2 Systems

The main system appears first, followed by any subsystem dependency.

2.1 cl-sat.glucose

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

Home Page

http://www.labri.fr/perso/lsimon/glucose/

Source Control

(:git "https://github.com/guicho271828/cl-sat.glucose.git")

Bug Tracker

https://github.com/guicho271828/cl-sat.glucose/issues

License

LLGPL

Description

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

Version

0.1

Defsystem Dependency

trivial-package-manager

Dependencies

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

Source

cl-sat.glucose.asd (file)

Component

src (module)

3 Modules

Modules are listed depth-first from the system components tree.

3.1 cl-sat.glucose/src

Parent

cl-sat.glucose (system)

Location

src/

Component

package.lisp (file)

4 Files

Files are sorted by type and then listed depth-first from the systems components trees.

4.1 Lisp

4.1.1 cl-sat.glucose.asd

Location

cl-sat.glucose.asd

Systems

cl-sat.glucose (system)

Packages

cl-sat.glucose-asd

4.1.2 cl-sat.glucose/src/package.lisp

Parent

src (module)

Location

src/package.lisp

Packages

cl-sat.glucose

Internal Definitions

• *glucose-home* (special variable)
• glucose-binary (function)

5 Packages

Packages are listed by definition order.

5.1 cl-sat.glucose-asd

Source

cl-sat.glucose.asd

Use List

• asdf/interface
• common-lisp

5.2 cl-sat.glucose

Source

package.lisp (file)

Use List

• cl-sat
• iterate
• alexandria
• trivia.level2
• common-lisp

Internal Definitions

• *glucose-home* (special variable)
• glucose-binary (function)

6 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.

6.1 Internal definitions

6.1.1 Special variables

Special Variable: *glucose-home*

Package

cl-sat.glucose

Source

package.lisp (file)

6.1.2 Functions

Function: glucose-binary &optional *GLUCOSE-HOME*

Package

cl-sat.glucose

Source

package.lisp (file)

Appendix A Indexes

A.1 Concepts

A.2 Functions

A.3 Variables

A.4 Data types