From a0f16720a7ec4c5e70beb445180f2fb73adebc26 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Thu, 10 Jun 2010 13:43:22 +0200 Subject: [PATCH] Add CNF builder convenience functions WIP, Still broken and incomplete Signed-off-by: Utz-Uwe Haus --- package.lisp | 9 ++- satwrap.lisp | 241 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 249 insertions(+), 1 deletion(-) diff --git a/package.lisp b/package.lisp index 913ea0a..3f6007e 100644 --- a/package.lisp +++ b/package.lisp @@ -61,7 +61,14 @@ ;; interface: (:export #:add-variable #:add-clause #:satisfiablep #:solution #:get-essential-variables - #:with-sat-solver #:with-index-hash) + #:with-sat-solver #:with-index-hash + #:add-clauses) + ;; convenience functions for common logical operations; could be + ;; handled specially one day by backends that support structure informations + ;; on CNFs + (: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 6824cd2..bd61671 100644 --- a/satwrap.lisp +++ b/satwrap.lisp @@ -229,3 +229,244 @@ Typically used to map objects to variables inside WITH-SAT-SOLVER." :do (setf (gethash x ht) num) :finally (return ht)))))) ,@body))) + +;; convenience syntax for logical operations: +(defun standardize (tree) + "Convert to NOT, AND, OR (preserving :ATOM)" + (cond + ((consp tree) + (destructuring-bind (op . expr) + tree + (case op + ((:IMPLY :IMPLIES) + (if (= 2 (length expr)) + `(:OR (:NOT ,(standardize (car expr))) + ,(standardize (cadr expr))) + (error "barf"))) + (:IFF + (if (= 2 (length expr)) + `(:AND ,(standardize `(:IMPLIES ,(car expr) ,(cadr expr))) + ,(standardize `(:IMPLIES ,(cadr expr) ,(car expr)))) + (error "barf"))) + (T `(,op ,@(standardize expr)))))) + (T tree))) + +(defun move-nots (tree) + "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree." + (cond + ((consp tree) + (destructuring-bind (op . expr) + tree + (case op + (:NOT (if (= 1 (length expr)) + (let ((subexpr (first expr))) + (if (consp subexpr) + (case (first subexpr) + ;; double-not: drop 2 levels + (:NOT (move-nots (cdr subexpr))) + ;; NOT AND: + (:AND `(:OR ,@(mapcar #'(lambda (c) + (move-nots `(:NOT ,c))) + (cdr subexpr)))) + ;; NOT OR: + (:OR `(:AND ,@(mapcar #'(lambda (c) + (move-nots `(:NOT ,c))) + (cdr subexpr)))) + ;; `quoted' atom: keep + (:ATOM subexpr) + (otherwise `(:NOT ,subexpr))) + ;; non-quoted atom: + `(:NOT ,subexpr))) + (error "non-unary :NOT expression: ~W" tree))) + ;; other operators: AND, OR, ATOM: descend + (T + `(,op ,@(mapcar #'move-nots expr)))))) + ;; non-cons: stop + (T tree))) + +(defun crossprod (list-of-lists) + (reduce #'(lambda (collected term) + (loop :for x :in term :appending + (loop :for tail :in collected + :collect `(,x ,@tail)))) + list-of-lists + :initial-value '(()))) + +(defun is-cnf (tree) + "Check that TREE is in CNF." + (flet ((and-form (f) + (and (consp f) + (eq :AND (car f)))) + (or-form (f) + (and (consp f) + (eq :OR (car f)))) + (atomic (f) + (if (consp f) + (and (not (eq :OR (car f))) + (not (eq :AND (car f)))) + T))) + (if (atomic tree) + T + (and (and-form tree) + (every #'(lambda (c) + (or (atomic c) + (and (or-form c) + (every #'atomic (cdr c))))) + (cdr tree)))))) + +(defun distribute2 (tree) + (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 )))) + . + 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 -- 2.11.4.GIT