Wednesday, October 19, 2005

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)
((eq 'or iter) ())
((eq 'not iter) (setf next t))
(t (if next

(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 :

Signing off,
Vishnu Vyas.

No comments: