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

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

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

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.

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

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

- Author
- Masataro Asai
- License
- LLGPL