cuddsat.lisp

   1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
   2 ;;;
   3 ;;; cuddsat.lisp --- SAT solver based on CUDD BDDs
   4
   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.
  11 ;;
  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.
  16 ;;
  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
  23 ;;
  24 ;; Commentary:
  25
  26 ;;
  27
  28 ;;; Code:
  29
  30 (eval-when (:compile-toplevel :load-toplevel)
  31   (declaim (optimize (speed 3) (debug 1) (safety 1))))
  32
  33
  34 (in-package #:CUDD)
  35 \f
  36
  37 (defstruct sat-env
  38   (name)
  39   (manager)
  40   (cnf)
  41   (true)
  42   (false)
  43   (vars #() :type simple-vector))
  44
  45 (defmacro reference (f)
  46   (let ((x (gensym)))
  47     `(let ((,x ,f))
  48        (cuddapi:cudd-ref ,x)
  49        ,x)))
  50
  51 (defmacro dereference (f manager)
  52   (let ((x (gensym)))
  53     `(let ((,x ,f))
  54        (cuddapi:cudd-recursive-deref ,manager ,x)
  55        ,x)))
  56
  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)))))
  60
  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)))
  76
  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))
  88
  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)
  98
  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))
 104
 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))
 113
 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)))
 122
 123     (cuddapi:cudd-quit manager)
 124 ;;    (format *debug-io* " done.~%")
 125
 126     ))
 127
 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))
 161
 162
 163
 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))))
 170
 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)))))
 176
 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)))
 210
 211
 212 \f
 213
 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))
 223
 224     ;; (format T "computing...~%")
 225     ))
 226
 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))
 236
 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))
 242
 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)))
 247
 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)))