test.clj

(defn lookup
  "Lookup a variable in the model.  Respects inversion of the variable if it is
  specified with a - symbol.  Returns nil if the variable is unset."
  [[first-char :as var] model]
  (if (= first-char \-)                         ; If the first character is '-'
    (if-let [[_ val] (find model (subs var 1))] ; test for existence
      (not val)                                 ; invert value if exists
      nil)                                      ; otherwise return nil
    (get model v)))

(def foobar {"A" false, "B" true})

(println "should return false:" (lookup "A" foobar))
(println "should return false:" (lookup "-B" foobar))
(println "should return true:" (lookup "B" foobar))
(println "should return nil:" (lookup "-C" foobar))

(defn satisfiable?
  "Checks to see if a given clause is satisfiable given a model."
  [clause, model]
  ;; Test all clauses
  (let [lookups (map #(lookup % model) clause)]
    (cond (every? false? lookups) false
          (some true? lookups) true
          :otherwise nil)))

(def barbaz '("A" "-B"))
(def buzfuz '("-A" "-B"))
(def sprangadang '("A" "-B" "C"))

(println "should return false:" (satisfiable? barbaz foobar))
(println "should return true:" (satisfiable? buzfuz foobar))
(println "should return nil:" (satisfiable? sprangadang foobar))


(defn solve
  "Solves some set of clauses recursively, given some model and some list of
  variables present in the clauses."
  [variables, clauses, model]
  (let [satisfied-result (map #(satisfiable? % model) clauses)]
    ;; If every clause is satisfiable, the set of clauses is satisfied by the
    ;; current model, so we should return it.
    (cond (every? true? satisfied-result) model
          ;; If some clause can't be satisfied, the set is not satisfiable given
          ;; this model.
          (some false? satisfied-result) false
          :otherwise ;; choose the first variable that is not yet defined
          (let [choice (first (filter #(nil? (lookup % model)) variables))]
            (if (nil? choice) false
                ;; And try setting it to true; if that doesn't work, try false.
                (or
                 (solve variables clauses (assoc model choice true))
                 (solve variables clauses (assoc model choice false))))))))

(def rock '(("A" "-B") ("-A" "-B")))
(def paper '(("A" "-B") ("-A" "-B") ("A" "B" "C")))
(def scissors '(("-A" "B") ("-B") ("A")))

(println "should return a model:" (solve '("A" "B") rock {}))
(println "should return a model:" (solve '("A" "B" "C") paper {}))
(println "should return false:" (solve '("A" "B") scissors {}))