Making computers think logically.

Conjunctive Normal Forms or CNF's as they are called are simply boolean expressions which are stuck together by conjunctions (and's) and by themselves each subexpressions is a bunch of variables (both negated and non-negated) which are strung toghether by or's. So whats the use of CNF's you ask. well for one thing they allow computers to think logically and make decisions.

Here is a small program which does exactly that. Solves CNF's. An explaination of the program is for another post of its own.

;;; Solves CNF forms
;;; the macro resolve-list takes as input a list of the form
;;; ((expr1) (expr2) (expr3) ... )
;;; where each expr is of the the form ( var1 or var2 or ... not varN ...or varK )

(defpackage :cnf

 (:use :common-lisp)
 (:export resolve-list))

(in-package :cnf)

;;; function seperate-parts.
;;; Seperate parts splits the expression into variables that are negated and those that
;;; are not negated.

(defun seperate-parts (expr1)
 "Seperates the negated variables and the non-negated variables"

 (let ((list-v ())
       (list-vneg ())
       (next ()))

   (dolist (iter expr1)
     (cond
       ((eq 'or iter) ())
       ((eq 'not iter) (setf next t))
       (t (if next
              (progn

                (push iter list-vneg)
                (setf next ()))
              (push iter list-v)))))
   (values list-v list-vneg)))

;;; function resolve-pair
;;; uses basic laws of logic to resolve 2 boolean expressions containing only
;;; or's or not's.


(defun resolve-pair (expr1 expr2)
 "Resolves a pair of conjunctive expressions"

 (let ((list1 ())
       (list2 ())
       (nlist1 ())
       (nlist2 ()))

   (multiple-value-bind (lst nlst)
       (seperate-parts expr1)
     (setf list1 lst)
     (setf nlist1 nlst))

   (multiple-value-bind (lst nlst)
       (seperate-parts expr2)
     (setf list2 lst)
     (setf nlist2 nlst))

   ;; rem-list is the list of variables that cancel out due to negation.

    ;; allp-list is the list of variables that are not negated and can occour in the final expression
    ;; alln-list is the list of variables that are negated and can occour in the final expression
    ;; red-list1 is the pretty version of allp-list with the or's in place
    ;; red-list2 is the pretty version of alln-list with the or's and not's in place.

   (let* ((rem-list (union (intersection list1 nlist2)
                           (intersection list2 nlist1)))
          (allp-list (remove-if #'(lambda (x) (if (member x rem-list) t nil))
                                (union list1 list2)))
          (alln-list (remove-if #'(lambda (x) (if (member x rem-list) t nil))
                                (union nlist1 nlist2)))
          (red-list1 ())
          (red-list2 ()))

          (dolist (pitm allp-list)
            (push pitm red-list1)
            (push 'or red-list1))

          (dolist (pitm alln-list)
            (push 'not red-list2)
            (push pitm red-list2)
            (push 'or red-list2))
         
          ;; since there is an extra or/not at the end.. which comes as the first element..

           ;; we can skip it and hence only the cdr of the list is returned.

          (delete 'or (nreverse (concatenate 'list red-list1 red-list2)) :count 1 :from-end t))))


(defmacro resolve-list (exprlist)
 "resolves a list of cnf's"

 `(reduce #'resolve-pair ,exprlist))

;;(end-package :cnf)

Update : The old code had some bugs which din't work in certain cases, so the code now is updated.

Technorati tag : lisp


Signing off,
Vishnu Vyas.