bdd.lisp (11682B)
1 ;;; Copyright (C) 2014 Tomas Hlavaty <tom@logand.com> 2 ;;; 3 ;;; Permission is hereby granted, free of charge, to any person 4 ;;; obtaining a copy of this software and associated documentation 5 ;;; files (the "Software"), to deal in the Software without 6 ;;; restriction, including without limitation the rights to use, copy, 7 ;;; modify, merge, publish, distribute, sublicense, and/or sell copies 8 ;;; of the Software, and to permit persons to whom the Software is 9 ;;; furnished to do so, subject to the following conditions: 10 ;;; 11 ;;; The above copyright notice and this permission notice shall be 12 ;;; included in all copies or substantial portions of the Software. 13 ;;; 14 ;;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 15 ;;; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 16 ;;; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 17 ;;; NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT 18 ;;; HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, 19 ;;; WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 20 ;;; OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER 21 ;;; DEALINGS IN THE SOFTWARE. 22 23 (defpackage :rw.bdd 24 (:use :cl)) 25 26 (in-package :rw.bdd) 27 28 (defparameter *mk-htab* (make-hash-table :test #'equal)) ;; (v l . h) equal => eq 29 30 (deftype var () '(integer 2 #.(floor most-positive-fixnum 2))) 31 (deftype nvar () '(integer #.(floor most-negative-fixnum 2) #.(floor most-positive-fixnum 2))) 32 33 (let ((k (list nil nil))) ;; reduce consing 34 (defun mk (v l h) 35 (declare (optimize speed) 36 (type var v) 37 (type (or bit list) l h)) 38 (let ((zero '(#.(floor most-positive-fixnum 2) nil . zero)) ;; TODO use nvars+1 39 (one '(#.(floor most-positive-fixnum 2) nil . one))) ;; TODO ue nvars+1 40 (when (typep l 'bit) 41 (setq l (if (zerop l) zero one))) 42 (when (typep h 'bit) 43 (setq h (if (zerop h) zero one))) 44 (cond 45 ((eq l h) l) 46 (t 47 (rplaca k v) 48 (let ((d (cdr k))) 49 (rplaca d l) 50 (rplacd d h)) 51 (or (gethash k *mk-htab*) 52 (prog1 (setf (gethash k *mk-htab*) k) 53 (setq k (list nil nil))))))))) 54 55 ;;(eq (mk 2 0 0) (mk 2 0 0)) 56 ;;(eq (mk 2 1 1) (mk 2 1 1)) 57 58 (defun app (op u1 u2) 59 (declare (optimize speed)) 60 (let ((g (make-hash-table :test #'equal)) 61 (k (list nil)) 62 (zero (mk 2 0 0)) 63 (one (mk 2 1 1))) 64 (labels ((rec (u1 u2) 65 (rplaca k u1) 66 (rplacd k u2) 67 (or (gethash k g) 68 (setf (gethash (cons u1 u2) g) 69 (destructuring-bind (v1 l1 &rest h1) u1 70 (declare (type var v1)) 71 (destructuring-bind (v2 l2 &rest h2) u2 72 (declare (type var v2)) 73 (cond 74 ((and (or (eq zero u1) (eq one u1)) 75 (or (eq zero u2) (eq one u2))) 76 (if (ecase op 77 (and (and (eq one u1) (eq one u2))) 78 (or (or (eq one u1) (eq one u2))) 79 (eq (eq u1 u2))) 80 one 81 zero)) 82 ((= v1 v2) 83 (mk v1 (rec l1 l2) (rec h1 h2))) 84 ((< v1 v2) 85 (mk v1 (rec l1 u2) (rec h1 u2))) 86 (t 87 (mk v2 (rec u1 l2) (rec u1 h2)))))))))) 88 (rec u1 u2)))) 89 90 ;;(app 'and (mk 2 0 1) (mk 3 0 1)) 91 ;;(app 'or (mk 2 0 1) (mk 3 0 1)) 92 ;;(app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1)) 93 94 (defun build (exp) 95 (declare (optimize speed)) 96 (labels ((rec (x) 97 (etypecase x 98 (bit (mk 2 x x)) 99 (nvar 100 (locally (declare (type fixnum x)) 101 (let ((v (abs x))) 102 (if (minusp x) 103 (mk v 1 0) 104 (mk v 0 1))))) 105 (cons 106 (let ((op (car x))) 107 (etypecase op 108 (integer x) ;; bdd 109 (symbol 110 (ecase op 111 ((and or eq) 112 (assert (cdr x)) ;; TODO empty and|or|eq? 113 (reduce (lambda (l r) 114 (app op (rec l) (rec r))) 115 (cddr x) 116 :initial-value (rec (cadr x)))) 117 (imp 118 (destructuring-bind (l r) (cdr x) 119 (rec `(or (not ,l) (and ,l ,r))))) 120 (not 121 (destructuring-bind (y) (cdr x) 122 (etypecase y 123 (bit (rec (if (zerop y) 1 0))) 124 (integer 125 (locally (declare (type nvar y)) 126 (rec (- y)))) 127 (cons 128 (destructuring-bind (v l &rest h) (rec y) 129 (mk v h l)))))))))))))) 130 (rec exp))) 131 132 ;;(build 0) 133 ;;(build 1) 134 ;;(build -2) 135 ;;(build 2) 136 ;;(build '(and 2 3)) 137 ;;(build '(and 2 -3)) 138 ;;(build '(or 2 3)) 139 ;;(build '(or -2 3)) 140 ;;(build '(and (or -2 3) 4 5)) 141 ;;(build '(not 0)) 142 ;;(build '(not 1)) 143 ;;(build '(not 2)) 144 ;;(build '(not -2)) 145 ;;(build '(not (or 2 3))) 146 ;;(eq (build '(and (or 2 3))) (build '(or 2 3))) 147 148 (defun restrict (u j b) 149 (let ((g (make-hash-table :test #'eq))) 150 (labels ((rec (u) 151 (or (gethash u g) 152 (setf (gethash u g) 153 (destructuring-bind (v l &rest h) u 154 (cond 155 ((< j v) u) 156 ((< v j) (mk v (rec l) (rec h))) ;; TODO O(exp) -> linear 157 ((= 0 b) (rec l)) 158 (t (rec h)))))))) 159 (rec u)))) 160 161 ;;(restrict (app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1)) 3 0) 162 163 (defun any-sat (u &optional ones) ;; TODO expand all dont-care vars 164 (declare (optimize speed)) 165 (let ((zero (mk 2 0 0)) 166 (one (mk 2 1 1))) 167 (labels ((rec (u) 168 (when (eq zero u) 169 (return-from any-sat nil)) 170 (unless (eq one u) 171 (destructuring-bind (v l &rest h) u 172 (declare (type var v)) 173 (if ones 174 (if (eq zero h) 175 (cons (- v) (any-sat l)) 176 (cons v (any-sat h))) 177 (if (eq zero l) 178 (cons v (any-sat h)) 179 (cons (- v) (any-sat l)))))))) 180 (rec u)))) 181 182 ;;(any-sat (build 0)) 183 ;;(any-sat (build 1)) 184 ;;(any-sat (build '(and 2 3))) 185 ;;(any-sat (build '(and 2 -3))) 186 ;;(any-sat (build '(or 2 3))) 187 ;;(any-sat (build '(or 2 3)) t) 188 ;;(any-sat (build '(or -2 3))) 189 ;;(any-sat (build '(or -2 3)) t) 190 191 (defun build-n-queens (n) 192 (declare (optimize speed) 193 (type (integer 1 12345) n)) 194 (flet ((var (i j) 195 (declare (type (integer 0 12345) i j)) 196 (+ 2 (* i n) j))) 197 `(and 198 ,@(loop ;; place a queen in each row 199 for i from 0 below n 200 collect `(or 201 ,@(loop 202 for j from 0 below n 203 collect (var i j)))) 204 ,@(loop ;; build requirements for each variable (field) 205 for i from 0 below n 206 appending 207 (loop 208 for j from 0 below n 209 appending 210 ;; build the requirements for all other fields than 211 ;; (i,j) assuming that (i,j) has a queen 212 (nconc 213 (loop ;; no one in the same column 214 for k from 0 below n 215 unless (= k j) 216 collect `(imp ,(var i j) (not ,(var i k)))) 217 (loop ;; no one in the same row 218 for k from 0 below n 219 unless (= k i) 220 collect `(imp ,(var i j) (not ,(var k j)))) 221 (loop ;; no one in the same up-right diagonal 222 for k from 0 below n 223 for ll = (+ k (- i) j) 224 when (and (<= 0 ll) (< ll n) (not (= k i))) 225 collect `(imp ,(var i j) (not ,(var k ll)))) 226 (loop ;; no one in the same down-right diagonal 227 for k from 0 below n 228 for ll = (+ i j (- k)) 229 when (and (<= 0 ll) (< ll n) (not (= k i))) 230 collect `(imp ,(var i j) (not ,(var k ll)))))))))) 231 232 (defun print-n-queens-board (n solution) 233 (print n) 234 (terpri) 235 (let ((r (rw:reader solution))) 236 (dotimes (i n) 237 (dotimes (j n) 238 (princ (if (plusp (funcall r)) #\X #\.))) 239 (terpri)))) 240 241 242 ;;(time (let ((n 1)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 243 ;;(time (let ((n 2)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 244 ;;(time (let ((n 3)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 245 ;;(time (let ((n 4)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 246 ;;(time (let ((n 5)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 247 ;;(time (let ((n 6)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 248 ;;(time (let ((n 7)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 249 ;;(time (let ((n 8)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 250 ;;(time (let ((n 9)) (print-n-queens-board n (any-sat (build (build-n-queens n)))))) 251 252 (defun to-dot (u &optional out) 253 (flet ((draw (s) 254 (format s "digraph bdd {~%") 255 (let ((g (make-hash-table :test #'eq)) 256 (zero (mk 2 0 0)) 257 (one (mk 2 1 1)) 258 (i 1)) 259 (labels ((rec (u) 260 (or (gethash u g) 261 (setf (gethash u g) 262 (cond 263 ((eq zero u) 264 (format s "n0 [label=\"0\",shape=square]~%") 265 0) 266 ((eq one u) 267 (format s "n1 [label=\"1\",shape=square]~%") 268 1) 269 (t 270 (let ((n (incf i))) 271 (destructuring-bind (v l &rest h) u 272 (declare (type var v)) 273 (format s "n~d [label=\"~a\"]~%" n v) 274 (format s "n~d -> n~d [style=dotted]~%" n (rec l)) 275 (format s "n~d -> n~d~%" n (rec h))) 276 n))))))) 277 (rec u))) 278 (format s "}~%"))) 279 (etypecase out 280 (null (draw *standard-output*)) 281 (stream (draw out)) 282 (pathname 283 (with-open-file (s out 284 :direction :output 285 :if-does-not-exist :create 286 :if-exists :supersede) 287 (draw s)))))) 288 289 ;;(to-dot (build '(and 2 3)) #p"/tmp/a.dot") 290 ;;(to-dot (build '(or (and 2 3) (and 4 5))) #p"/tmp/a.dot") 291 ;;(to-dot (build (build-n-queens 4)) #p"/tmp/a.dot") 292 ;;(rw.os:run-command "dot" '("-Tpng" "-o/tmp/a.png" "/tmp/a.dot"))