Skip to content

Instantly share code, notes, and snippets.

@omasanori
Created May 8, 2011 05:17
Show Gist options
  • Save omasanori/961132 to your computer and use it in GitHub Desktop.
Save omasanori/961132 to your computer and use it in GitHub Desktop.
(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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment