sat.clj

;Code from http://peteriserins.com/2011/12/23/sat-in-clojure-core-logic.html

;; lein try org.clojure/core.logic "0.8.8"

(require '[clojure.core.logic :refer [conde run* fresh ] :as l])

(declare goalify)

(defn and-rewrite [expr]
  `(conde
    (~(goalify (second expr))
     ~(goalify (second (rest expr))))))

(defn or-rewrite [expr]
  `(conde
    (~(goalify (second expr)))
    (~(goalify (second (rest expr))))))

(defn demorgan [subexpr]
  (if (and (seq? subexpr)
           (= 'not (first subexpr)))
    (second subexpr)
    (cons 'not (list subexpr))))

(defn not-rewrite [expr]
  (let [expr (second expr)]
    (cond
     (symbol? expr)
     `(l/== ~expr false)
     (= 'not (first expr))
     (goalify (second expr))
     (= 'and (first expr))
     (goalify (cons 'or  (map demorgan (rest expr))))
     (= 'or (first expr))
     (goalify (cons 'and (map demorgan (rest expr)))))))

(defn goalify [expr]
  "Turns boolean expressions into core.logic goals"
  (cond
   (symbol? expr)
   `(l/== ~expr true)
   (= 'and (first expr))
    (and-rewrite expr)
   (= 'or (first expr))
    (or-rewrite expr)
   (= 'not (first expr))
    (not-rewrite expr)))

(defmacro sat [vars expr] 
  "SAT"
  `(run* [q#]
         (fresh ~vars
                ~(goalify expr)
                (l/== q# ~vars))))
;Usage

(sat [p] (and p (not p)))
;=> ()

(sat [p q] (not (and (or (not p) q)
                     q)))
;=> ([_.0 false] [true false])