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


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)

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

S-exp -> CNF converter

The input list can be an arbitrary propositional formula containing or, and, not. AND and OR are sometimes implied (e.g. a single atom without any conjunction/disjunction). Negated/false atoms are specified by (not <atom>).

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.

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


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