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 3.0 "Montgomery Scott" on Fri Jun 26 10:32:57 2020 GMT+0.


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

1 Introduction


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

[[https://travis-ci.org/cl-model-languages/cl-sat][https://travis-ci.org/cl-model-languages/cl-sat.svg?branch=master]]

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

*NEWS*

+ 2018/12/24 :: Implemented Tseytin's transformation for the input logic formula.
                The input S-exp can be an arbitrary logical formula that is not necessarily a CNF.
+ 2019/1/8 :: Implemented a =:COMPETITION= keyword for the generic function
              =SOLVE=, which accepts =:year=, =:track=, =:name= argument
              specifying the solver that particupated in SAT Competition 2016,2017,2018.
              For example, you can run
              =(solve :competition 
:name "Lingeling" :track "main_and_glucose_hack" :year 2018)= to obtain the Lingeling that participated in SAT Competition 2018. The list of available solvers are: + 2016: https://baldur.iti.kit.edu/sat-competition-2016/solvers/ + 2017: https://baldur.iti.kit.edu/sat-competition-2017/solvers/ + 2017: http://sat2018.forsyte.tuwien.ac.at/solvers/ + [[./competition.org][Here is the list of solvers that worked.]] + 2019/1/25 :: the input formula can now contain (IMPLY lhs rhs) and (IFF lhs rhs). + 2019/3/6 :: the input formula can contain more operations. See description below ** Usage In order to load and run minisat2, run follows: #+begin_src lisp (ql:quickload :cl-sat.minisat) (cl-sat:solve '(and (or a b) (or a !b c)) :minisat) -> (C B) T T (ql:quickload :cl-sat.glucose) (cl-sat:solve '(and (or a b) (or a !b c)) :glucose) -> (C B) T T (cl-sat:solve '(and (or a b) (or a !b c)) :competition :year 2018 :track "main_and_glucose_hack" :name "Lingeling") -> (C B A) T T #+end_src ** Solver API *Generic function* =(solve pathname (eql :solvername) &rest options)= 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. + On some occasions, depending on the solver, it also returns the fourth value, which is a list of variables that don't matter: it can be either true or false. ** Input format Users will most often use the method specialized to the S-exp interface =(solve list (eql :solvername) &rest options)=. =list= is a cons tree of symbols as an arbitrary propositional formula. The following logical operators are supported: + =or= + =and= + =not= + =imply => when= (synonyms) + =iff= + =eq equal <=>= (synonyms, variations of IFF that take multiple statements) + =xor= 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 interpreted as the negated atoms: =!A= is same as =(not A)=. These are internally converted into a NNF via De Morgan's law and then to a CNF via Tseytin transformation. 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)) (or (and a b) (and b c)) ; -> (and (or aux1 aux2) (or (not aux1) a) (or aux1 (not a) (not b)) ...) #+END_SRC ** S-exp converters Users might also be interested in the functions used for processing the logical formula. + =(symbolicate-form form)= :: This function is the first step of converting the input into a normal form. It normalizes the input tree containing numbers and !-negated vars into a tree of symbols. Note that it does not guarantee to return any type of normal forms (e.g. NNF,CNF,DNF,ANF). It accepts any types of compound forms, not limited to AND/OR/NOT. + =(expand-extensions form)= :: Translates extended logical operations into AND, OR, NOT. It support the following operations: + =IMPLY, =>, WHEN= (synonyms), + =IFF=, + =EQ, EQUAL, <=>= (synonyms, a variation of IFF that takes multiple statements), + =XOR=. + =(simplify-nnf form)= :: Remove some obvious constants / conflicts in the NNF. The result does not contain: + Single compound forms: + (and X), (or X) + Compound forms containing true/false constants: + =(and ... (or) ... ) -> (or)= + =(or ... (and) ... ) -> (and)= + =(or ... X ... (not X) ... ) -> (and)= + =(and ... X ... (not X) ... ) -> (or)= + Duplicated forms: + =(and ... X ... X ... ) -> (and ... X ... ...)= + =(or ... X ... X ... ) -> (or ... X ... ...)= + =(to-nnf form)= :: Applying De-Morgan's law, the resulting tree contains negations only at the leaf nodes. Calls =expand-extensions= and =simplify-nnf= internally. + =(to-cnf form &optional converter)= :: Translates the results to a CNF. Calls =symbolicate-form= and =to-nnf= internally. =converter= argument specifies which algorithm to use for the conversion, defaulting to =#'to-cnf-tseytin=. ** Helper functions =(var suffix &optional (prefix "V"))= This function interns SUFFIX (usually a number, but can be any printable object) to a symbol with the optional PREFIX. The new symbol is interned in a package =CL-SAT.VARIABLES= . This function is particularly useful for implementing some SAT encoding of other problems, such as knapsack or bin-packing problem. ** 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 ** 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

Packages
Exported Definitions
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)

Internal Definitions

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-dimacs.lisp

Dependency

src/2-class.lisp (file)

Parent

cl-sat (system)

Location

src/3-dimacs.lisp

Exported Definitions
Internal Definitions

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

3.1.7 cl-sat/src/4-competition.lisp

Dependency

src/3-dimacs.lisp (file)

Parent

cl-sat (system)

Location

src/4-competition.lisp

Exported Definitions

solve (method)

Internal Definitions

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

4 Packages

Packages are listed by definition order.


Next: , 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: Packages   [Contents][Index]

4.2 cl-sat.variables

Source

src/1-parse.lisp (file)


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

4.3 cl-sat.aux-variables

Source

src/1-parse.lisp (file)


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/2-class.lisp (file)

Special Variable: *verbosity*
Package

cl-sat

Source

src/3-dimacs.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.
TEMPLATE should be a string that ends with one or more X’s, these X’s will be replaced by random characters.
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. An error of type file-error is signalled if a unique file name can’t be generated after a number of attempts.

Package

cl-sat

Source

src/1-util.lisp (file)


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

5.1.3 Functions

Function: aux SUFFIX &optional PREFIX

intern a suffix to an auxiliary symbol

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: expand-extensions FORM

Translates extended logical operations into AND, OR, NOT.
IMPLY, =>, WHEN (synonyms),
IFF,
EQ, EQUAL, <=> (synonyms, a variation of IFF that takes multiple statements), XOR.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: parse-dimacs-output FILE INSTANCE
Package

cl-sat

Source

src/3-dimacs.lisp (file)

Function: print-cnf INSTANCE &optional STREAM *VERBOSITY*
Package

cl-sat

Source

src/3-dimacs.lisp (file)

Function: simplify-nnf FORM

Remove some obvious constants / conflicts in the form. The result does not contain: Single compound forms:
(and X), (or X)
Compound forms containing true/false constants:
(and ... (or) ... ) -> (or)
(or ... (and) ... ) -> (and)
(or ... X ... (not X) ... ) -> (and)
(and ... X ... (not X) ... ) -> (or)
Duplicated forms:
(and ... X ... X ... ) -> (and ... X ... ...)
(or ... X ... X ... ) -> (or ... X ... ...)

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: symbolicate-form TREE

This function is the first step of converting the input into a normal form.
It normalizes the input tree containing numbers and !-negated vars into a tree of symbols. Note that it does not guarantee to return any type of normal forms (e.g. NNF,CNF,DNF,ANF). It accepts any types of compound forms, not limited to AND/OR/NOT.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: to-anf FORM

Convert an arbitrary logical form into an algebraic normal form consisting of XOR, AND, and T.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: to-cnf FORM &optional CONVERTER

Translates the results to a CNF.
Calls SYMBOLICATE-FORM and TO-NNF internally.
CONVERTER argument specifies which algorithm to use for the conversion, default: #’to-cnf-tseytin.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: to-cnf-naive NNF

Convert a NNF into a flattened CNF via a naive method.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: to-cnf-tseytin FORM

Convert a NNF into a flattened CNF.
OR branches containing ANDs that could result in an exponential CNF
are converted into a linear-sized equisatisfiable formula
via Tseytin transformation by Tseytin 1968.

aux-variables are generated in CL-SAT.AUX-VARIABLES package.

G.S. Tseytin: On the complexity of derivation in propositional calculus. Presented at the Leningrad Seminar on Mathematical Logic held in September 1966.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: to-nnf FORM

Applying De-Morgan’s law, the resulting tree contains negations only at the leaf nodes. Calls expand-extensions internally.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: var SUFFIX &optional PREFIX

Helper function: Interns SUFFIX (usually a number, but can be any printable object) to a symbol with the optional PREFIX. The new symbol is interned in package CL-SAT.VARIABLES.

Package

cl-sat

Source

src/1-parse.lisp (file)


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

5.1.4 Generic functions

Generic Function: solve INPUT SOLVER-DESIGNATOR &rest ARGS &key DEBUG YEAR TRACK NAME CONVERTER &allow-other-keys
Package

cl-sat

Source

src/2-class.lisp (file)

Methods
Method: solve (INPUT pathname) (COMPETITION (eql competition)) &rest OPTIONS &key DEBUG YEAR TRACK NAME &allow-other-keys
Source

src/4-competition.lisp (file)

Method: solve (I list) SOLVER &rest ARGS &key CONVERTER &allow-other-keys
Method: solve (*INSTANCE* sat-instance) SOLVER &rest ARGS &key DEBUG &allow-other-keys
Generic Function: variables INSTANCE
Package

cl-sat

Source

src/2-class.lisp (file)

Methods
Method: variables (INSTANCE sat-instance)
Method: variables (INSTANCE sat-instance) around

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
Direct slots
Slot: cnf
Initargs

:cnf

Readers

cnf (generic function)

Slot: %variables

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

5.2 Internal definitions


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

5.2.1 Special variables

Special Variable: *base-url*
Package

cl-sat

Source

src/4-competition.lisp (file)

Special Variable: +random-string-size-min+
Package

cl-sat

Source

src/1-util.lisp (file)

Special Variable: +temp-file-attempts+
Package

cl-sat

Source

src/1-util.lisp (file)


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

5.2.2 Functions

Function: %merge-same-clauses TYPE FORMS
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: %sort-clauses FORMS
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: %to-anf FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: %to-nnf FORM
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: attempt-create-temp DIRECTORY BASE-DIR NAME-PREFIX RANDOM-STRING-SIZE ATTEMPTS

Creates a file/directory in BASE-DIR with NAME-PREFIX as a prefix of the name and RANDOM-STRING-SIZE random base62 characters at the end.
Returns the name of the created file.
Signals an error if it can’t generate a unique name after ATTEMPTS attempts.

Package

cl-sat

Source

src/1-util.lisp (file)

Function: clause< A B
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: create-nonexisting DIRECTORY PATH

Attempts to create a file/directory, returns NIL if it exists already and T otherwise.

Package

cl-sat

Source

src/1-util.lisp (file)

Function: dispatch FORM TOP K

Naive implementation that expands the inner ANDs of ORs into ORs of ANDs (potentially exponentially explode).
Implemented using Continuation Passing Style. Calling K with a value is equivalent to returning the result of processing FORM.

TOP is a boolean which, when NIL, means the current position is inside an OR.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: download-solver YEAR TRACK NAME
Package

cl-sat

Source

src/4-competition.lisp (file)

Function: format1 STREAM FORMAT-CONTROL FIRST-ARG &rest MORE-ARGS
Package

cl-sat

Source

src/1-util.lisp (file)

Function: generate-temp-name NAME-PREFIX RANDOM-STRING-SIZE

Generates a random name for a temp file/directory.
NAME-PREFIX is the prefix of the name, after which RANDOM-STRING-SIZE random characters are added.

Package

cl-sat

Source

src/1-util.lisp (file)

Function: negate FORM

Simple negation not involving De-Morgan’s law.

Package

cl-sat

Source

src/1-parse.lisp (file)

Function: parse-assignments FILE INSTANCE
Package

cl-sat

Source

src/3-dimacs.lisp (file)

Function: parse-assignments-ignoring-symbols FILE INSTANCE
Package

cl-sat

Source

src/3-dimacs.lisp (file)

Function: parse-true-dimacs-output FILE INSTANCE
Package

cl-sat

Source

src/3-dimacs.lisp (file)

Function: random-base62 N

Returns a random base62 string with n characters.

Package

cl-sat

Source

src/1-util.lisp (file)

Function: symbol< A B
Package

cl-sat

Source

src/1-parse.lisp (file)

Function: symbol<= A B
Package

cl-sat

Source

src/1-parse.lisp (file)


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

5.2.3 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: Internal definitions   [Contents][Index]

5.2.4 Conditions

Condition: build-error ()
Package

cl-sat

Source

src/4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: chmod-error ()
Package

cl-sat

Source

src/4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: competition-setup-error ()
Package

cl-sat

Source

src/4-competition.lisp (file)

Direct superclasses

error (condition)

Direct subclasses
Direct methods

print-object (method)

Direct slots
Slot: year
Initargs

:year

Slot: track
Initargs

:track

Slot: name
Initargs

:name

Condition: download-error ()
Package

cl-sat

Source

src/4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: unzip-error ()
Package

cl-sat

Source

src/4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)


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․asd file
cl-sat/src/0-package.lisp: The cl-sat/src/0-package․lisp file
cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse․lisp file
cl-sat/src/1-util.lisp: The cl-sat/src/1-util․lisp file
cl-sat/src/2-class.lisp: The cl-sat/src/2-class․lisp file
cl-sat/src/3-dimacs.lisp: The cl-sat/src/3-dimacs․lisp file
cl-sat/src/4-competition.lisp: The cl-sat/src/4-competition․lisp file

