;; 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)

__: Fixed 2 bugs in code.__

**Upadte 1**__: Found destructuring more efficient than comparing with the last element.__

**Update 2**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

## No comments:

Post a Comment