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