commit 514d7e0cfe2ce783c37a13afb983ea187d4868d7
parent 8cea49aeaaaddd7485826d393e447793ae46f9ea
Author: Tomas Hlavaty <tom@logand.com>
Date: Thu, 19 Jun 2014 22:55:10 +0200
bdd package added
Diffstat:
| A | bdd.lisp | | | 237 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 237 insertions(+), 0 deletions(-)
diff --git a/bdd.lisp b/bdd.lisp
@@ -0,0 +1,237 @@
+;;; Copyright (C) 2014 Tomas Hlavaty <tom@logand.com>
+;;;
+;;; Permission is hereby granted, free of charge, to any person
+;;; obtaining a copy of this software and associated documentation
+;;; files (the "Software"), to deal in the Software without
+;;; restriction, including without limitation the rights to use, copy,
+;;; modify, merge, publish, distribute, sublicense, and/or sell copies
+;;; of the Software, and to permit persons to whom the Software is
+;;; furnished to do so, subject to the following conditions:
+;;;
+;;; The above copyright notice and this permission notice shall be
+;;; included in all copies or substantial portions of the Software.
+;;;
+;;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+;;; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+;;; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+;;; NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+;;; HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+;;; WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+;;; OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+;;; DEALINGS IN THE SOFTWARE.
+
+(defpackage :rw.bdd
+ (:use :cl))
+
+(in-package :rw.bdd)
+
+(defparameter *mk-htab* (make-hash-table :test #'equal)) ;; (v l . h) equal => eq
+
+(let ((k (list nil nil))) ;; reduce consing
+ (defun mk (v l h)
+ (check-type v (integer 2 *))
+ (check-type l (or bit list))
+ (check-type h (or bit list))
+ (let ((zero '(#.most-positive-fixnum nil . zero))
+ (one '(#.most-positive-fixnum nil . one)))
+ (when (typep l 'bit)
+ (setq l (if (zerop l) zero one)))
+ (when (typep h 'bit)
+ (setq h (if (zerop h) zero one)))
+ (check-type l list)
+ (check-type h list)
+ (cond
+ ;;((zerop v) zero)
+ ;;((= 1 v) one)
+ ((eq l h) l)
+ (t
+ (rplaca k v)
+ (let ((d (cdr k)))
+ (rplaca d l)
+ (rplacd d h))
+ (or (gethash k *mk-htab*)
+ (prog1 (setf (gethash k *mk-htab*) k)
+ (setq k (list nil nil)))))))))
+
+;;(eq (mk 2 0 0) (mk 2 0 0))
+;;(eq (mk 2 1 1) (mk 2 1 1))
+
+(defun app (op u1 u2)
+ (let ((g (make-hash-table :test #'equal))
+ (zero (mk 2 0 0))
+ (one (mk 2 1 1)))
+ (labels ((rec (u1 u2)
+ (let ((k (cons u1 u2))) ;; TODO reduce consing
+ (or (gethash k g)
+ (setf (gethash k g)
+ (destructuring-bind (v1 l1 &rest h1) u1
+ (destructuring-bind (v2 l2 &rest h2) u2
+ (cond
+ ((and (or (eq zero u1) (eq one u1))
+ (or (eq zero u2) (eq one u2)))
+ (if (ecase op
+ (and (and (eq one u1) (eq one u2)))
+ (or (or (eq one u1) (eq one u2)))
+ (eq (eq u1 u2)))
+ one
+ zero))
+ ((= v1 v2)
+ (mk v1 (rec l1 l2) (rec h1 h2)))
+ ((< v1 v2)
+ (mk v1 (rec l1 u2) (rec h1 u2)))
+ (t
+ (mk v2 (rec u1 l2) (rec u1 h2)))))))))))
+ (rec u1 u2))))
+
+;;(app 'and (mk 2 0 1) (mk 3 0 1))
+;;(app 'or (mk 2 0 1) (mk 3 0 1))
+;;(app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1))
+
+(defun build (exp)
+ (labels ((rec (x)
+ (etypecase x
+ (bit (mk 2 x x))
+ (integer
+ (let ((v (abs x)))
+ (if (minusp x)
+ (mk v 1 0)
+ (mk v 0 1))))
+ (cons
+ (let ((op (car x)))
+ (etypecase op
+ (integer x) ;; bdd
+ (symbol
+ (ecase op
+ ((and or eq)
+ (assert (cdr x)) ;; TODO empty and|or|eq?
+ (reduce (lambda (l r)
+ (app op (rec l) (rec r)))
+ (cddr x)
+ :initial-value (rec (cadr x))))
+ (imp
+ (destructuring-bind (l r) (cdr x)
+ (rec `(or (not ,l) (and ,l ,r)))))
+ (not
+ (destructuring-bind (y) (cdr x)
+ (etypecase y
+ (bit (rec (if (zerop y) 1 0)))
+ (integer (rec (- y)))
+ (cons
+ (destructuring-bind (v l &rest h) (rec y)
+ (mk v h l))))))))))))))
+ (rec exp)))
+
+;;(build 0)
+;;(build 1)
+;;(build -2)
+;;(build 2)
+;;(build '(and 2 3))
+;;(build '(and 2 -3))
+;;(build '(or 2 3))
+;;(build '(or -2 3))
+;;(build '(and (or -2 3) 4 5))
+;;(build '(not 0))
+;;(build '(not 1))
+;;(build '(not 2))
+;;(build '(not -2))
+;;(build '(not (or 2 3)))
+;;(eq (build '(and (or 2 3))) (build '(or 2 3)))
+
+(defun restrict (u j b)
+ (let ((g (make-hash-table :test #'eq)))
+ (labels ((rec (u)
+ (or (gethash u g)
+ (setf (gethash u g)
+ (destructuring-bind (v l &rest h) u
+ (cond
+ ((< j v) u)
+ ((< v j) (mk v (rec l) (rec h))) ;; TODO O(exp) -> linear
+ ((= 0 b) (rec l))
+ (t (rec h))))))))
+ (rec u))))
+
+;;(restrict (app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1)) 3 0)
+
+(defun any-sat (u &optional ones) ;; TODO expand all dont-care vars
+ (let ((zero (mk 2 0 0))
+ (one (mk 2 1 1)))
+ (labels ((rec (u)
+ (when (eq zero u)
+ (return-from any-sat nil))
+ (unless (eq one u)
+ (destructuring-bind (v l &rest h) u
+ (if ones
+ (if (eq zero h)
+ (cons (- v) (any-sat l))
+ (cons v (any-sat h)))
+ (if (eq zero l)
+ (cons v (any-sat h))
+ (cons (- v) (any-sat l))))))))
+ (rec u))))
+
+;;(any-sat (build 0))
+;;(any-sat (build 1))
+;;(any-sat (build '(and 2 3)))
+;;(any-sat (build '(and 2 -3)))
+;;(any-sat (build '(or 2 3)))
+;;(any-sat (build '(or 2 3)) t)
+;;(any-sat (build '(or -2 3)))
+;;(any-sat (build '(or -2 3)) t)
+
+(defun build-n-queens (n)
+ (flet ((var (i j)
+ (+ 2 (* i n) j)))
+ `(and
+ ,@(loop ;; place a queen in each row
+ for i from 0 below n
+ collect `(or
+ ,@(loop
+ for j from 0 below n
+ collect (var i j))))
+ ,@(loop ;; build requirements for each variable (field)
+ for i from 0 below n
+ appending
+ (loop
+ for j from 0 below n
+ appending
+ ;; build the requirements for all other fields than
+ ;; (i,j) assuming that (i,j) has a queen
+ (nconc
+ (loop ;; no one in the same column
+ for k from 0 below n
+ unless (= k j)
+ collect `(imp ,(var i j) (not ,(var i k))))
+ (loop ;; no one in the same row
+ for k from 0 below n
+ unless (= k i)
+ collect `(imp ,(var i j) (not ,(var k j))))
+ (loop ;; no one in the same up-right diagonal
+ for k from 0 below n
+ for ll = (+ k (- i) j)
+ when (and (<= 0 ll) (< ll n) (not (= k i)))
+ collect `(imp ,(var i j) (not ,(var k ll))))
+ (loop ;; no one in the same down-right diagonal
+ for k from 0 below n
+ for ll = (+ i j (- k))
+ when (and (<= 0 ll) (< ll n) (not (= k i)))
+ collect `(imp ,(var i j) (not ,(var k ll))))))))))
+
+(defun print-n-queens-board (n solution)
+ (print n)
+ (terpri)
+ (let ((r (rw:reader solution)))
+ (dotimes (i n)
+ (dotimes (j n)
+ (princ (if (plusp (funcall r)) #\X #\.)))
+ (terpri))))
+
+
+;;(time (let ((n 1)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 2)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 3)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 4)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 5)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 6)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 7)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 8)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
+;;(time (let ((n 9)) (print-n-queens-board n (any-sat (build (build-n-queens n))))))
