-
Notifications
You must be signed in to change notification settings - Fork 0
/
bdds.lisp
286 lines (261 loc) · 10.2 KB
/
bdds.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(defvar *ite-hash* nil)
(defun triple-eq (l1 l2)
"triple equality predicate (all elements eq)"
(or (eq l1 l2)
(and (cddr l1)
(cddr l2)
(eq (first l1) (first l2))
(eq (second l1) (second l2))
(eq (third l1) (third l2)))))
(sb-ext:define-hash-table-test triple-eq sxhash)
(defun get-ite-node (&rest args)
args)
(defun build-bdd (constraint &optional limit)
"construct a BDD for constraint (does not convert to CNF)"
(let ((memo (make-hash-table :test 'equal))
(rhs (rhs constraint))
(lhs (lhs constraint))
(rel (rel constraint))
(count 0))
(block recursion
(labels
((bb-aux (terms size sum max depth)
(cond
((> sum rhs) (if (eql rel '>=) t nil))
((and (or (eql rel '>=)
(endp terms))
(= sum rhs)))
((< (+ sum max) rhs) nil)
((not (nth-value 1 (gethash (cons size sum) memo)))
#+assert (assert terms)
(setf count (1+ count))
(if (and limit
(or (> depth 5000)
(> count limit)))
(return-from recursion :fail)
(let* ((term (car terms))
(var (tvar term))
(coef (let ((coef (tcoef term)))
#+assert (assert (> coef 0))
coef))
(max (- max coef))
(key (cons size sum))
(size (1- size))
(depth (1+ depth))
(hi (bb-aux (cdr terms) size (+ sum coef)
max depth))
(lo (bb-aux (cdr terms) size sum
max depth)))
(setf (gethash key memo)
(if (eq hi lo)
hi
(get-ite-node var hi lo))))))
(t (gethash (cons size sum) memo)))))
(let* ((s (apply #'+ (mapcar #'tcoef lhs)))
(bdd (bb-aux lhs (length lhs) 0 s 0)))
(values bdd count))))))
(defun sort-constraints-sum (constraints)
"sort terms in constraints (largest coefficient sum first)"
(let* ((llhs (mapcar
(dot
(lambda (l)
(sort (copy-list l)
(lambda (x1 x2)
(< (abs (tvar x1))
(abs (tvar x2))))))
#'lhs)
constraints))
(f (lambda (&rest terms)
(let* ((coefs (mapcar #'tcoef terms))
(sum (apply #'+ coefs))
(var (abs (tvar (car terms)))))
(cons var sum))))
(l (apply #'mapcar (cons f llhs)))
(l (sort l (lambda (x1 x2) (> (cdr x1) (cdr x2)))))
(h (make-hash-table)))
(loop
for i from 1
for pair in l
do (setf (gethash (car pair) h) i))
(mapcar (lambda (c)
(make-constraint
(rel c)
(sort (copy-list (lhs c))
(lambda (x1 x2)
(< (gethash (abs (tvar x1)) h)
(gethash (abs (tvar x2)) h))))
(rhs c)))
constraints)))
(defun always-falsified (terms rel rhs max)
#+assert (assert (for-all (dot #'> #'tcoef) terms))
#-assert (declare (ignorable terms))
(or (< max rhs)
(and (eql rel '=) (< rhs 0))))
(defun exists-falsified (largs)
(find-if (curry #'apply #'always-falsified) largs))
(defun always-satisfied (terms rel rhs max)
(declare (ignorable max))
#+assert (assert (for-all (dot #'> #'tcoef) terms))
(if (eql rel '>=)
(<= rhs 0)
(and (endp terms)
(= rhs 0))))
(defun recursion-args (pos terms rel rhs max)
(let* ((term (car terms))
(var (tvar term))
(coef (let ((coef (tcoef term)))
#+assert (assert (> coef 0))
coef))
(rhs (if (if pos (> var 0) (< var 0))
(- rhs coef)
rhs))
(max (- max coef)))
(list (cdr terms) rel rhs max)))
(defun build-big-bdd (constraints &optional limit)
(let* ((length (length constraints))
(constraints (sort-constraints-sum constraints))
(memo (make-hash-table :test 'equal))
(count 0))
(format t "c building big BDD (~A constraints)~%" length)
(block blow-up
(labels
((initial-arguments (constraint)
(let* ((lhs (lhs constraint))
(max (apply #'+ (mapcar #'tcoef lhs))))
(list lhs (rel constraint)
(rhs constraint) max)))
(check-too-big (depth)
(setf count (1+ count))
(if (and limit
(or (> depth 5000)
(> count (* 1.2 limit))))
(return-from blow-up :fail)))
(largs-hi (largs)
(loop for args in largs
collect (apply #'recursion-args (cons t args))))
(largs-lo (largs)
(loop for args in largs
collect (apply #'recursion-args (cons nil args))))
(bb-aux (vars largs size depth)
(unless (exists-falsified largs)
(or (for-all (curry #'apply #'always-satisfied) largs)
(let* ((rhss (mapcar #'cddr largs))
(key (list rhss size)))
(multiple-value-bind (v found)
(gethash key memo)
(if found v
(progn
(check-too-big depth)
(let* ((var (abs (car vars)))
(size (1- size))
(depth (1+ depth))
(largs-hi (largs-hi largs))
(largs-lo (largs-lo largs))
(hi (bb-aux (cdr vars) largs-hi
size depth))
(lo (bb-aux (cdr vars) largs-lo
size depth)))
(setf (gethash key memo)
(if (eq hi lo)
hi
(get-ite-node
var hi lo))))))))))))
(let ((lvars (mapcar (dot (lambda (l) (sort l #'<))
(curry #'mapcar
(dot #'abs #'tvar))
#'lhs)
constraints)))
(assert (not (cdr (remove-duplicates lvars :test 'equal)))))
(let ((bdd (bb-aux (mapcar (dot #'abs #'tvar)
(lhs (car constraints)))
(mapcar #'initial-arguments constraints)
(length (lhs (car constraints)))
0)))
(values bdd count))))))
(defun convert-bdd (node &optional (monotonic nil))
"convert BDD into CNF"
(declare (ignorable monotonic))
(labels
((cb-aux (node)
(cond
((equal node t) t)
((not node) nil)
((cdddr node) (cdddr node))
(t (let* ((v (car node))
(hi (cb-aux (cadr node)))
(lo (cb-aux (caddr node))))
(setf
(cdddr node)
(cond
((eql hi lo) hi)
;; hi is nil cases
((and (not hi) (not lo)) nil)
((and (not hi) (eql lo t)) (- v))
((not hi) (get-and (- v) lo))
;; hi is t cases
((and (eql hi t) (not lo)) v)
((and (eql hi t) (eql lo t)) t)
;; hi is unknown
(monotonic (get-ite+-monotonic v hi lo))
(t (get-ite+ v hi lo)))))))))
(let ((v (cb-aux node)))
#+assert (assert v)
(add-clause (cl v))
v)))
(defun add-0-terms (constraints)
(let* ((all-variables
(loop for constraint in constraints
append (loop for term in (lhs constraint)
collect (abs (tvar term)))))
(all-variables (remove-duplicates all-variables)))
(mapcar
(lambda (constraint)
(let* ((lhs (lhs constraint))
(aux-terms
(loop
for v in all-variables
unless (find-if (dot (curry #'eql v)
#'abs #'tvar)
lhs)
collect (cons v 0))))
(make-constraint (rel constraint)
(append lhs aux-terms)
(rhs constraint))))
constraints)))
(defun all-bdds-aux (triples)
(let* ((merged-constraints (list (first (car triples))))
(remaining-triples nil)
(bdd (second (car triples)))
(size (third (car triples))))
(loop
for triple in (cdr triples)
for c = (first triple)
for s = (third triple)
for l = (multiple-value-list
(build-big-bdd
(add-0-terms
(cons c merged-constraints))))
for new-bdd = (first l)
for new-size = (second l)
when (<= new-size (+ size s))
do (progn
(setf bdd new-bdd size new-size)
(push c merged-constraints))
else do (push triple remaining-triples)
finally (return
(values
(list bdd size (length merged-constraints))
remaining-triples)))))
(defun all-bdds (triples acc)
(if (endp triples)
(progn
(format t "sizes: ~A~%" (mapcar #'third acc))
(mapcar #'car acc))
(multiple-value-bind (bdd triples)
(all-bdds-aux triples)
(all-bdds triples (cons bdd acc)))))
(defun add-bdd (constraint)
"build BDD and produce CNF for it"
(let ((m (equal (rel constraint) '>=))
(b (build-bdd constraint)))
(convert-bdd b m)))