The cl-sat Reference Manual

Table of Contents

Next: , Previous: , Up: (dir)   [Contents][Index]

The cl-sat Reference Manual

This is the cl-sat Reference Manual, version 0.1, generated automatically by Declt version 2.3 "Robert April" on Tue Feb 20 08:16:59 2018 GMT+0.


Next: , Previous: , Up: Top   [Contents][Index]

1 Introduction


* CL-SAT  - Common Lisp API to Boolean SAT Solvers

This library provides a simple S-exp -> CNF translator and an API to Boolean SAT solvers.
  
It does not provide actual implementation to each solver instance by itself.
Currently there are two implementations. Consult the following:

+ https://github.com/guicho271828/cl-sat.minisat
+ https://github.com/guicho271828/cl-sat.glucose

** Usage
   
In order to load and run minisat2, run follows:

: (ql:quickload :cl-sat.minisat)
:
: (cl-sat:solve '(and (or a b) (or a !b c)) :minisat)
: ->
: (C A)
: T
: T

** solver API

Each solver implementation should provide a method =(solve pathname (eql :solvername) &rest options)=.
Additional arguments are passed to the underlying solvers (unless explicitly specified).

It should return a list of true variables as the first value, a boolean indicating SAT when true, and a
boolean indicating whether the result is determined. For example,

+ =NIL,NIL,NIL= means the solver failed due to the timelimit etc. so the result was indeterminable.
+ =NIL,T,T= means that the problem is SAT by assigning all variables to false.
+ =NIL,NIL,T= means that the problem is UNSAT.

** S-exp -> CNF converter

The input list is interpreted as a CNF formula.
=AND= and =OR= are sometimes implied.
Negated/false atoms are specified by =NOT=.

Each term can be specified by a symbol or a number, but do not mix two styles (it may contain bugs).
Symbols with =!= prefix and negative numbers are treated as false atoms.

Examples:

#+BEGIN_SRC lisp
a ;; -> equivalent to (and (or a))

(or a b) ;; -> equivalent to (and (or a b))

(and a b c) ;; -> equivalent to (and (or a) (or b) (or c))

(and 1 !b c) ;; -> undefined

(and a (or !b c)) ;; equivalent to (and (or a) (or (not b) c))
#+END_SRC

** Dependencies

Required libraries depends on the solver instance. See the corresponding documentation.

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



** 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: , Previous: , Up: Top   [Contents][Index]

2 Systems

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


Previous: , Up: Systems   [Contents][Index]

2.1 cl-sat

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

License

LLGPL

Description

Common Lisp API to Boolean SAT Solvers

Version

0.1

Dependencies
Source

cl-sat.asd (file)

Components

Next: , Previous: , Up: Top   [Contents][Index]

3 Files

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


Previous: , Up: Files   [Contents][Index]

3.1 Lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.1 cl-sat.asd

Location

cl-sat.asd

Systems

cl-sat (system)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.2 cl-sat/src/0-package.lisp

Parent

cl-sat (system)

Location

src/0-package.lisp

Packages

cl-sat


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.3 cl-sat/src/1-parse.lisp

Dependency

src/0-package.lisp (file)

Parent

cl-sat (system)

Location

src/1-parse.lisp

Exported Definitions

form-cnf (function)

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.4 cl-sat/src/1-util.lisp

Dependency

src/1-parse.lisp (file)

Parent

cl-sat (system)

Location

src/1-util.lisp

Exported Definitions

with-temp (macro)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.5 cl-sat/src/2-class.lisp

Dependency

src/1-util.lisp (file)

Parent

cl-sat (system)

Location

src/2-class.lisp

Exported Definitions
Internal Definitions

cnf (method)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.6 cl-sat/src/3-methods.lisp

Dependency

src/2-class.lisp (file)

Parent

cl-sat (system)

Location

src/3-methods.lisp

Exported Definitions

Previous: , Up: Lisp files   [Contents][Index]

3.1.7 cl-sat/src/3-print.lisp

Dependency

src/3-methods.lisp (file)

Parent

cl-sat (system)

Location

src/3-print.lisp

Exported Definitions

print-cnf (function)


Next: , Previous: , Up: Top   [Contents][Index]

4 Packages

Packages are listed by definition order.


Previous: , Up: Packages   [Contents][Index]

4.1 cl-sat

Source

src/0-package.lisp (file)

Nickname

sat

Use List
Exported Definitions
Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

5 Definitions

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


Next: , Previous: , Up: Definitions   [Contents][Index]

5.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.1 Special variables

Special Variable: *instance*
Package

cl-sat

Source

src/3-methods.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.2 Macros

Macro: with-temp (VAR &key DIRECTORY TEMPLATE TMPDIR DEBUG) &body BODY

Create a temporary file, then remove the file by unwind-protect.
Most arguments are analogous to mktemp.
When DIRECTORY is non-nil, creates a directory instead.
When DEBUG is non-nil, it does not remove the directory so that you can investigate what happened inside the directory.

Package

cl-sat

Source

src/1-util.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.3 Functions

Function: form-cnf FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: print-cnf INSTANCE &optional STREAM
Package

cl-sat

Source

src/3-print.lisp (file)

Function: sat-instance-variables INSTANCE
Package

cl-sat

Source

src/3-methods.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.4 Generic functions

Generic Function: solve INPUT SOLVER-DESIGNATOR &rest ARGS
Package

cl-sat

Source

src/2-class.lisp (file)

Methods
Method: solve (I list) SOLVER &rest ARGS
Source

src/3-methods.lisp (file)

Method: solve (*INSTANCE* sat-instance) SOLVER &rest ARGS
Source

src/3-methods.lisp (file)


Previous: , Up: Exported definitions   [Contents][Index]

5.1.5 Classes

Class: sat-instance ()
Package

cl-sat

Source

src/2-class.lisp (file)

Direct superclasses

standard-object (class)

Direct methods
  • solve (method)
  • initialize-instance (method)
  • cnf (method)
Direct slots
Slot: cnf
Initargs

:cnf

Readers

cnf (generic function)


Previous: , Up: Definitions   [Contents][Index]

5.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.1 Functions

Function: %form->cnf FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: composite-negate-p FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: flatten-cnf FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: negate FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: normalize-form TREE
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: var NUMBER

intern a number to a symbol

Package

cl-sat

Source

src/1-parse.lisp (file)


Previous: , Up: Internal definitions   [Contents][Index]

5.2.2 Generic functions

Generic Function: cnf OBJECT
Package

cl-sat

Methods
Method: cnf (SAT-INSTANCE sat-instance)

automatically generated reader method

Source

src/2-class.lisp (file)


Previous: , Up: Top   [Contents][Index]

Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts

Jump to:   C   F   L  
Index Entry  Section

C
cl-sat.asd: The cl-sat<dot>asd file
cl-sat/src/0-package.lisp: The cl-sat/src/0-package<dot>lisp file
cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse<dot>lisp file
cl-sat/src/1-util.lisp: The cl-sat/src/1-util<dot>lisp file
cl-sat/src/2-class.lisp: The cl-sat/src/2-class<dot>lisp file
cl-sat/src/3-methods.lisp: The cl-sat/src/3-methods<dot>lisp file
cl-sat/src/3-print.lisp: The cl-sat/src/3-print<dot>lisp file

F
File, Lisp, cl-sat.asd: The cl-sat<dot>asd file
File, Lisp, cl-sat/src/0-package.lisp: The cl-sat/src/0-package<dot>lisp file
File, Lisp, cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse<dot>lisp file
File, Lisp, cl-sat/src/1-util.lisp: The cl-sat/src/1-util<dot>lisp file
File, Lisp, cl-sat/src/2-class.lisp: The cl-sat/src/2-class<dot>lisp file
File, Lisp, cl-sat/src/3-methods.lisp: The cl-sat/src/3-methods<dot>lisp file
File, Lisp, cl-sat/src/3-print.lisp: The cl-sat/src/3-print<dot>lisp file

L
Lisp File, cl-sat.asd: The cl-sat<dot>asd file
Lisp File, cl-sat/src/0-package.lisp: The cl-sat/src/0-package<dot>lisp file
Lisp File, cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse<dot>lisp file
Lisp File, cl-sat/src/1-util.lisp: The cl-sat/src/1-util<dot>lisp file
Lisp File, cl-sat/src/2-class.lisp: The cl-sat/src/2-class<dot>lisp file
Lisp File, cl-sat/src/3-methods.lisp: The cl-sat/src/3-methods<dot>lisp file
Lisp File, cl-sat/src/3-print.lisp: The cl-sat/src/3-print<dot>lisp file

Jump to:   C   F   L  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   %  
C   F   G   M   N   P   S   V   W  
Index Entry  Section

%
%form->cnf: Internal functions

C
cnf: Internal generic functions
cnf: Internal generic functions
composite-negate-p: Internal functions

F
flatten-cnf: Internal functions
form-cnf: Exported functions
Function, %form->cnf: Internal functions
Function, composite-negate-p: Internal functions
Function, flatten-cnf: Internal functions
Function, form-cnf: Exported functions
Function, negate: Internal functions
Function, normalize-form: Internal functions
Function, print-cnf: Exported functions
Function, sat-instance-variables: Exported functions
Function, var: Internal functions

G
Generic Function, cnf: Internal generic functions
Generic Function, solve: Exported generic functions

M
Macro, with-temp: Exported macros
Method, cnf: Internal generic functions
Method, solve: Exported generic functions
Method, solve: Exported generic functions

N
negate: Internal functions
normalize-form: Internal functions

P
print-cnf: Exported functions

S
sat-instance-variables: Exported functions
solve: Exported generic functions
solve: Exported generic functions
solve: Exported generic functions

V
var: Internal functions

W
with-temp: Exported macros

Jump to:   %  
C   F   G   M   N   P   S   V   W  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.3 Variables

Jump to:   *  
C   S  
Index Entry  Section

*
*instance*: Exported special variables

C
cnf: Exported classes

S
Slot, cnf: Exported classes
Special Variable, *instance*: Exported special variables

Jump to:   *  
C   S  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   C   P   S  
Index Entry  Section

C
cl-sat: The cl-sat system
cl-sat: The cl-sat package
Class, sat-instance: Exported classes

P
Package, cl-sat: The cl-sat package

S
sat-instance: Exported classes
System, cl-sat: The cl-sat system

Jump to:   C   P   S