;; R. Williams
;; Artificial Intelligence
;; 
;; Implements the algorithm of Fig. 7.17 (p. 223) using local search to
;; try to find a satisfying assignment for a set of clauses (passed to
;; this function as a list of clauses).  In order for this code to run,
;; the file satisfiability.lisp must also be loaded since this code uses
;; some helpers from that file.

(setq *verbose-output* t)

(defun walksat (clauses &optional (p .5) (max-flips 1000))
  (let* ((vars (remove-duplicates
		(apply #'append (mapcar #'extract-vars clauses))))
	 (num-vars (length vars))
	 (vals (random-vals num-vars))
	 (truth-vals (combine-vars-and-vals vars vals)))
    (dotimes (i max-flips (failure-message max-flips))
      (let* ((unsat-clauses
	      (remove-if #'(lambda (c) (eval-truth c truth-vals)) clauses))
	     (count-unsat (length unsat-clauses)))
	(if (zerop count-unsat)
	    (return (success-message i truth-vals)))
	(let* ((candidate-clause (random-element unsat-clauses count-unsat))
	       (candidate-vars
		(remove-duplicates (extract-vars candidate-clause)))
	       (num-candidate-vars (length candidate-vars)))
	  (if (< (random 1.0) p)
	      (progn
		(if *verbose-output* (format t "~%Random flip"))
		(flip-value (random-element candidate-vars num-candidate-vars)
			    truth-vals))
	      (progn
		(if *verbose-output* (format t "~%Best flip"))
		(best-flip candidate-vars clauses truth-vals)))
	  )))))
	     
;; has side effect of changing the truth-vals argument
(defun best-flip (vars clauses truth-vals)
  (let (best-var
	(best-score (1+ (length clauses))))
    (dolist (var vars)
      (flip-value var truth-vals)
      (let ((this-score (score clauses truth-vals)))
	(if (< this-score best-score)
	    (progn
	      (setf best-score this-score)
	      (setf best-var var))))
      (flip-value var truth-vals)) ; flip it back to original value
    ;; finally, flip the var that gave the best score
    (flip-value best-var truth-vals)
    ))

(defun score (clauses truth-vals)
  (let ((num-unsat 0))
    (dolist (clause clauses num-unsat)
      (if (not (eval-truth clause truth-vals))
	  (incf num-unsat)))))

;; has side effect of changing the truth-vals argument
(defun flip-value (var truth-vals)
  (let* ((var-val-pair (assoc var truth-vals))
	 (val (cdr var-val-pair)))
    (setf (cdr var-val-pair) (not val))
    truth-vals))

(defun success-message (num-flips truth-vals)
  (format t "~%Found ~s in ~s flips." truth-vals num-flips))

(defun failure-message (max-flips)
  (format t "~%Found no satisfying assignment in ~s flips." max-flips))

(defun random-element (list list-len)
  (nth (random list-len) list))

(defun random-boolean ()
  (zerop (random 2)))

(defun random-vals (n)
  (cond ((zerop n) nil)
	(t (cons (random-boolean) (random-vals (1- n))))))

#| A test case:
(setq *clauses* '((or (not p) q) p))
(walksat *clauses*)
|#