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:


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.


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

solver API

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.

S-exp -> CNF converter

The input list is interpreted as a CNF formula. AND and OR are sometimes implied. Negated/false atoms are specified by NOT.

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 treated as false atoms.


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


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.

Masataro Asai