The cl-sat Reference Manual

This is the cl-sat Reference Manual, version 0.1, generated automatically by Declt version 4.0 beta 2 "William Riker" on Sun Dec 08 17:21:09 2024 GMT+0.

Table of Contents


1 Introduction


2 Systems

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


2.1 cl-sat

Common Lisp API to Boolean SAT Solvers

Author

Masataro Asai

Contact

License

LLGPL

Version

0.1

Dependencies
  • trivia (system).
  • alexandria (system).
  • iterate (system).
  • trivial-features (system).
Source

cl-sat.asd.

Child Components

3 Files

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


3.1 Lisp


3.1.1 cl-sat/cl-sat.asd

Source

cl-sat.asd.

Parent Component

cl-sat (system).

ASDF Systems

cl-sat.


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

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Packages

cl-sat.


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

Dependency

src/0-package.lisp (file).

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Packages
Public Interface
Internals

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

Dependency

src/1-parse.lisp (file).

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Public Interface

with-temp (macro).

Internals

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

Dependency

src/1-util.lisp (file).

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Public Interface
Internals

cnf (reader method).


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

Dependency

src/2-class.lisp (file).

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Public Interface

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

Dependency

src/3-dimacs.lisp (file).

Source

cl-sat.asd.

Parent Component

cl-sat (system).

Public Interface
Internals

4 Packages

Packages are listed by definition order.


4.1 cl-sat

Source

src/0-package.lisp.

Nickname

sat

Use List
  • alexandria.
  • common-lisp.
  • iterate.
  • trivia.level2.
Public Interface
Internals

4.2 cl-sat.aux-variables

Source

src/1-parse.lisp.


4.3 cl-sat.variables

Source

src/1-parse.lisp.


5 Definitions

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


5.1 Public Interface


5.1.1 Special variables

Special Variable: *instance*
Package

cl-sat.

Source

src/2-class.lisp.

Special Variable: *verbosity*
Package

cl-sat.

Source

src/3-dimacs.lisp.


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.


5.1.3 Ordinary functions

Function: aux (suffix &optional prefix)

intern a suffix to an auxiliary symbol

Package

cl-sat.

Source

src/1-parse.lisp.

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.

Function: parse-assignments (file instance &optional ignore-first)

Parser for Minisat 2.2

Package

cl-sat.

Source

src/3-dimacs.lisp.

Function: parse-dimacs-output (file instance)
Package

cl-sat.

Source

src/3-dimacs.lisp.

Function: print-cnf (instance &optional stream *verbosity*)
Package

cl-sat.

Source

src/3-dimacs.lisp.

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.

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.

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.

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.

Function: to-cnf-naive (nnf)

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

Package

cl-sat.

Source

src/1-parse.lisp.

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.

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.

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.


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.

Methods
Method: solve ((input pathname) (competition (eql :competition)) &rest options &key debug year track name &allow-other-keys)
Source

src/4-competition.lisp.

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.

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

5.1.5 Standalone methods

Method: initialize-instance ((i sat-instance) &rest args &key form cnf converter &allow-other-keys)
Source

src/2-class.lisp.

Method: print-object ((c competition-setup-error) s)
Source

src/4-competition.lisp.


5.1.6 Classes

Class: sat-instance
Package

cl-sat.

Source

src/2-class.lisp.

Direct methods
Direct slots
Slot: cnf
Initargs

:cnf

Readers

cnf.

Writers

This slot is read-only.

Slot: %variables

5.2 Internals


5.2.1 Special variables

Special Variable: *base-url*
Package

cl-sat.

Source

src/4-competition.lisp.

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

cl-sat.

Source

src/1-util.lisp.

Special Variable: +temp-file-attempts+
Package

cl-sat.

Source

src/1-util.lisp.


5.2.2 Ordinary functions

Function: %merge-same-clauses (type forms)
Package

cl-sat.

Source

src/1-parse.lisp.

Function: %sort-clauses (forms)
Package

cl-sat.

Source

src/1-parse.lisp.

Function: %to-anf (form)
Package

cl-sat.

Source

src/1-parse.lisp.

Function: %to-nnf (form)
Package

cl-sat.

Source

src/1-parse.lisp.

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.
If DIRECTORY is non-nil, creates a directory.
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.

Function: clause< (a b)
Package