F
File, Lisp, cl-sat.asd: The cl-sat․asd file
File, Lisp, cl-sat/src/0-package.lisp: The cl-sat/src/0-package․lisp file
File, Lisp, cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse․lisp file
File, Lisp, cl-sat/src/1-util.lisp: The cl-sat/src/1-util․lisp file
File, Lisp, cl-sat/src/2-class.lisp: The cl-sat/src/2-class․lisp file
File, Lisp, cl-sat/src/3-dimacs.lisp: The cl-sat/src/3-dimacs․lisp file
File, Lisp, cl-sat/src/4-competition.lisp: The cl-sat/src/4-competition․lisp file

L
Lisp File, cl-sat.asd: The cl-sat․asd file
Lisp File, cl-sat/src/0-package.lisp: The cl-sat/src/0-package․lisp file
Lisp File, cl-sat/src/1-parse.lisp: The cl-sat/src/1-parse․lisp file
Lisp File, cl-sat/src/1-util.lisp: The cl-sat/src/1-util․lisp file
Lisp File, cl-sat/src/2-class.lisp: The cl-sat/src/2-class․lisp file
Lisp File, cl-sat/src/3-dimacs.lisp: The cl-sat/src/3-dimacs․lisp file
Lisp File, cl-sat/src/4-competition.lisp: The cl-sat/src/4-competition․lisp file

