;;; This file defines a problem "SAT" which describes a search space over
;;; a satisfiability. A state contains the problem in CNF form (described below)
;;; and an association list of the variables which have been set with their
;;; truth values.
;;;
;;; The user should call set-problem to set the problem. Then, call search with
;;; the initial state set to the return value of get-initial and goal-p and get-next
;;; used as the goal checking and generating functions.
;;;
;;; The solution extracted by the search can be passed to get-solution which will
;;; return NULL if the state is not a solution or the assoc list representing the
;;; solution assignments otherwise.
;;;
;;; CNF problems are of the form:
;;;
;;; <problem> -> '(' <clause>* ')'
;;; <clause>  -> '(' <literal>* ')'
;;; <literal> -> <var> | '(' 'not' <var> ')'
;;; <var>     -> a symbol
;;;
;;; No clause should contain the same literal twice.
;;;
;;; Solutions are in the form of an association list from variables
;;; to T or NIL values. You should use the association list access methods
;;; to deal with a solution. Also, note that if a variable is unassigned
;;; in the solution (i.e., does not appear in the association list), either
;;; of its values is consistent with the solution. It is not constrained to
;;; be either true or false.
;;;
;;; Note that within SAT, a "problem" is a CNF formula. Outside SAT a "problem"
;;; is a search state. Sorry about this ambiguity.. wouldn't a typed language be
;;; neat?


;; State struct is used to store the current state
(defstruct state
   (problem NIL)    ; a list of clauses
   (assignment NIL) ; an association list of assignments
   )

(defun copy-state (state)
   (make-state
      :problem (copy-tree (state-problem state))
      :assignment (copy-alist (state-assignment state))))
    
(let ((problem NIL)             ; The problem in CNF form as described above
      (unit-vars NIL))          ; List storing current set of unit variables
   ;; Set the problem to prob   
   (defun set-problem (prob)
      (setf problem prob))

   ;; Returns the current problem.   
   (defun get-problem ()
      problem)

   ;; Get the solution described by state
   (defun get-solution (state)
      (if (or
              (null state)
              (not (state-p state)))
         NIL
         (state-assignment state)))
   
   ;; Get the initial state specified by prob
   (defun get-initial ()
      (let ((init (make-state :problem problem)))
         (init-unit-prop init)
         ))
   
   ;; Check if state is a goal (is it an empty statement?)
   (defun goal-p (state)
      (null (state-problem state)))

   ;; Returns the variable in the given literal
   (defun get-var (lit)
      (if (not (is-pos lit))
         (second lit)
         lit))
   
   ;; Returns T if the literal is positive, NIL
   ;; if it's negated.
   (defun is-pos (lit)
      (or (not (listp lit))
          (not (eq (first lit) 'NOT))))
         
   ;; Creates a literal from the variable and the is-positive
   ;; setting
   (defun make-lit (var value)
      (if value
         var
         (list 'not var)))
   
   ;; Get the next state list. If there is a
   ;; null clause in problem, then it is an unsolveable
   ;; problem (because there's no way to satisfy one of 
   ;; the clauses), so return no next states. Otherwise,
   ;; pick the first available variable and set it to
   ;; both true and false.
   (defun get-next (state)
      (let ((problem (state-problem state)))
         (if (or
                 (null problem)
                 (member NIL problem))
            NIL
            ;; Choose the first available variable. Strip the
            ;; NOT off negated lits.
            (let* ((chosen-lit (first (first problem)))
                   (chosen-var (get-var chosen-lit))
                   (state-true (copy-state state))
                   (state-false (copy-state state)))
               (list
                  (unit-prop (set-var-state chosen-var T state-true))
                  (unit-prop (set-var-state chosen-var NIL state-false)))))))

   ;; Find any unit clauses that might exist and put their vars
   ;; on the unit-var list. Then, propogate them away.
   (defun init-unit-prop (state)
      (setf unit-vars (find-units (state-problem state)))
      (unit-prop state))
   
   ;; Find any unit clauses in the given list. 
   (defun find-units (problem &optional (unit-vars-so-far NIL))
      (if (null problem)
         unit-vars-so-far
         (let ((clause (first problem)))
            (if (and
                     (not (null clause))
                     (null (rest clause)))
               (find-units (rest problem) (cons (cons (get-var (first clause))
                                                   (is-pos (first clause))) 
                                             unit-vars-so-far))
               (find-units (rest problem) unit-vars-so-far)))))
   
   ;; Destructively propagate unit variables in state. Do
   ;; not check for contradictions.
   (defun unit-prop (state)
      (setf state (inner-unit-prop state))
      state)
   
   ;; Destructively propagate unit variables in problem.
   (defun inner-unit-prop (state)
      (if (not (null unit-vars))
         (let ((chosen-var (first (first unit-vars)))
               (chosen-val (rest (first unit-vars))))
            (setf unit-vars (rest unit-vars))
            (setf state (set-var-state chosen-var chosen-val state))
            (inner-unit-prop state))
         state))
      
   ;; Destructively modify the problem to reflect setting
   ;; var to value and update the unit variable list. Problem-so-far is
   ;; an accumulator.
   (defun set-var (var value problem &optional (problem-so-far NIL))
      (if (null problem)
         problem-so-far
         (let ((clause (first problem)))
            (if (member (make-lit var value) clause :test #'equalp)
               (set-var var value (rest problem) problem-so-far)
               (set-var var value (rest problem) (cons (strip-var 
                                                          clause 
                                                          (make-lit var (not value)))
                                                    problem-so-far))))))

   ;; strips a variable from a clause. Keeps track of potential unit variable
   (defun strip-var (clause lit &optional (clause-so-far NIL))
      (cond
            ((null clause) 
             (when (and (not (null clause-so-far))
                        (null (rest clause-so-far)))
                (setf unit-vars (cons (cons (get-var (first clause-so-far))
                                         (is-pos (first clause-so-far)))
                                   unit-vars)))
             clause-so-far)
            ((equalp lit (first clause)) 
             (strip-var (rest clause) lit clause-so-far))
            (T (strip-var (rest clause) lit (cons (first clause) clause-so-far)))))
   
   ;; Destructively modify the state to reflect setting 
   ;; var to value.
   (defun set-var-state (var value state)
      (let ((assg (state-assignment state)))
         (setf assg (acons var value assg))
         (setf (state-assignment state) assg)
         (setf (state-problem state) (set-var var value (state-problem state)))
         state
      ))
   )