cl-model-languages / cl-sat.glucose

CL-SAT instance to Glucose state-of-the-art SAT solver. This downloads the later 2014 version (2nd in the 2014 SAT competition).
3 stars 0 forks source link

CL-SAT instance to Glucose state-of-the-art SAT solver.

See [[https://github.com/guicho271828/cl-sat][cl-sat]] for details.

This downloads the later 2014 version (2nd in the competition) from http://www.labri.fr/perso/lsimon/glucose/.

** Usage

See also: https://github.com/guicho271828/cl-sat

+BEGIN_SRC lisp

(cl-sat:solve '(and (or a b) (or a !b c)) :glucose) ;; -> ;; (C A) ;; T ;; T

+END_SRC

** Dependencies

Requires cURL and Make to download & build the binary.

This library is at least tested on implementation listed below:

Also, it depends on the following libraries:

** Installation

** Author

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

Licensed under the LLGPL License.