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.
The main system appears first, followed by any subsystem dependency.
cl-sat
Common Lisp API to Boolean SAT Solvers
Masataro Asai
LLGPL
0.1
trivia
(system).
alexandria
(system).
iterate
(system).
trivial-features
(system).
src/0-package.lisp
(file).
src/1-parse.lisp
(file).
src/1-util.lisp
(file).
src/2-class.lisp
(file).
src/3-dimacs.lisp
(file).
src/4-competition.lisp
(file).
Files are sorted by type and then listed depth-first from the systems components trees.
cl-sat/cl-sat.asd
cl-sat/src/0-package.lisp
cl-sat/src/1-parse.lisp
cl-sat/src/1-util.lisp
cl-sat/src/2-class.lisp
cl-sat/src/3-dimacs.lisp
cl-sat/src/4-competition.lisp
cl-sat/src/1-parse.lisp
src/0-package.lisp
(file).
cl-sat
(system).
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).
%merge-same-clauses
(function).
%sort-clauses
(function).
%to-anf
(function).
%to-nnf
(function).
clause<
(function).
dispatch
(function).
negate
(function).
symbol<
(function).
symbol<=
(function).
cl-sat/src/1-util.lisp
src/1-parse.lisp
(file).
cl-sat
(system).
with-temp
(macro).
+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).
cl-sat/src/2-class.lisp
src/1-util.lisp
(file).
cl-sat
(system).
*instance*
(special variable).
initialize-instance
(method).
sat-instance
(class).
solve
(generic function).
variables
(generic function).
cnf
(reader method).
cl-sat/src/3-dimacs.lisp
src/2-class.lisp
(file).
cl-sat
(system).
*verbosity*
(special variable).
parse-assignments
(function).
parse-dimacs-output
(function).
print-cnf
(function).
cl-sat/src/4-competition.lisp
src/3-dimacs.lisp
(file).
cl-sat
(system).
print-object
(method).
solve
(method).
*base-url*
(special variable).
build-error
(condition).
chmod-error
(condition).
competition-setup-error
(condition).
download-error
(condition).
download-solver
(function).
unzip-error
(condition).
Packages are listed by definition order.
cl-sat
sat
alexandria
.
common-lisp
.
iterate
.
trivia.level2
.
*instance*
(special variable).
*verbosity*
(special variable).
aux
(function).
expand-extensions
(function).
parse-assignments
(function).
parse-dimacs-output
(function).
print-cnf
(function).
sat-instance
(class).
simplify-nnf
(function).
solve
(generic function).
symbolicate-form
(function).
to-anf
(function).
to-cnf
(function).
to-cnf-naive
(function).
to-cnf-tseytin
(function).
to-nnf
(function).
var
(function).
variables
(generic function).
with-temp
(macro).
%merge-same-clauses
(function).
%sort-clauses
(function).
%to-anf
(function).
%to-nnf
(function).
*base-url*
(special variable).
+random-string-size-min+
(special variable).
+temp-file-attempts+
(special variable).
attempt-create-temp
(function).
build-error
(condition).
chmod-error
(condition).
clause<
(function).
cnf
(generic reader).
competition-setup-error
(condition).
create-nonexisting
(function).
dispatch
(function).
download-error
(condition).
download-solver
(function).
format1
(function).
generate-temp-name
(function).
negate
(function).
random-base62
(function).
symbol<
(function).
symbol<=
(function).
unzip-error
(condition).
Definitions are sorted by export status, category, package, and then by lexicographic order.
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.
intern a suffix to an auxiliary symbol
Translates extended logical operations into AND, OR, NOT.
IMPLY, =>, WHEN (synonyms),
IFF,
EQ, EQUAL, <=> (synonyms, a variation of IFF that takes multiple statements),
XOR.
Parser for Minisat 2.2
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 ... ...)
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.
Convert an arbitrary logical form into an algebraic normal form consisting of XOR, AND, and T.
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.
Convert a NNF into a flattened CNF via a naive method.
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.
Applying De-Morgan’s law, the resulting tree contains negations only at the leaf nodes. Calls expand-extensions internally.
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.
pathname
) (competition (eql :competition)
) &rest options &key debug year track name &allow-other-keys) ¶list
) solver &rest args &key converter &allow-other-keys) ¶sat-instance
) solver &rest args &key debug &allow-other-keys) ¶sat-instance
)) ¶sat-instance
)) ¶sat-instance
) &rest args &key form cnf converter &allow-other-keys) ¶competition-setup-error
) s) ¶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.
Attempts to create a file/directory, returns NIL if it exists already and T otherwise.
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.
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.
Simple negation not involving De-Morgan’s law.
Returns a random base62 string with n characters.
sat-instance
)) ¶automatically generated reader method
cnf
.
Jump to: | %
A C D E F G I M N P R S T V W |
---|
Jump to: | %
A C D E F G I M N P R S T V W |
---|
Jump to: | %
*
+
C N S T Y |
---|
Jump to: | %
*
+
C N S T Y |
---|
Jump to: | B C D F P S U |
---|
Jump to: | B C D F P S U |
---|