; MaxWalkSAT weighted satisfiability solver ; ; A General Stochastic Approach to Solving Problems with Hard and Soft ; Constraints Henry Kautz, Bart Selman, and Yueyen Jiang. In The ; Satisfiability Problem: Theory and Applications, Dingzhu Gu, Jun Du, ; and Panos Pardalos (Eds.), DIMACS Series in Discrete Mathematics and ; Theoretical Computer Science, vol. 35, American Mathematical Society, ; 1997, pages 573-586. ; ; ; David Andrzejewski (andrzeje@cs.wisc.edu) ; ; Command-line arguments ; 0 propositional clauses filename ; 1 parameter settings filename ; ; EX: clj mws.clj test.clauses test.param ; (use '[clojure.contrib.duck-streams :only (read-lines)]) (use '[clojure.contrib.seq-utils :only (indexed)]) (use 'clojure.set) (def rng (new java.util.Random)) (defstruct logicclause :weight :atoms) (defstruct logicatom :inverted :predicate) (defstruct solution :pvals :satweight :unsat) ; Parameter data structure (defstruct parameters :numiter :prand :P) ; Parameter names and parsing functions (def parameter-processing (hash-map "numiter" (list :numiter #(Integer/parseInt %1)) "prand" (list :prand #(Float/parseFloat %1)) "P" (list :P #(Integer/parseInt %1)))) ; Verbose output of intermediate steps (def verbosity true) (defn affects? "Does predicate p affect clause c?" [p c] (some #(= (:predicate %1) p) (:atoms c))) (defn update-pvals "Return pvals with flip flipped" [pvals flip] (assoc pvals flip (not (nth pvals flip)))) (defn eval-atom "Evaluate atom truth value" [pvals a] (if (:inverted a) (not (nth pvals (:predicate a))) (nth pvals (:predicate a)))) (defn eval-clause "Evalute clause truth value" [pvals c] (some (partial eval-atom pvals) (:atoms c))) (defn sat-weight "Total weight of satisfied clauses" [clauses pvals] (reduce + (map :weight (filter (partial eval-clause pvals) clauses)))) (defn parse-atom "Integer < P optionally preceded by ~ for negation (EX: ~2 or 4)" [astr] (if (. astr startsWith "~") (struct logicatom true (Integer/parseInt (. astr substring 1))) (struct logicatom false (Integer/parseInt astr)))) (defn parse-line "Clause weight followed by atoms, whitespace separated" [line] (let [[weight & atoms] (.split line "\\s+")] (struct logicclause (Float/parseFloat weight) (map parse-atom atoms)))) (defn valid-line "Is this line 1) non-whitespace? and 2) not a comment?" [commentchar line] (and (not (zero? (.. line trim length))) (nil? (re-matches (re-pattern (str "^\\s*\\" commentchar ".*")) line)))) (defn read-clause-file "Read file with 1 line per clause" [filename] (map parse-line (filter (partial valid-line "#") (read-lines filename)))) (defn unsat-clauses "Which clauses are unsat for predicate values pvals?" [pvals clauses] (set (filter #(not (eval-clause pvals %1)) clauses))) (defn get-pred-effect "For this predicate, which clauses does it affect?" [clauses p] (set (filter (partial affects? p) clauses))) (defn rand-select "Randomly select an element from (non-infinite) collection" [coll] (nth (vec coll) (. rng nextInt (count coll)))) (defn rand-pred [c] "Randomly choose a predicate in clause c" (let [catoms (vec (:atoms c))] (:predicate (nth catoms (. rng nextInt (count catoms)))))) (defn flip-score "What is the score delta of flipping predicate p?" [pvals peffect flip] (let [cset (nth peffect flip)] (- (sat-weight cset (update-pvals pvals flip)) (sat-weight cset pvals)))) (defn greedy-pred "Find the greedy local move to sat clause c" [c pvals peffect] (apply max-key (partial flip-score pvals peffect) (map :predicate (:atoms c)))) (defn get-move [runparam cursoln peffect] "Get the next local move (greedy or random)" (let [c (rand-select (:unsat cursoln))] (if (< (. rng nextFloat) (:prand runparam)) (rand-pred c) (greedy-pred c (:pvals cursoln) peffect)))) (defn update-unsat "Update set of unsatisfied clauses after flipping flip" [unsat pvals peffect flip] (let [affected (nth peffect flip) newpvals (update-pvals pvals flip)] (union (difference unsat affected) (unsat-clauses newpvals affected)))) (defn rand-bool-vec "A random boolean vector of length L" [L] (vec (for [pi (range L)] (. rng nextBoolean)))) (defn update-solution "Update a solution by flipping" [soln flip peffect] (let [delta (flip-score (:pvals soln) peffect flip)] (if verbosity (println (format "flip %d (delta=%f)" flip delta))) (struct solution (update-pvals (:pvals soln) flip) (+ (:satweight soln) delta) (update-unsat (:unsat soln) (:pvals soln) peffect flip)))) (defn max-walk-sat "The MaxWalkSAT weighted satisfiability solver" [runparam clauses peffect initsoln] (loop [cursoln initsoln ; current solution bestsoln initsoln ; best solution found thus far ctr (:numiter runparam)] ; how many iter left? (if verbosity (do (println (format "Best SAT weight = %f" (:satweight bestsoln))) (print (format "Step %d " (- (:numiter runparam) ctr))))) ; Stop when all clauses are satisfied, or we've done all iterations (if (or (zero? ctr) (empty? (:unsat cursoln))) bestsoln (let [flip (get-move runparam cursoln peffect) newsoln (update-solution cursoln flip peffect)] (recur newsoln (if (> (:satweight newsoln) (:satweight bestsoln)) newsoln bestsoln) (dec ctr)))))) (defn print-solution "Print the results of a solution" [solution clauses] (doseq [[p pval] (indexed (:pvals solution))] (println (format "pred %d = %b" p pval))) (println (format "%d of %d clauses satisfied (satweight = %f)" (- (count clauses) (count (:unsat solution))) (count clauses) (:satweight solution)))) (defn parse-param-line "Parse a line of the parameters file" [pline] (let [[pname pval] (. pline split "\\=") [psym pfcn] (get parameter-processing pname)] (list psym (pfcn pval)))) (defn read-param-file "Read the parameter file" [pfilename] (apply struct-map parameters (mapcat parse-param-line (read-lines pfilename)))) (let [clausefile (nth *command-line-args* 0) paramfile (nth *command-line-args* 1) runparam (read-param-file paramfile) clauses (read-clause-file clausefile) peffects (map (partial get-pred-effect clauses) (range (:P runparam))) pinit (rand-bool-vec (:P runparam)) initsoln (struct solution pinit (sat-weight clauses pinit) (unsat-clauses pinit clauses))] (print-solution (max-walk-sat runparam clauses peffects initsoln) clauses))