;;;
;;; Propositional Logic Satisfiability Tools
;;;
;;; Sentences are implemented here as pre-order trees of symbols.
;;; Logical operators include the following list of symbols:
;;;
;;;   "AND", "^"        = n-ary conjunction
;;;   "OR", "V"         = n-ary disjunction
;;;   "NOT", "~"        = unary negation
;;;   "IMPLIES", "=>"   = implication
;;;   "EQUIV", "<=>"    = equivalence
;;;
;;; So, an example 3SAT sentence would be:
;;;
;;;   (and (or P       Q       (not S))
;;;        (or (not P) Q       R      )
;;;        (or (not P) (not R) (not S))
;;;        (or P       (not S) Tee    ))
;;;
;;; This may also be written as:
;;;
;;;   (^ (V  P     Q     (~ S))
;;;      (V  (~ P) Q     R    )
;;;      (V  (~ P) (~ R) (~ S))
;;;      (V  P     (~ S) Tee  ))
;;;
;;; Many of the routines in this package work only on sentences
;;; using the operators "AND", "OR", and "NOT", and no others, but
;;; a function is provided which translates all other sentences 
;;; into this form.
;;;
;;; This package provides tools for evaluating and generating such
;;; sentences.  Assignments of truth values to propositions are
;;; maintained in a simple manner, using an association list.
;;;
;;; Essentially none of this code has been optimized for 3SAT (as
;;; opposed to general propositional logic sentences).  These tools
;;; would run much faster if, for example, the truth value of
;;; each clause was maintained separately and pointers were available
;;; from atomic propositions to the clauses which include them.
;;; 
;;; DAVID NOELLE  Wed May  8 16:59:23 1996
;;;


;;;
;;; Package
;;;

(cl::defpackage "SAT"
  (:export "^"
	   "V"
	   "~"
	   "IMPLIES"
	   "=>"
	   "EQUIV"
	   "<=>"
           "ASSIGN-TRUTH-VALUE"
	   "GET-TRUTH-VALUE"
	   "TOGGLE-TRUTH-VALUE"
	   "MAKE-ALL-FALSE"
	   "MAKE-RANDOM-ASSIGNMENT"
	   "PRINT-TRUTH-ASSIGNMENT-LIST"
	   "CANONICALIZE-SENTENCE"
	   "EXTRACT-ATOMS"
	   "EVALUATE-SENTENCE"
	   "IS-3CNF-P"
	   "MAKE-RANDOM-3CNF-SENTENCE"
	   "NUMBER-OF-SATISFIED-3CNF-CLAUSES"
	   "RANDOM-WALK-SAT"))

(cl::in-package "SAT")


;;;
;;; Truth Assignment Lists
;;;

;;; assign-truth-value  --  Assign the given truth value to the given
;;; proposition in the given truth assignment list.  Note that the
;;; given alist is not copied, but is modified directly.  It is 
;;; important, therefore, to always update any pointers to the current
;;; assignment list to whatever this function returns.
(defun assign-truth-value (proposition truth-value alist)
  (declare (type symbol proposition truth-value)
	   (type list alist))
  (let ((binding 
	 (or (assoc proposition alist)
	     (let ((new-binding (cons proposition nil)))
	       (declare (type cons new-binding))
	       (push new-binding alist)
	       new-binding))))
    (declare (type cons binding))
    (setf (cdr binding) truth-value)
    alist))

;;; get-truth-value  --  Return the truth value of the given proposition
;;; in the given truth assignment list.
(defun get-truth-value (proposition alist)
  (declare (type symbol proposition)
	   (type list alist))
  (cdr (assoc proposition alist)))

;;; toggle-truth-value  --  This is essentially identical to:
;;;   (assign-truth-value p (not (get-truth-value p alist)) alist)
;;; It will run a little faster than this nested form, however.
;;; Note that the given alist is not copied, but is modified directly.
(defun toggle-truth-value (proposition alist)
  (declare (type symbol proposition)
	   (type list alist))
  (let ((binding 
	 (or (assoc proposition alist)
	     (let ((new-binding (cons proposition nil)))
	       (declare (type cons new-binding))
	       (push new-binding alist)
	       new-binding))))
    (declare (type cons binding))
    (setf (cdr binding) (not (cdr binding)))
    alist))

