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-symm-sift)
 148     (loop :for c :in clauses
 149        :do (sat-env-add-clause env c))
 150     env))
 151
 152
 153
 154 (defmacro with-sat-bdd ((name numatoms clauses) &body body)
 155   `(let ((,name (make-cnf ,numatoms ,clauses)))
 156      (declare (dynamic-extent ,name))
 157      (unwind-protect
 158           (progn ,@body)
 159        (destroy-sat-env ,name))))
 160
 161 (defun satisfiablep (sat-env f)
 162   (= 0
 163      (the cudd-int
 164        (cuddapi:cudd-bdd-leq (sat-env-manager sat-env)
 165                              f (sat-env-false sat-env)))))
 166
 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"
 170   (let ((t-ess '())
 171         (f-ess '()))
 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)))
 179                  (tmp2 (reference
 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)))
 183                (cond
 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))
 189                   (push i t-ess)
 190                   (dereference bdd manager)
 191                   (dereference tmp2 manager)
 192                   (setf bdd tmp1))
 193                  ((and (not sat-with-T) sat-with-F)
 194                   (push i f-ess)
 195                   (dereference bdd manager)
 196                   (dereference tmp1 manager)
 197                   (setf bdd tmp2)))))
 198        :finally (dereference bdd manager))
 199      (list f-ess t-ess)))
 200
 201
 202 \f
 203
 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)
 210     (apply #'values
 211            (satisfiablep bdd (sat-env-cnf bdd))
 212            (get-essential-vars bdd))
 213
 214     ;; (format T "computing...~%")
 215     ))
 216
 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)
 221                      :for x :in ,objects
 222                       :for num :from 1
 223                       :do (setf (gethash x ht) num)
 224                       :finally (return ht))))
 225      ,@body))
 226
 227 (defun clauses-for-if (lhs rhs)
 228   "Return clauses for LHS -> RHS, both being disjunctions."
 229   (mapcar #'(lambda (lhsatom)
 230               (cons (- lhsatom) rhs))
 231           lhs))
 232
 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)))
 237
 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))
 244   (let ((clauses '()))
 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))
 252              (push c clauses)))
 253     ;    (format T "~D ~A~%" numvars clauses)
 254     (satcheck numvars clauses)))