Jump to:   C   F   L  

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

A.2 Functions

Jump to:   %  
A   C   D   E   F   G   M   N   P   R   S   T   V   W  
Index Entry  Section

%
%merge-same-clauses: Internal functions
%sort-clauses: Internal functions
%to-anf: Internal functions
%to-nnf: Internal functions

A
attempt-create-temp: Internal functions
aux: Exported functions

C
clause<: Internal functions
cnf: Internal generic functions
cnf: Internal generic functions
create-nonexisting: Internal functions

D
dispatch: Internal functions
download-solver: Internal functions

E
expand-extensions: Exported functions

F
format1: Internal functions
Function, %merge-same-clauses: Internal functions
Function, %sort-clauses: Internal functions
Function, %to-anf: Internal functions
Function, %to-nnf: Internal functions
Function, attempt-create-temp: Internal functions
Function, aux: Exported functions
Function, clause<: Internal functions
Function, create-nonexisting: Internal functions
Function, dispatch: Internal functions
Function, download-solver: Internal functions
Function, expand-extensions: Exported functions
Function, format1: Internal functions
Function, generate-temp-name: Internal functions
Function, negate: Internal functions
Function, parse-assignments: Internal functions
Function, parse-assignments-ignoring-symbols: Internal functions
Function, parse-dimacs-output: Exported functions
Function, parse-true-dimacs-output: Internal functions
Function, print-cnf: Exported functions
Function, random-base62: Internal functions
Function, simplify-nnf: Exported functions
Function, symbol<: Internal functions
Function, symbol<=: Internal functions
Function, symbolicate-form: Exported functions
Function, to-anf: Exported functions
Function, to-cnf: Exported functions
Function, to-cnf-naive: Exported functions
Function, to-cnf-tseytin: Exported functions
Function, to-nnf: Exported functions
Function, var: Exported functions

