This is the cl-sat Reference Manual, version 0.1, generated automatically by Declt version 3.0 "Montgomery Scott" on Mon Dec 02 09:45:55 2019 GMT+0.
|• Introduction||What cl-sat is all about|
|• Systems||The systems documentation|
|• Files||The files documentation|
|• Packages||The packages documentation|
|• Definitions||The symbols documentation|
|• Indexes||Concepts, functions, variables and data types|
* 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: + 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