Making computers think logically, The new and imporved version.

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

Signing Off,
Vishnu Vyas