random-walk-3-sat.clj

(defn rand-assign
  [n]
  (take n (repeatedly #(rand-nth [true false]))))

(defn clause-satisfied?
  [assign clause]
  (some #(= (nth assign (first %)) (second %)) clause))

(defn formula-satisfied?
  [assign formula]
  (every? (partial clause-satisfied? assign) formula))

(defn unsatisfied-clauses
  [assign formula]
  (filter (complement (partial clause-satisfied? assign))
          formula))

(defn rand-variable
  [clause]
  (rand-nth (keys clause)))

(defn swap-variable
  [assign variable]
  (concat (conj (vec (take variable assign))
                (not (nth assign variable)))
          (drop (inc variable) assign)))

(defn walk
  [assign formula]
  (when-not (formula-satisfied? assign formula)
    (swap-variable assign
                   (rand-variable
                     (first (unsatisfied-clauses assign formula))))))

(defn walk-repeatedly
  [assign formula n]
  (when-not (zero? n)
    (if-let [result (walk assign formula)]
      (recur result formula (dec n))
      true)))

(defn random-walk-3-sat
  [f n R]
  (if-not (zero? R)
    (if (walk-repeatedly (rand-assign n) f (* 3 n))
      "充足可能である"
      (recur f n (dec R)))
    "おそらく充足不可能である"))

(def formula
  [{0 true, 1 true, 2 true}
   {3 true, 1 true, 2 false}
   {0 false, 3 true, 2 true}
   {0 false, 3 false, 1 true}
   {3 false, 1 false, 2 true}
   {0 false, 1 false, 2 false}
   {0 true, 3 false, 2 false}
   {0 true, 3 true, 1 false}])

(println (random-walk-3-sat formula 4 3))