cl-sat.

Source

src/1-parse.lisp.

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.

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.

Function: download-solver (year track name)
Package

cl-sat.

Source

src/4-competition.lisp.

Function: format1 (stream format-control first-arg &rest more-args)
Package

cl-sat.

Source

src/1-util.lisp.

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.

Function: negate (form)

Simple negation not involving De-Morgan’s law.

Package

cl-sat.

Source

src/1-parse.lisp.

Function: random-base62 (n)

Returns a random base62 string with n characters.

Package

cl-sat.

Source

src/1-util.lisp.

Function: symbol< (a b)
Package

cl-sat.

Source

src/1-parse.lisp.

Function: symbol<= (a b)
Package

cl-sat.

Source

src/1-parse.lisp.


5.2.3 Generic functions

Generic Reader: cnf (object)
Package

cl-sat.

Methods
Reader Method: cnf ((sat-instance sat-instance))

automatically generated reader method

Source

src/2-class.lisp.

Target Slot

cnf.


5.2.4 Conditions

Condition: build-error
Package

cl-sat.

Source

src/4-competition.lisp.

Direct superclasses

competition-setup-error.

Condition: chmod-error
Package

cl-sat.

Source

src/4-competition.lisp.

Direct superclasses

competition-setup-error.

Condition: competition-setup-error
Package

cl-sat.

Source

src/4-competition.lisp.

Direct superclasses

error.

Direct subclasses
Direct methods

print-object.

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.

Direct superclasses

competition-setup-error.

Condition: unzip-error
Package

cl-sat.

Source

src/4-competition.lisp.

Direct superclasses

competition-setup-error.


Appendix A Indexes


A.1 Concepts


A.2 Functions

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

%
%merge-same-clauses: Private ordinary functions
%sort-clauses: Private ordinary functions
%to-anf: Private ordinary functions
%to-nnf: Private ordinary functions

A
attempt-create-temp: Private ordinary functions
aux: Public ordinary functions

C
clause<: Private ordinary functions
cnf: Private generic functions
cnf: Private generic functions
create-nonexisting: Private ordinary functions

D
dispatch: Private ordinary functions
download-solver: Private ordinary functions

E
expand-extensions: Public ordinary functions

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

G
generate-temp-name: Private ordinary functions
Generic Function, cnf: Private generic functions
Generic Function, solve: Public generic functions
Generic Function, variables: Public generic functions

I
initialize-instance: Public standalone methods

M
Macro, with-temp: Public macros
Method, cnf: Private generic functions
Method, initialize-instance: Public standalone methods
Method, print-object: Public standalone methods
Method, solve: Public generic functions
Method, solve: Public generic functions
Method, solve: Public generic functions
Method, variables: Public generic functions
Method, variables: Public generic functions

N
negate: Private ordinary functions

P
parse-assignments: Public ordinary functions
parse-dimacs-output: Public ordinary functions
print-cnf: Public ordinary functions
print-object: Public standalone methods

R
random-base62: Private ordinary functions

S
simplify-nnf: Public ordinary functions
solve: Public generic functions
solve: Public generic functions
solve: Public generic functions
solve: Public generic functions
symbol<: Private ordinary functions
symbol<=: Private ordinary functions
symbolicate-form: Public ordinary functions

T
to-anf: Public ordinary functions
to-cnf: Public ordinary functions
to-cnf-naive: Public ordinary functions
to-cnf-tseytin: Public ordinary functions
to-nnf: Public ordinary functions

V
var: Public ordinary functions
variables: Public generic functions
variables: Public generic functions
variables: Public generic functions

W
with-temp: Public macros


A.4 Data types

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

B
build-error: Private conditions

C
chmod-error: Private conditions
cl-sat: The cl-sat system
cl-sat: The cl-sat package
cl-sat.asd: The cl-sat/cl-sat․asd file
cl-sat.aux-variables: The cl-sat․aux-variables package
cl-sat.variables: The cl-sat․variables package
Class, sat-instance: Public classes
competition-setup-error: Private conditions
Condition, build-error: Private conditions
Condition, chmod-error: Private conditions
Condition, competition-setup-error: Private conditions
Condition, download-error: Private conditions
Condition, unzip-error: Private conditions

D
download-error: Private conditions

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

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

U
unzip-error: Private conditions