Max-WalkSAT (MWS) weighted satisfiability solver

mws.clj

; 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 ([email protected])
;
; 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))