G
generate-temp-name: Internal functions
Generic Function, cnf: Internal generic functions
Generic Function, solve: Exported generic functions
Generic Function, variables: Exported generic functions

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

N
negate: Internal functions

P
parse-assignments: Internal functions
parse-assignments-ignoring-symbols: Internal functions
parse-dimacs-output: Exported functions
parse-true-dimacs-output: Internal functions
print-cnf: Exported functions

R
random-base62: Internal functions

S
simplify-nnf: Exported functions
solve: Exported generic functions
solve: Exported generic functions
solve: Exported generic functions
solve: Exported generic functions
symbol<: Internal functions
symbol<=: Internal functions
symbolicate-form: Exported functions

T
to-anf: Exported functions
to-cnf: Exported functions
to-cnf-naive: Exported functions
to-cnf-tseytin: Exported functions
to-nnf: Exported functions

V
var: Exported functions
variables: Exported generic functions
variables: Exported generic functions
variables: Exported generic functions

W
with-temp: Exported macros

Jump to:   %  
A   C   D   E   F   G   M   N   P   R   S   T   V   W  

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

A.3 Variables

Jump to:   %   *   +  
C   N   S   T   Y  
Index Entry  Section

%
%variables: Exported classes

*
*base-url*: Internal special variables
*instance*: Exported special variables
*verbosity*: Exported special variables

