1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
3 ;;; cuddsat.lisp --- SAT solver based on CUDD BDDs
5 ;; Copyright (C) 2009 Utz-Uwe Haus <lisp@uuhaus.de>
7 ;; This code is free software; you can redistribute it and/or modify
8 ;; it under the terms of the version 3 of the GNU General
9 ;; Public License as published by the Free Software Foundation, as
10 ;; clarified by the prequel found in LICENSE.Lisp-GPL-Preface.
12 ;; This code is distributed in the hope that it will be useful, but
13 ;; without any warranty; without even the implied warranty of
14 ;; merchantability or fitness for a particular purpose. See the GNU
15 ;; Lesser General Public License for more details.
17 ;; Version 3 of the GNU General Public License is in the file
18 ;; LICENSE.GPL that was distributed with this file. If it is not
19 ;; present, you can access it from
20 ;; http://www.gnu.org/copyleft/gpl.txt (until superseded by a
21 ;; newer version) or write to the Free Software Foundation, Inc., 59
22 ;; Temple Place, Suite 330, Boston, MA 02111-1307 USA
30 (eval-when (:compile-toplevel
:load-toplevel
)
31 (declaim (optimize (speed 3) (debug 1) (safety 1))))
43 (vars #() :type simple-vector
))
45 (defmacro reference
(f)
51 (defmacro dereference
(f manager
)
54 (cuddapi:cudd-recursive-deref
,manager
,x
)
58 `(integer ,#.
(1- (- (expt 2 (* 8 (- (cffi:foreign-type-size
:int
) 1)))))
59 ,#.
(expt 2 (* 8 (- (cffi:foreign-type-size
:int
) 1)))))
61 (defun make-clause-tree (env c
)
62 (loop :with f
:= (reference (sat-env-false env
))
63 :with manager
:= (sat-env-manager env
)
64 :with vars
:= (sat-env-vars env
)
65 :for x
:of-type fixnum
:in c
66 :as var
:= (svref vars
(the cudd-int
(abs x
)))
67 :as phase
:= (signum x
)
68 :do
(let* ((var (if (= 1 phase
)
70 (cuddapi:cudd-bdd-nand manager var var
)))
71 (tmp (cuddapi:cudd-bdd-or manager var f
)))
73 (dereference f manager
)
77 (defun sat-env-add-clause (env c
)
78 (let* ((subtree (make-clause-tree env c
))
79 (newcnf (cuddapi:cudd-bdd-and
(sat-env-manager env
)
80 (sat-env-cnf env
) subtree
)))
82 (cuddapi:cudd-ref newcnf
)
83 ;; deref consumed old tree
84 (cuddapi:cudd-recursive-deref
(sat-env-manager env
) (sat-env-cnf env
))
85 (cuddapi:cudd-recursive-deref
(sat-env-manager env
) subtree
)
86 (setf (sat-env-cnf env
) newcnf
))
89 (defun destroy-sat-env (env)
90 (with-slots (name manager cnf vars
)
92 (declare (type simple-vector vars
))
93 (format *debug-io
* "~&Cleaning up sat-env ~A, tree has ~D nodes~%" name
94 (cuddapi:cudd-dag-size cnf
))
95 ;; goes to stderr, unfortunately:
96 ;; (cuddapi:cudd-print-debug manager cnf (length (sat-env-vars env)) 4)
97 ;; (cuddapi:cudd-print-minterm manager cnf)
99 ;; (format *debug-io* " ~D refs initially~%"
100 ;; (cuddapi:cudd-check-zero-ref manager))
101 (cuddapi:cudd-recursive-deref manager cnf
)
102 (when (= 0 (the cudd-int
(cuddapi:cudd-check-zero-ref manager
)))
103 (break "env ~A empty too early: ~A" name env
))
105 ;; (format *debug-io* " destroyed tree, ~D left~%"
106 ;; (cuddapi:cudd-check-zero-ref manager))
107 (when (/= (length vars
) (the cudd-int
(cuddapi:cudd-check-zero-ref manager
)))
108 (break "env ~A occupation does not match varcount: ~D vs ~D; ~A"
111 (cuddapi:cudd-check-zero-ref manager
)
114 (loop :for x
:across vars
115 :do
(cuddapi:cudd-deref x
))
116 ;; (format *debug-io* " ~D vars deleted, ~D left~%"
117 ;; (length vars) (cuddapi:cudd-check-zero-ref manager))
118 (unless (= 0 (the cudd-int
(cuddapi:cudd-check-zero-ref manager
)))
119 (break "env ~A unclean: ~A" name env
))
120 (unless (= 0 (the cudd-int
(cuddapi:cudd-debug-check manager
)))
121 (break "debug check failed ~D~%" (cuddapi:cudd-debug-check manager
)))
123 (cuddapi:cudd-quit manager
)
124 ;; (format *debug-io* " done.~%")
128 (defun make-cnf (numatoms clauses
)
129 (let* ((name (gensym "cnf-sat-env"))
130 (manager (make-cudd-manager :initial-num-vars
(1+ numatoms
)))
131 (truevar (cuddapi:cudd-read-one manager
))
132 (falsevar (cuddapi:cudd-read-logic-zero manager
))
133 (vars (coerce (the list
134 (loop :for i
:of-type fixnum
:from
0 :upto numatoms
135 :collecting
(reference (cuddapi:cudd-bdd-new-var manager
))))
137 (env (make-sat-env :name name
143 (cuddapi:cudd-ref truevar
) ;; it is used as inital cnf
144 (cuddapi:cudd-enable-reordering-reporting manager
)
145 (cuddapi:cudd-autodyn-enable manager
:cudd-reorder-symm-sift
)
146 ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift-conv)
147 ; (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift)
148 (loop :for c
:in clauses
149 :do
(sat-env-add-clause env c
))
154 (defmacro with-sat-bdd
((name numatoms clauses
) &body body
)
155 `(let ((,name
(make-cnf ,numatoms
,clauses
)))
156 (declare (dynamic-extent ,name
))
159 (destroy-sat-env ,name
))))
161 (defun satisfiablep (sat-env f
)
164 (cuddapi:cudd-bdd-leq
(sat-env-manager sat-env
)
165 f
(sat-env-false sat-env
)))))
167 (defun get-essential-vars (sat-env)
168 "Return a list of two lists: the indices of vars fixed to FALSE and those
169 fixed to TRUE in the current cnf of sat-env"
172 (loop :with bdd
:= (reference (sat-env-cnf sat-env
))
173 :with manager
:= (sat-env-manager sat-env
)
174 :for i
:of-type fixnum
:from
1 :below
(length (sat-env-vars sat-env
))
175 :as var
:= (svref (sat-env-vars sat-env
) i
)
176 :as negvar
:= (cuddapi:cudd-bdd-nand manager var var
)
177 :do
(let ((tmp1 (reference
178 (cuddapi:cudd-bdd-and manager var bdd
)))
180 (cuddapi:cudd-bdd-and manager negvar bdd
))))
181 (let ((sat-with-T (satisfiablep sat-env tmp1
))
182 (sat-with-F (satisfiablep sat-env tmp2
)))
184 ((or (and sat-with-T sat-with-F
)
185 (and (not sat-with-T
) (not sat-with-F
)))
186 (dereference tmp1 manager
)
187 (dereference tmp2 manager
))
188 ((and sat-with-T
(not sat-with-F
))
190 (dereference bdd manager
)
191 (dereference tmp2 manager
)
193 ((and (not sat-with-T
) sat-with-F
)
195 (dereference bdd manager
)
196 (dereference tmp1 manager
)
198 :finally
(dereference bdd manager
))
204 (defun satcheck (numatoms clauses
)
205 "Check the CNF of CLAUSES or satisfiability.
206 NUMATOMS is the number of variables occuring in clauses, they are numbered from 1 through NUMATOMS.
207 CLAUSES is a list of lists, where the sublists are (sparse) disjunctions of atom-indices. Positive/negative sign of index determine phase of literal in the clause.
208 Return 3 values: T or NIL to answer SAT(clauses), and two lists of fixed-to-1 and fixed-to-0 atoms."
209 (with-sat-bdd (bdd numatoms clauses
)
211 (satisfiablep bdd
(sat-env-cnf bdd
))
212 (get-essential-vars bdd
))
214 ;; (format T "computing...~%")
217 (defmacro with-index-hash
((mapping &key
(test 'cl
:eq
)) objects
&body body
)
218 "Execute BODY while binding MAPPING to a hash-table (with predicate
219 TEST, defaults to #'cl:eq) mapping the OBJECTS to small integers."
220 `(let ((,mapping
(loop :with ht
:= (make-hash-table :test
,test
)
223 :do
(setf (gethash x ht
) num
)
224 :finally
(return ht
))))
227 (defun clauses-for-if (lhs rhs
)
228 "Return clauses for LHS -> RHS, both being disjunctions."
229 (mapcar #'(lambda (lhsatom)
230 (cons (- lhsatom
) rhs
))
233 (defun clauses-for-iff (lhs rhs
)
234 "Return clauses for LHS -> RHS, both being disjunctions."
235 (append (clauses-for-if lhs rhs
)
236 (clauses-for-if rhs lhs
)))
238 (defun testsat (numvars numclauses
&key
239 (maxlhs (/ numvars
2))
240 (maxrhs (/ numvars
2)))
241 (declare (type fixnum numvars numclauses
))
242 (setf maxlhs
(ceiling maxlhs
))
243 (setf maxrhs
(ceiling maxrhs
))
245 (declare (type fixnum maxlhs maxrhs
))
246 (loop :repeat numclauses
247 :as lhs
:= (loop :repeat
(random maxlhs
)
248 :collecting
(1+ (random numvars
)))
249 :as rhs
:= (loop :repeat
(random maxrhs
)
250 :collecting
(1+ (random numvars
)))
251 :do
(dolist (c (clauses-for-iff lhs rhs
))
253 ; (format T "~D ~A~%" numvars clauses)
254 (satcheck numvars clauses
)))