From 7f0489362a3604706badf37757f4d2f5a6b7965c Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Thu, 17 Jun 2010 16:12:54 +0200 Subject: [PATCH] Fix non-cnf formula addition interface Signed-off-by: Utz-Uwe Haus --- package.lisp | 3 +- satwrap.lisp | 322 +++++++++++++++++++++++++++++------------------------------ 2 files changed, 162 insertions(+), 163 deletions(-) diff --git a/package.lisp b/package.lisp index 3f6007e..a3f58a2 100644 --- a/package.lisp +++ b/package.lisp @@ -66,9 +66,8 @@ ;; convenience functions for common logical operations; could be ;; handled specially one day by backends that support structure informations ;; on CNFs + (:export #:add-formula) (:export #:add-and #:add-or #:add-xor #:add-if #:add-iff) - ;; convenience functions like the above without immediate adding - (:export #:make-and-cnf #:make-or-cnf #:negate-cnf #:make-if-cnf #:make-iff-cnf) ;; input/output (:export #:read-dimacs #:write-dimacs) ;; utils diff --git a/satwrap.lisp b/satwrap.lisp index fd6a40b..562d9b9 100644 --- a/satwrap.lisp +++ b/satwrap.lisp @@ -233,8 +233,9 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." ,@body))) ;; convenience syntax for logical operations: -(defun standardize (tree) - "Convert to NOT, AND, OR (preserving :ATOM)" +(defun standardize (tree) + "Convert tree of logical operations to elementary :NOT, :AND, :OR tree (preserving :ATOM). +Supports :IMPLY, :IFF, binary :XOR, and :NOR. " (cond ((consp tree) (destructuring-bind (op . expr) @@ -244,16 +245,26 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." (if (= 2 (length expr)) `(:OR (:NOT ,(standardize (car expr))) ,(standardize (cadr expr))) - (error "barf"))) + (error "non-binary :IMPLY operation: ~A" tree))) (:IFF (if (= 2 (length expr)) `(:AND ,(standardize `(:IMPLIES ,(car expr) ,(cadr expr))) ,(standardize `(:IMPLIES ,(cadr expr) ,(car expr)))) - (error "barf"))) - (T `(,op ,@(standardize expr)))))) + (error "non-binary :IFF operation: ~A" tree))) + (:XOR + (if (= 2 (length expr)) + (let ((e1 (standardize (first expr))) + (e2 (standardize (second expr)))) + `(:OR (:AND ,e1 (:NOT ,e2)) + (:AND ,e2 (:NOT ,e1)))) + (error "non-binary :XOR operation: ~A" tree))) + (:NOR + `(:AND ,@(mapcar #'(lambda (p) `(:NOT ,(standardize p))) expr))) + + (T `(,op ,@(mapcar #'standardize expr)))))) (T tree))) -(defun move-nots (tree) +(defun standard-tree->nnf (tree) "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree." (cond ((consp tree) @@ -265,14 +276,14 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." (if (consp subexpr) (case (first subexpr) ;; double-not: drop 2 levels - (:NOT (move-nots (cdr subexpr))) + (:NOT (standard-tree->nnf (cadr subexpr))) ;; NOT AND: (:AND `(:OR ,@(mapcar #'(lambda (c) - (move-nots `(:NOT ,c))) + (standard-tree->nnf `(:NOT ,c))) (cdr subexpr)))) ;; NOT OR: (:OR `(:AND ,@(mapcar #'(lambda (c) - (move-nots `(:NOT ,c))) + (standard-tree->nnf `(:NOT ,c))) (cdr subexpr)))) ;; `quoted' atom: keep (:ATOM subexpr) @@ -282,11 +293,12 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." (error "non-unary :NOT expression: ~W" tree))) ;; other operators: AND, OR, ATOM: descend (T - `(,op ,@(mapcar #'move-nots expr)))))) + `(,op ,@(mapcar #'standard-tree->nnf expr)))))) ;; non-cons: stop (T tree))) (defun crossprod (list-of-lists) + "Return a list of all lists containing one element from each sublist of LIST-OF-LISTS." (reduce #'(lambda (collected term) (loop :for x :in term :appending (loop :for tail :in collected @@ -316,159 +328,147 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." (every #'atomic (cdr c))))) (cdr tree)))))) -(defun distribute2 (tree) +(defun distribute (tree) + "Pull out :ANDs to reduce standardized tree in NNF to CNF." (if (consp tree) (case (car tree) - (:AND (let ((subtrees (mapcar #'distribute2 (cdr tree)))) - (assert (every #'is-cnf subtrees)) - `(:AND ,@(apply #'append subtrees)))) - (:OR (let ((subtrees (mapcar #'distribute2 (cdr tree)))) - (assert (every #'is-cnf subtree)) - `(:AND )))) - . + (:AND (let ((sub-cnfs (mapcar #'distribute (cdr tree)))) + (assert (every #'is-cnf sub-cnfs) + (sub-cnfs) + "Not all in CNF: ~{~A~^~%~}" sub-cnfs) + (let (clauses) + (loop :for sub-cnf :in sub-cnfs + :if (and (consp sub-cnf) + (eq :AND (car sub-cnf))) + ;; AND(AND ..) = AND .. + :do (dolist (clause (cdr sub-cnf)) + (push clause clauses)) + :else :do (push sub-cnf clauses)) + `(:AND ,@clauses)))) + (:OR (let (ands) + (dolist (term (mapcar #'distribute (cdr tree))) + (assert (is-cnf term) + (term) + "~A not in CNF" term) + (if (consp term) + (case (car term) + (:AND (push (cdr term) ands)) + (:OR (dolist (c (cdr term)) + (push `(,c) ands))) + (otherwise (push `(,term) ands))) + (push `(,term) ands))) + (let ((clauses (crossprod ands))) + `(:AND ,@(mapcar #'(lambda (c) + (format T "~&;; c=~A~%" c) + (if (not (consp c)) + c + `(:OR ,@ (loop :for subterm :in c + :if (and (consp subterm) + (eq :OR (car subterm))) + ;; (OR(OR...)) == (OR ...) + :append (cdr subterm) + ;; if C is not an OR-clause + ;; it is considered atomic: + :else :append `(,subterm))))) + clauses))))) + (otherwise + tree)) tree)) -(defun distribute (tree) - "Pull out ANDs and unite sequential OR/OR or AND/AND. Input must be in NNF. Returns -CNF of TREE." - (if (consp tree) - (destructuring-bind (op . expr) - tree - (case op - (:OR (let (ands ors others) - (dolist (term (mapcar #'distribute expr)) - (if (consp term) - (case (car term) - (:OR (push term ors)) - (:AND (push term ands)) - (otherwise (push term others))) - (push term others))) - ; (break "~A ~A ~A" ands ors others) - (if ands - (distribute - (let ((terms (mapcar #'(lambda (or-clause) - `(:OR ,@(mapcar #'cdr ors) - ,@others - ,@or-clause)) - (crossprod (mapcar #'cdr ands))))) - (break "~A" `(:AND ,@terms)) - `(:AND ,@terms))) - `(:OR ,@others ,@(mapcar #'cdr ors))))) - (:AND (let ((subexpr '())) - (dolist (e expr) - (if (consp e) - (case (first e) - (:AND (dolist (f (cdr e)) - (push (distribute f) subexpr))) - (:OR (push (mapcar #'distribute (cdr e)) subexpr)) - (otherwise (push e subexpr))) - (push e subexpr))) - `(:AND ,@subexpr))) - (otherwise - ;; :NOT, :ATOM or implicit leaf: keep - tree))) - tree)) -(defun tree->cnf (tree) - (labels ( - - ) - (distribute - (move-nots - (standardize tree)))) - ;; (cond - ;; ((consp tree) - ;; (destructuring-bind (op . expr) - ;; tree - ;; (case op - ;; ((:IMPLY :IMPILES) - ;; (if (= 2 (length expr)) - ;; (tree->cnf `(:OR (:NOT ,(car expr)) ,(cadr expr))) - ;; (error "barf"))) - ;; (:IFF - ;; (if (= 2 (length expr)) - ;; (tree->cnf `(:AND (:IMPLIES ,(car expr) ,(cadr expr)) - ;; (:IMPLIES ,(cadr expr) ,(car expr)))) - ;; (error "barf"))) - ;; (:) - - ;; (:AND (mapcar #'tree->cnf expr)) - ;; (:OR (tree->cnf `(:NOT (:AND (:NOT ,expr))))) - ;; (:NOT (if (= 1 (length expr)) - ;; () - ;; (error)) (mapcar )))) - ;; ) - ;; ((and lis))) - ) - -(defun tree->cnf (tree) - (etypecase tree - (number `(,tree)) - (cons (case (car tree) - (:AND - ;; flatten: - `(,(apply #'append (mapcar #'tree->cnf (cdr tree))))) - (:NOT - (if (= 2 (length tree)) - (let ((expr (cdr tree))) - (cond - ;; we prefer AND by swapping NOT AND to AND NOT - ((eq :AND (car expr)) - (tree->cnf `(:AND (mapcar #'- (tree->cnf (cdr expr)))))) - ((eq :OR (car expr)) - (tree->cnf `(:AND ))) - ((numberp expr) (- expr)) - (T (error "unsupported")))) - `(,(mapcar #'(lambda (clause) (mapcar #'- clause)) - (tree->cnf (cadr tree)))) - (error "non-unary :NOT expression: ~A" tree))) - - - - (:OR (tree->cnf `(:NOT (:AND ,(cdr tree))))) - (:XOR - (if (= 3 (length tree)) - (let ((a (cadr tree)) - (b (caddr tree))) - (tree->cnf `(:AND (:OR ,a ,b) - (:OR (:NOT ,a) (:NOT ,b))))) - (error "non-binary :XOR expression: ~A" tree))) - ((:IMPLIES :IMPLY) - (if (= 3 (length tree)) - (tree->cnf `(:OR (:NOT ,(cadr tree)) - (caddr tree))) - (error "non-binary :IMPLIES expression: ~A" tree))) - (:IFF - (if (= 3 (length tree)) - (let ((a (cadr tree)) - (b (caddr tree))) - (tree->cnf `(:AND (:IMPLIES ,a ,b) - (:IMPLIES ,b ,a)))) - (error "non-binary :IFF expression: ~A" tree))) - (otherwise - (error "unsupported expression: ~A" tree)))) - (T (error "Formula contains unsupported expression: ~A" tree)))) - -(defmacro build-cnf (tree) - `(tree->cnf ',tree)) - -(defun make-and-cnf (literals) - (mapcar #'list literals)) -(defun make-or-cnf (literals) - literals) -(defun negate-cnf (list-of-clauses) - (mapcar #'(lambda (c) (mapcar #'- c)) list-of-clauses)) -(defun make-xor-cnf (a b) - (make-or-cnf)`(,a ,(- b)) - literals) - -(defgeneric add-and (solver literals) - (:documentation "Add clauses for AND(literals) to SOLVER.")) -(defgeneric add-or (solver literals) - (:documentation "Add clauses for OR(literals) to SOLVER.")) -(defgeneric add-xor (solver literals) - (:documentation "Add clauses for XOR(literals) to SOLVER.")) -(defgeneric add-if (solver lhs rhs) - (:documentation "Add clauses for lhs -> rhs to SOLVER.")) -(defgeneric add-iff (solver lhs rhs) - (:documentation "Add clauses for lhs <-> rhs to SOLVER.")) \ No newline at end of file +(defun tree->cnf (tree &optional (mapping #'cl:identity) (atom-test #'eql)) + "Convert TREE to CNF, applying MAPPING to atoms and afterwards and removing duplicate literals in clauses using atom-test to test for equality. Also simplifies trivially fulfilled clauses to empty clause." + (labels ((atomic (f) + (if (consp f) + (and (not (eq :OR (car f))) + (not (eq :AND (car f)))) + T)) + (map-literals (cnf) + ;; destructively apply MAPPING + (if (atomic cnf) + (setf cnf (funcall mapping cnf)) + (setf (cdr cnf) ;; we must be looking at an AND + (mapcar #'(lambda (clause) + (if (atomic clause) + (funcall mapping clause) + `(:OR ,@(mapcar #'(lambda (lit) + (funcall mapping lit)) + (cdr clause))))) + (cdr cnf)))) + cnf) + (negated-litp (lit) + (and (consp lit) (eq :NOT (car lit)))) + (atom-for (lit) + (if (consp lit) + (case (car lit) + (:NOT (atom-for (second lit))) + (:ATOM (second lit)) + (otherwise lit)) + lit)) + (duplicate-literalsp (l1 l2) + (funcall atom-test (atom-for l1) (atom-for l2))) + (trivial-clausep (c) + (loop :for (lit . haystack) :on c + :as needle := (atom-for lit) + :as negated := (and (consp lit) (eq :NOT (car lit))) + :when (find-if #'(lambda (x) + (and (if negated + (not (negated-litp x)) + (negated-litp x)) + (funcall atom-test needle (atom-for x)))) + haystack) + :return T + :finally (return NIL))) + (clean-clauses (cnf) + ;; destructively apply MAPPING + (if (atomic cnf) + (setf cnf (funcall mapping cnf)) + (setf (cdr cnf) ;; we must be looking at an AND + (mapcar #'(lambda (clause) + (if (atomic clause) + (funcall mapping clause) + (if (trivial-clausep clause) + '(:OR ) + `(:OR ,@(remove-duplicates + (cdr clause) + :test #'duplicate-literalsp))))) + (cdr cnf)))) + cnf)) + (clean-clauses + (map-literals + (distribute + (standard-tree->nnf + (standardize tree))))))) + + +(defgeneric add-formula (solver formula &key mapping atom-test) + (:documentation "Add logical FORMULA to SOLVER. +Formula is an expression tree that can contain high-level abbreviations :IMPLY, :IFF, :NOR and :XOR, as well as the basic :AND, :OR, :NOT. Everything else is considered an atom. Atoms can also be explicitly written as (:ATOM foo). +All atoms will be mapped through MAPPING before being added to the solver to convert your favorite atoms to phased variables. MAPPING is a function of 1 argument, the atom. It defaults to #'identity. Afterwards, clean clauses (removing duplicates and simplifying trivial clauses, comparing atoms using ATOM-TEST (default: #'eql).") + (:method ((solver sat-solver) (formula list) &key (mapping #'identity) (atom-test #'eql)) + (add-clauses solver (tree->cnf formula mapping atom-test)))) + +(defgeneric add-and (solver literals &key mapping) + (:documentation "Add clauses for AND(literals) to SOLVER.") + (:method ((solver sat-solver) (literals list) &key (mapping #'identity)) + (add-formula solver `(:AND ,@literals) mapping))) + +(defgeneric add-or (solver literals &key mapping) + (:documentation "Add clauses for OR(literals) to SOLVER.") + (:method ((solver sat-solver) (literals list) &key (mapping #'identity)) + (add-formula solver `(:OR ,@literals) mapping))) + +(defgeneric add-xor (solver literals &key mapping) + (:documentation "Add clauses for binary XOR(literals) to SOLVER.") + (:method ((solver sat-solver) (literals list) &key (mapping #'identity)) + (add-formula solver `(:XOR ,@literals) mapping))) + +(defgeneric add-if (solver lhs rhs &key mapping) + (:documentation "Add clauses for lhs -> rhs to SOLVER.") + (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity)) + (add-formula solver `(:IMPLIES ,lhs ,rhs) mapping))) + +(defgeneric add-iff (solver lhs rhs &key mapping) + (:documentation "Add clauses for lhs <-> rhs to SOLVER.") + (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity)) + (add-formula solver `(:IFF ,lhs ,rhs) mapping))) \ No newline at end of file -- 2.11.4.GIT