;;; make-all-false  --  Constructs and returns a truth assignment list
;;; for the given atomic propositions, initializing all truth assignments
;;; to false.
(defun make-all-false (propositions)
  (declare (type list propositions))
  (let ((alist nil))
    (declare (type list alist))
    (dolist (p propositions)
      (setq alist (assign-truth-value p nil alist)))
    alist))

;;; make-random-assignment  --  Constructs and returns a truth assignment
;;; list for the given atomic propositions, initializing all truth 
;;; assignments to random values.
(defun make-random-assignment (propositions)
  (declare (type list propositions))
  (let ((alist nil))
    (declare (type list alist))
    (dolist (p propositions)
      (setq alist (assign-truth-value p (= (random 2) 0) alist)))
    alist))

;;; print-truth-assignment-list  --  Print out the contents of a truth
;;; assignment list.
(defun print-truth-assignment-list (alist &optional (stream t))
  (declare (type list alist))
  (loop
    for binding in alist
    do
    (format stream 
	    "~&~S = ~A~&" 
	    (car binding) (if (cdr binding) "TRUE" "FALSE")))
  nil)


;;;
;;; Sentence Canonicalization And Evaluation
;;;

;;; canonicalize-sentence  --  Translate the given sentence into one
;;; that uses only "AND", "OR", and "NOT" operators.
(defun canonicalize-sentence (s)
  (declare (type (or symbol list) s))
  (if (symbolp s)
    s
    (case (first s)
      ((and ^) 
       (cons 'and (mapcar #'canonicalize-sentence (rest s))))
      ((or V)  
       (cons 'or  (mapcar #'canonicalize-sentence (rest s))))
      ((not ~)
       (when (cddr s)
	 (format *error-output* 
		 "~&Warning:  Ignoring extra arguments to negation - ~S.~&"
		 s))
       (list 'not (second s)))
      ((implies =>)
       (when (cdddr s)
	 (format *error-output*
		 "~&Warning:  Ignoring extra arguments to implication - ~S.~&"
		 s))
       (list 'or 
	     (list 'not (canonicalize-sentence (second s)))
	     (canonicalize-sentence (third s))))
      ((equiv <=>)
       (when (cdddr s)
	 (format *error-output*
		 "~&Warning:  Ignoring extra arguments to equivalence - ~S.~&"
		 s))
       (let ((p1 (canonicalize-sentence (second s)))
	     (p2 (canonicalize-sentence (third s))))
	 (declare (type (or symbol list) p1 p2))
	 (list 'and
	       (list 'or
		     (list 'not p1)
		     p2)
	       (list 'or
		     (list 'not (copy-tree p2))
		     (copy-tree p1)))))
      (otherwise
       (format *error-output* "~&Warning:  Unknown operator ~S.~&" (first s))
       s))))

;;; extract-atoms  --  Returns a list of the atomic propositions in
;; the given sentence.
(defun extract-atoms (s)
  (declare (type (or symbol list) s))
  (unless (or (eq s t) (eq s nil))
    (if (symbolp s)
      (list s)
      (if (listp s)
	(delete-duplicates
	 (apply #'nconc (mapcar #'extract-atoms (rest s))))
	(progn
	  (format *error-output* 
		  "~&Warning:  Unknown object ~S disregarded.~&"
		  s)
	  nil)))))

;;; evaluate-sentence  --  Determine the truth value of the given sentence
;;; using the given truth assignment list for the values of atomic
;;; propositions.  The sentence should have previously been canonicalized.
(defun evaluate-sentence (s alist)
  (declare (type (or symbol list) s)
	   (type list alist))
  (progv (mapcar #'car alist) (mapcar #'cdr alist)
    (eval s)))


;;;
;;; 3CNF Sentence Tools
;;;

;;; is-3cnf-p  --  Returns non-nil iff the given sentence is canonicalized
;;; and in 3-CNF format.
(defun is-3cnf-p (s)
  (declare (type (or symbol list) s))
  (and (listp s)
       (eq (first s) 'and)
       (loop
	 for clause in (rest s)
	 always 
	 (and (listp clause)
	      (eq (first clause) 'or)
	      (= (list-length (rest clause)) 3)
	      (loop
		for literal in (rest clause)
		always
		(or (symbolp literal)
		    (and (listp literal)
			 (= (list-length (rest literal)) 1)
			 (eq (first literal) 'not)
			 (symbolp (second literal)))))))))

;;; make-random-3cnf-sentence  --  Returns a random sentence in 3-CNF
;;; format.  The number of atomic propositional symbols and the number
;;; of clauses are specified as arguments.
(defun make-random-3cnf-sentence (n c)
  (declare (type fixnum n c))
  (when (> n (* 3 c))
    (format *error-output* 
	    "~&Error:  ~D symbols cannot appear in only ~D 3-clauses."
	    n c)
    (return-from make-random-3cnf-sentence nil))
  (flet ((select-random-literal (l &optional (size (list-length l)))
            (let ((proposition (nth (random size) l)))
	      (declare (type symbol proposition))
	      (if (= (random 2) 0)
		(list 'not proposition)
		proposition))))
    (let ((atoms (loop repeat n collect (gentemp "P-")))
	  (sentence nil)
	  (clause nil))
      (declare (type list atoms sentence clause))
      (loop 
	do
	(setq sentence
	      (cons 'and 
		    (loop 
		      repeat c collect
		      (loop
			do
			(setq clause
			      (list 'or
				    (select-random-literal atoms n)
				    (select-random-literal atoms n)
				    (select-random-literal atoms n)))
			;; Make sure that no duplicate literals appear ...
			until (= (list-length 
				  (remove-duplicates (rest clause) 
						     :test #'equalp))
				 3)
			finally (return clause)))))
	;; Make sure that all atoms appear at least once ...
	until (= (list-length (extract-atoms sentence)) n))
      sentence)))

;;; number-of-satisfied-3cnf-clauses  --  Returns the number of clauses 
;;; in the given 3-CNF sentence which are satisfied by the bindings in 
;;; the given truth assignment list.  Assumes that the sentence is in 
;;; canonical 3-CNF form.
(defun number-of-satisfied-3cnf-clauses (s alist)
  (declare (type (or symbol list) s)
	   (type list alist))
  (progv (mapcar #'car alist) (mapcar #'cdr alist)
    (loop
      for clause in (rest s) 
      count (eval clause))))


;;;
;;; Solve Satisfiability Problems By Random Walk
;;;

;;; random-walk-sat  --  Attempts to check the satisfiability of the
;;; given sentence by randomly walking through possible truth assignments.
;;; Optional arguments determine the length of the walk before restarting
;;; from a random assignment, and the number of restarts before declaring
;;; unsatisfiability.
(defun random-walk-sat (sentence &optional (max-restarts 0) (max-steps nil))
  (declare (type (or symbol list) sentence)
	   (type fixnum max-restarts)
	   (type (or fixnum null) max-steps))
  (let* ((s (canonicalize-sentence sentence))
	 (propositions (extract-atoms s))
	 (number-of-atoms (list-length propositions))
	 (maximum-steps (or max-steps (* 10 number-of-atoms)))
	 (assignments nil))
    (declare (type (or symbol list) s)
	     (type list propositions)
	     (type fixnum number-of-atoms maximum-steps)
	     (type list assignments))
    (format t "~&Executing SAT Random Walk on the canonicalized sentence:")
    (format t "~&~S~&Max Restarts:  ~D     Max Steps:  ~D~&~%"
	    s max-restarts maximum-steps)
    (time
     (block whole-search
       (loop
	 repeat (+ max-restarts 1) do
	 (setq assignments (make-random-assignment propositions))
	 (loop
	   repeat maximum-steps do
	   ;; Toggle a random proposition ...
	   (setq assignments
		 (toggle-truth-value 
		  (nth (random number-of-atoms) propositions)
		  assignments))
	   (when (evaluate-sentence s assignments)
	     (return-from whole-search))))
       ;;; Completed search without finding a satisfactory assignment ...
       (setq assignments nil)))
    (format t "~&~%Solution:")
    (if assignments
      (print-truth-assignment-list assignments)
      (format t "  no satisfying truth assignment found."))
    (format t "~&~%")
    assignments))