Common Lisp API to Boolean SAT Solvers

Upstream URL


Masataro Asai



1CL-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:



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.
Implemented a :COMPETITION keyword for the generic functionSOLVE, which accepts :year, :track, :name argumentspecifying 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:
  • 2017:
  • 2017:
  • Here is the list of solvers that worked.
the input formula can now contain (IMPLY lhs rhs) and (IFF lhs rhs).
the input formula can contain more operations. See description below


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)

(ql:quickload :cl-sat.glucose)

(cl-sat:solve '(and (or a b) (or a !b c)) :glucose)
(C B)

(cl-sat:solve '(and (or a b) (or a !b c)) :competition :year 2018 :track "main_and_glucose_hack" :name "Lingeling")
(C B A)

1.2Solver 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 trueor false.

1.3Input 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.


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

1.4S-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 negationsonly 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.

1.5Helper 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.


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


  • Masataro Asai (


Copyright (c) 2016 Masataro Asai (


Licensed under the LLGPL License.

Dependencies (5)

  • alexandria
  • fiveam
  • iterate
  • trivia
  • trivial-features
  • GitHub
  • Quicklisp