## cl-sat

2022-07-08

Common Lisp API to Boolean SAT Solvers

# 1CL-SAT - Common Lisp API to Boolean SAT Solvers

https://travis-ci.org/cl-model-languages/cl-sat.svg?branch=master

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`

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

## 1.1Usage

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

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

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

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

- Single compound forms:
`(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.

## 1.6Dependencies

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

## 1.7Author

- Masataro Asai (guicho2.71828@gmail.com)

# 2Copyright

Copyright (c) 2016 Masataro Asai (guicho2.71828@gmail.com)

# 3License

Licensed under the LLGPL License.