CL-SAT - Common Lisp API to Boolean SAT Solvers

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 <form> :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/
• 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:

(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

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:

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)) ...)

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.