;;-------------------------------------------------------------------------
;; Stubs of functions students should write for WalkSAT implementation,
;; Homework 4, CMSC 471, Fall 2009

;; Should be a fairly straightforward rewriting of the
;; pseudocode given by Russell & Norvig.  You'll want
;; to start by using COLLECT-VARS to get a list of all of
;; the variables in the clauses.
;; Hints:  
;;   Look at the functions I've provided in walksat-utils.lisp
;;     and the other stubs below -- most of the steps in the
;;     pseudocode WalkSAT algorithm can be done by calling one
;;     of those functions.
;;   A good way to do action A "with probability p" is to
;;     generate a random number between 0 and 1, and perform
;;     action A if the random number is between 0 and p.
(defun walksat (clauses p max_flips)
  "Implements the WalkSAT algorithm as shown in R&N Figure 7.17.
   Returns two values:  the satisfying model (or NIL if none found) 
   and the number of assignments tried (in the range [1, MAX_FLIPS])"
  )


;; Hint:  See note in walksat-utils.lisp about Lisp's RANDOM
;; function.  (random 0.5) may be useful here.
(defun random-assts (vars)
  "Create a set of random assignments."
  )

;; Hint: you probably want to write FALSE-CLAUSES first
;; and use it here.  RANDOM-ELEMENT may also be useful.
(defun random-false-clause (model clauses)
  "Select a random clause from CLAUSES that is not satisfied by MODEL"
  )

;; Hint: it may be useful to use SATISFIES-ONE
(defun false-clauses (model clauses)
  "Return a list of all clauses in CLAUSES that are not satisfied by MODEL"
  )

;; Hint:  There's no particular reason to try to be efficient
;; or clever here.  How I implemented it:  Call FALSE-CLAUSES
;; to get a list of all of the false clauses.  
;; Then iterate through the list of variables, generating the
;; model that results from flipping each one, and call 
;; COUNT-SATISFIES to get the number of false clauses for
;; each of these new models.  Keep track of which variables
;; result in the smallest number of unsatisfied clauses.
;; If there is a tie, return one of these "max-sat" (equivalently,
;; "min-false-clause") variables at random.

(defun choose-max-sat (vars clauses model)
  "Return the variable that maximizes the number of satisfied clauses 
when flipped"
  )