The cl-sat Reference Manual

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 4.0 beta 2 "William Riker" on Mon Aug 15 03:58:36 2022 GMT+0.

Table of Contents


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.

2 Systems

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


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

2.1 cl-sat

Common Lisp API to Boolean SAT Solvers

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

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.


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

3.1 Lisp


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

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.


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

4.1 cl-sat.aux-variables

Source

src/1-parse.lisp.


4.2 cl-sat

Source

src/0-package.lisp.

Nickname

sat

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

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

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.


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

5.1 Public Interface


Next: , Previous: , Up: Public Interface   [Contents][Index]

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


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

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.


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

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.


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

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


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

A.1 Concepts


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

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

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

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

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

Jump to:   B   C   D   F   P   S   U