+
+random-string-size-min+: Internal special variables
+temp-file-attempts+: Internal special variables

C
cnf: Exported classes

N
name: Internal conditions

S
Slot, %variables: Exported classes
Slot, cnf: Exported classes
Slot, name: Internal conditions
Slot, track: Internal conditions
Slot, year: Internal conditions
Special Variable, *base-url*: Internal special variables
Special Variable, *instance*: Exported special variables
Special Variable, *verbosity*: Exported special variables
Special Variable, +random-string-size-min+: Internal special variables
Special Variable, +temp-file-attempts+: Internal special variables

T
track: Internal conditions

Y
year: Internal conditions

Jump to:   %   *   +  
C   N   S   T   Y  

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

A.4 Data types

Jump to:   B   C   D   P   S   U  
Index Entry  Section

B
build-error: Internal conditions

C
chmod-error: Internal conditions
cl-sat: The cl-sat system
cl-sat: The cl-sat package
cl-sat.aux-variables: The cl-sat․aux-variables package
cl-sat.variables: The cl-sat․variables package
Class, sat-instance: Exported classes
competition-setup-error: Internal conditions
Condition, build-error: Internal conditions
Condition, chmod-error: Internal conditions
Condition, competition-setup-error: Internal conditions
Condition, download-error: Internal conditions
Condition, unzip-error: Internal conditions

D
download-error: Internal conditions

P
Package, cl-sat: The cl-sat package
Package, cl-sat.aux-variables: The cl-sat․aux-variables package
Package, cl-sat.variables: The cl-sat․variables package

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

U
unzip-error: Internal conditions

Jump to:   B   C   D   P   S   U