;;; Finds all satisfying assignments for a given propositional calculus
;;; sentence by checking every row in the truth table.
;;;
;;; The sentence is not assumed to be in CNF or any other normalized form,
;;; but it is assumed to be well-formed and contain only AND, OR, NOT,
;;; and IF expressions.

(defun exhaustive-check-satisfiability (sentence)
  (let* ((vars (extract-vars sentence))
	 (num-vars (length vars))
	 (vals (make-list num-vars)) ; initially all nils
	 )
    (dotimes (i (expt 2 num-vars))
      (let ((truth-vals (combine-vars-and-vals vars vals)))
	(if (eval-truth sentence truth-vals)
	    (format t "~%Satisfied by: ~s" truth-vals))
	(setf vals (next-vals vals)))
      )))

;; returns an association list of var/val dotted pairs
(defun combine-vars-and-vals (vars vals)
  (mapcar #'cons vars vals))

;; extracts a list of variables from an expression representing
;; a propositional calculus sentence
(defun extract-vars (form)
  (if (atom form) (list form)
      (set-difference
       (remove-duplicates
	(flatten form))
       '(t nil and or not if))))

(defun flatten (expr)
  (cond
   ((atom expr) expr)
   ((atom (first expr)) (cons (first expr) (flatten (rest expr))))
   (t (append (flatten (first expr)) (flatten (rest expr))))))

;; essentially adds one in binary (where t and nil correspond to 1 and 0,
;; respectively, and the bits are ordered from least to most significant)
(defun next-vals (vals)
  (cond
   ((null vals) nil)
   ((first vals) (cons nil (next-vals (rest vals))))
   (t (cons t (rest vals)))))

;;; Returns the truth value of a given propositional calculus sentence
;;; given the truth values of its individual variables.  The truth values
;;; are given as T and NIL.
;;;
;;; The sentence is assumed to be well formed, using only AND, OR, NOT
;;; and IF (plus the constants T or NIL), together with atomic variable
;;; names.  The sentence is not assumed to be in CNF or any other
;;; normalized form.
;;; 
;;; This code uses the Lisp evaluator to evaluate AND, OR, and NOT
;;; expressions.
;;;
;;; Sample call:
;;; 
;;; (eval-truth '(if (and p q) r) '((p . t) (q . nil) (r . t)))
;;;

(defun eval-truth (form truth-vals)
  (eval (varsubst (change-if-to-or form) truth-vals)))

;; used to convert an IF expression to the corresponding OR expression
(defun change-if-to-or (form)
  (cond ((atom form) form)
	((eql (first form) 'if)
	 `(or (not ,(change-if-to-or (second form)))
		   ,(change-if-to-or (third form))))
	(t (cons (change-if-to-or (first form))
		 (change-if-to-or (rest form))))
	))

;; substitutes values from subst-alist for the variables in form
(defun varsubst (form subst-alist)
  (cond ((null subst-alist) form)
	(t (varsubst (subst (cdar subst-alist)
			    (caar subst-alist)
			    form)
		     (cdr subst-alist)))
	))