To us, here and now, it appears thus.

rants, ramblings and other things that make life worth living…

Making computers think logically, The new and imporved version.

leave a comment »

The previous post about solving CNF using a bit of common lisp was something that transpired out of a conversation with Vivek. The previous program even though was functionaly good, lacked a certain sense of aesthetics that lisp programs should have. So with a little more effort, and some help from Thomas.F.Burdick from c.l.l, here is the new and imporved version.


;; CNF Solver, ver 2.0
;; Same functionality as the previous one
;; but is better in that its easier to work.
;; Thanks to a little help from Thomas.F.Brudrick


(defpackage :cnf
(:use :common-lisp)
(:export resovle))

(in-package :cnf)

(defun seperate-parts (expr)
"seperate the epxression into negated and non negated variables"

(loop for s = (pop expr)
      if (eql s 'or)
       do (values)
      else if (eql s 'not)
       collect (pop expr) into vneg
      else collect s into v
      while expr
      finally return (values v vneg)))


(defun resolve-pair (expr1 expr2)
"resolves a pair of cnf expressions."
(flet
    ; xform is a formatting function which is used to take a list
      ; of symbols and convert them into a list of symbols padded
      ; appropriately with the pre and post symbols.
      ((xform (list pre post)
         (let ((x (car (last list))))
           (loop for item in list
                 if (eql item x) nconc (nconc (when pre (list pre))
                                              (list item))
                 else nconc (nconc (when pre (list pre))
                                   (list item)
                                   (list post))))))

  (multiple-value-bind (list1 nlist1) (seperate-parts expr1)
    (multiple-value-bind (list2 nlist2) (seperate-parts expr2)

      ;rem is the set of variables that cancel out.
        ;allp is the set of all non-negated symbols.
        ;alln is the set of all negated symbols.
        (let* ((rem (union (intersection list1 nlist2)
                         (intersection list2 nlist1)))
             (allp (set-difference (union list1 list2) rem))
             (alln (set-difference (union nlist1 nlist2) rem)))
        (nconc (xform allp '() 'or)
               (when alln
                 (nconc (list 'or)
                        (xform alln 'not 'or)))))))))

(defmacro resolve (exprlist)
"resolves a list of CNF expressions"

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


;; (end-package :cnf)


Upadte 1: Fixed 2 bugs in code.

Update 2 : Found destructuring more efficient than comparing with the last element.
hence xform can be written as.


    ;; xform is a formatting function which is used to take a list
      ;; of symbols and convert them into a list of symbols padded
      ;; appropriately with the pre and post symbols.
      ((xform (list pre post)
       (loop for (item . morep) on list
                 if morep  nconc (nconc (when pre (list pre))
                                        (list item)
                                        (when post (list post)))
                 else nconc (nconc (when pre (list pre))
                                   (list item)))))

Technorati Tag:

Signing Off,
Vishnu Vyas

Advertisements

Written by vishnuvyas

October 20, 2005 at 4:21 am

Posted in Geeky Stuff

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: