cl-sat


* CL-SAT  - Common Lisp API to Boolean SAT Solvers

[[https://travis-ci.org/cl-model-languages/cl-sat][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= 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:
  + 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/
  + [[./competition.org][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

** Usage
   
In order to load and run minisat2, run follows:

#+begin_src lisp
(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
#+end_src

** Solver 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 true
  or false.

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

#+BEGIN_SRC lisp
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)) ...)
#+END_SRC

** S-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 negations
     only 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=.

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

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





alexandria

cl-sat

Upstream URL

Author

License

cl-sat

Version:

License:

Authors:

Dependencies:

cl-sat.test

License:

Authors:

Dependencies:

Dependencies (5)

Dependents (3)