The cl-sat Reference Manual

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

• cl-sat.aux-variables.
• cl-sat.variables.

Public Interface

• aux (function).
• expand-extensions (function).
• simplify-nnf (function).
• symbolicate-form (function).
• to-anf (function).
• to-cnf (function).
• to-cnf-naive (function).
• to-cnf-tseytin (function).
• to-nnf (function).
• var (function).

Internals

• %merge-same-clauses (function).
• %sort-clauses (function).
• %to-anf (function).
• %to-nnf (function).
• clause< (function).
• dispatch (function).
• negate (function).
• symbol< (function).
• symbol<= (function).

---

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

• +random-string-size-min+ (special variable).
• +temp-file-attempts+ (special variable).
• attempt-create-temp (function).
• create-nonexisting (function).
• format1 (function).
• generate-temp-name (function).
• random-base62 (function).

---

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

• *instance* (special variable).
• initialize-instance (method).
• sat-instance (class).
• solve (generic function).
• variables (generic function).

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

• *verbosity* (special variable).
• parse-assignments (function).
• parse-dimacs-output (function).
• print-cnf (function).

---

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

• print-object (method).
• solve (method).

Internals

• *base-url* (special variable).
• build-error (condition).
• chmod-error (condition).
• competition-setup-error (condition).
• download-error (condition).
• download-solver (function).
• unzip-error (condition).

---

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

• cnf.
• initialize-instance.
• solve.
• variables.
• variables.

Direct slots

Slot: cnf ¶

Initargs

:cnf

Readers

cnf.

Writers

This slot is read-only.

Slot: %variables ¶

---

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

• build-error.
• chmod-error.
• download-error.
• unzip-error.

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.

---