modify default solver parameters
[cl-cudd.git] / cuddsat.lisp
blobb31df5c27625c901cae83120c8a2f736d730c895
1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
2 ;;;
3 ;;; cuddsat.lisp --- SAT solver based on CUDD BDDs
5 ;; Copyright (C) 2009 Utz-Uwe Haus <lisp@uuhaus.de>
6 ;; $Id:$
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
24 ;; Commentary:
26 ;;
28 ;;; Code:
30 (eval-when (:compile-toplevel :load-toplevel)
31 (declaim (optimize (speed 3) (debug 1) (safety 1))))
34 (in-package #:CUDD)
37 (defstruct sat-env
38 (name)
39 (manager)
40 (cnf)
41 (true)
42 (false)
43 (vars #() :type simple-vector))
45 (defmacro reference (f)
46 (let ((x (gensym)))
47 `(let ((,x ,f))
48 (cuddapi:cudd-ref ,x)
49 ,x)))
51 (defmacro dereference (f manager)
52 (let ((x (gensym)))
53 `(let ((,x ,f))
54 (cuddapi:cudd-recursive-deref ,manager ,x)
55 ,x)))
57 (deftype cudd-int ()
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)
69 var
70 (cuddapi:cudd-bdd-nand manager var var)))
71 (tmp (cuddapi:cudd-bdd-or manager var f)))
72 (reference tmp)
73 (dereference f manager)
74 (setf f tmp))
75 :finally (return f)))
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)))
81 ;; reference new tree
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))
87 (values))
89 (defun destroy-sat-env (env)
90 (with-slots (name manager cnf vars)
91 env
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"
109 name
110 (length vars)
111 (cuddapi:cudd-check-zero-ref manager)
112 env))
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))))
136 'simple-vector))
137 (env (make-sat-env :name name
138 :manager manager
139 :cnf truevar
140 :true truevar
141 :false falsevar
142 :vars vars)))
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-sift)
148 (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift)
149 (cuddapi:cudd-autodyn-enable manager :cudd-reorder-window-4)
150 (cuddapi:cudd-set-max-growth manager 12d0)
151 (format T ";; cudd: max sift growth ~D, max number of variables sifted: ~D~%"
152 (cuddapi:cudd-read-max-growth manager)
153 (cuddapi:cudd-read-sift-max-var manager))
154 (loop :for c :in clauses
155 :with numclauses := (length clauses)
156 :for counter :downfrom numclauses
157 :do (sat-env-add-clause env c)
158 :when (= 0 (mod counter 10))
159 :do (format T "~&;; ~D clauses to go~%" counter))
160 env))
164 (defmacro with-sat-bdd ((name numatoms clauses) &body body)
165 `(let ((,name (make-cnf ,numatoms ,clauses)))
166 (declare (dynamic-extent ,name))
167 (unwind-protect
168 (progn ,@body)
169 (destroy-sat-env ,name))))
171 (defun satisfiablep (sat-env f)
172 (= 0
173 (the cudd-int
174 (cuddapi:cudd-bdd-leq (sat-env-manager sat-env)
175 f (sat-env-false sat-env)))))
177 (defun get-essential-vars (sat-env)
178 "Return a list of two lists: the indices of vars fixed to FALSE and those
179 fixed to TRUE in the current cnf of sat-env"
180 (let ((t-ess '())
181 (f-ess '()))
182 (loop :with bdd := (reference (sat-env-cnf sat-env))
183 :with manager := (sat-env-manager sat-env)
184 :for i :of-type fixnum :from 1 :below (length (sat-env-vars sat-env))
185 :as var := (svref (sat-env-vars sat-env) i)
186 :as negvar := (cuddapi:cudd-bdd-nand manager var var)
187 :do (let ((tmp1 (reference
188 (cuddapi:cudd-bdd-and manager var bdd)))
189 (tmp2 (reference
190 (cuddapi:cudd-bdd-and manager negvar bdd))))
191 (let ((sat-with-T (satisfiablep sat-env tmp1))
192 (sat-with-F (satisfiablep sat-env tmp2)))
193 (cond
194 ((or (and sat-with-T sat-with-F)
195 (and (not sat-with-T) (not sat-with-F)))
196 (dereference tmp1 manager)
197 (dereference tmp2 manager))
198 ((and sat-with-T (not sat-with-F))
199 (push i t-ess)
200 (dereference bdd manager)
201 (dereference tmp2 manager)
202 (setf bdd tmp1))
203 ((and (not sat-with-T) sat-with-F)
204 (push i f-ess)
205 (dereference bdd manager)
206 (dereference tmp1 manager)
207 (setf bdd tmp2)))))
208 :finally (dereference bdd manager))
209 (list f-ess t-ess)))
214 (defun satcheck (numatoms clauses)
215 "Check the CNF of CLAUSES or satisfiability.
216 NUMATOMS is the number of variables occuring in clauses, they are numbered from 1 through NUMATOMS.
217 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.
218 Return 3 values: T or NIL to answer SAT(clauses), and two lists of fixed-to-1 and fixed-to-0 atoms."
219 (with-sat-bdd (bdd numatoms clauses)
220 (apply #'values
221 (satisfiablep bdd (sat-env-cnf bdd))
222 (get-essential-vars bdd))
224 ;; (format T "computing...~%")
227 (defmacro with-index-hash ((mapping &key (test 'cl:eq)) objects &body body)
228 "Execute BODY while binding MAPPING to a hash-table (with predicate
229 TEST, defaults to #'cl:eq) mapping the OBJECTS to small integers."
230 `(let ((,mapping (loop :with ht := (make-hash-table :test ,test)
231 :for x :in ,objects
232 :for num :from 1
233 :do (setf (gethash x ht) num)
234 :finally (return ht))))
235 ,@body))
237 (defun clauses-for-if (lhs rhs)
238 "Return clauses for LHS -> RHS, both being disjunctions."
239 (mapcar #'(lambda (lhsatom)
240 (cons (- lhsatom) rhs))
241 lhs))
243 (defun clauses-for-iff (lhs rhs)
244 "Return clauses for LHS -> RHS, both being disjunctions."
245 (append (clauses-for-if lhs rhs)
246 (clauses-for-if rhs lhs)))
248 (defun testsat (numvars numclauses &key
249 (maxlhs (/ numvars 2))
250 (maxrhs (/ numvars 2)))
251 (declare (type fixnum numvars numclauses))
252 (setf maxlhs (ceiling maxlhs))
253 (setf maxrhs (ceiling maxrhs))
254 (let ((clauses '()))
255 (declare (type fixnum maxlhs maxrhs))
256 (loop :repeat numclauses
257 :as lhs := (loop :repeat (random maxlhs)
258 :collecting (1+ (random numvars)))
259 :as rhs := (loop :repeat (random maxrhs)
260 :collecting (1+ (random numvars)))
261 :do (dolist (c (clauses-for-iff lhs rhs))
262 (push c clauses)))
263 ; (format T "~D ~A~%" numvars clauses)
264 (satcheck numvars clauses)))