satwrap.lisp

   1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
   2 ;;;
   3 ;;; satwrap.lisp --- SAT solvers wrapped for CL
   4
   5 ;; Copyright (C) 2010 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 #:satwrap)
  35 \f
  36 (defvar *default-sat-backend* :minisat
  37   "Name of the default backend to be used by make-sat-solver.")
  38
  39 (defparameter *satwrap-backends*
  40   `((:precosat . ,(find-class 'satwrap.precosat:precosat-backend))
  41     (:minisat  . ,(find-class 'satwrap.minisat:minisat-backend)))
  42   "Alist of symbolic name to backend class name for all supported backends.")
  43
  44 (defun describe-supported-backends ()
  45   "Return a list of (designator . description) pairs of the supported backends"
  46   (loop :for (key . class) :in *satwrap-backends*
  47      :as descr := (let ((instance (make-instance class)))
  48                     (format nil "~A version ~A"
  49                             (satwrap.backend:sat-backend-name instance)
  50                             (satwrap.backend:sat-backend-version instance)))
  51      :collect `(,key . ,descr)))
  52
  53 \f
  54 ;;; Frontend:
  55 (defclass sat-solver ()
  56   ((backend :initarg :backend :accessor sat-solver-backend)
  57    (numvars :initform 0 :accessor sat-solver-numvars)
  58    ;; CNF; split into 'old' and 'new' to allow incremental solving
  59    (new-clauses :initform '() :accessor sat-solver-new-clauses)
  60    (old-clauses :initform '() :accessor sat-solver-old-clauses)
  61    )
  62   (:default-initargs :backend (make-instance (cdr (assoc *default-sat-backend*
  63                                                          *satwrap-backends*))))
  64   (:documentation "A Sat solver abstraction"))
  65
  66 (defmethod sat-solver-numclauses ((solver sat-solver))
  67   (+ (length (sat-solver-new-clauses solver))
  68      (length (sat-solver-old-clauses solver))
  69      ))
  70
  71 (defmethod print-object ((solver sat-solver) stream)
  72   (print-unreadable-object (solver stream :type T :identity T)
  73     (format stream "~D vars, ~D clauses, backend ~A"
  74             (sat-solver-numvars solver)
  75             (sat-solver-numclauses solver)
  76             (sat-solver-backend solver))))
  77
  78 (defmethod clause-valid ((solver sat-solver) (clause list))
  79   "Check that CLAUSE is a valid clause for SOLVER."
  80   (loop
  81      :with max := (sat-solver-numvars solver)
  82      :with min := (- max)
  83      :for v :in clause
  84      :always (and (not (zerop v))
  85                   (<= min v max))))
  86
  87 (defmethod clause-valid ((solver sat-solver) (clause vector))
  88   "Check that CLAUSE is a valid clause for SOLVER."
  89   (loop
  90      :with max := (sat-solver-numvars solver)
  91      :with min := (- max)
  92      :for v :across clause
  93      :always (and (not (zerop v))
  94                   (<= min v max))))
  95
  96 (defmacro iota (n &optional (start 1))
  97   "Return a list of the N sequential integers starting at START (default: 1)."
  98   (let ((i (gensym "i")))
  99     `(loop :repeat ,n
 100         :for ,i :from ,start
 101         :collect ,i)))
 102
 103 (define-condition satwrap-condition (error)
 104   ()
 105   (:documentation "Superclass of all conditions raised by satwrap code."))
 106
 107 (define-condition invalid-clause (satwrap-condition)
 108   ((solver :initarg :solver :reader invalid-clause-solver)
 109    (clause :initarg :clause :reader invalid-clause-clause))
 110   (:report (lambda (condition stream)
 111              (format stream "Invalid clause ~A for solver ~A"
 112                      (invalid-clause-clause condition)
 113                      (invalid-clause-solver condition)))))
 114
 115 (define-condition invalid-backend (satwrap-condition)
 116   ((name :initarg :name :reader invalid-backend-name))
 117   (:report (lambda (condition stream)
 118              (declare (special *satwrap-backends* *default-sat-backend*))
 119              (format stream "Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
 120                      (invalid-backend-name condition)
 121                      (mapcar #'car *satwrap-backends*)
 122                      *default-sat-backend*))))
 123
 124 (defmethod flush-to-backend ((solver sat-solver))
 125   "Populate backend, possibly flushing old backend contents."
 126   (let ((deleted '()))
 127     (satwrap.backend:synchronize-backend (sat-solver-backend solver)
 128                                          (sat-solver-numvars solver)
 129                                          (sat-solver-new-clauses solver)
 130                                          deleted
 131                                          (sat-solver-old-clauses solver))
 132     (setf (sat-solver-old-clauses solver)
 133           (nconc (sat-solver-new-clauses solver)
 134                  (if deleted
 135                      (delete-if #'(lambda (c)
 136                                     (find c deleted :test #'equal))
 137                                 (sat-solver-old-clauses solver))
 138                      (sat-solver-old-clauses solver))))
 139     (setf (sat-solver-new-clauses solver) '())))
 140
 141 \f
 142 (defun make-sat-solver (&optional (backend *default-sat-backend*))
 143   "Return a new sat solver instance. Optional argument BACKEND can be used to
 144 specify which backend should be used. It defaults to *default-sat-backend*."
 145   (let ((be (assoc backend *satwrap-backends* :test #'eq)))
 146     (if be
 147         (make-instance 'sat-solver :backend (make-instance (cdr be)))
 148         (error 'invalid-backend :name backend))))
 149
 150 (defgeneric add-variable (solver)
 151   (:documentation "Add another variable to SOLVER. Returns new variable index.")
 152   (:method ((solver sat-solver))
 153     (incf (sat-solver-numvars solver))))
 154
 155 (defgeneric add-clause (solver clause)
 156   (:documentation "Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
 157   (:method ((solver sat-solver) (clause list))
 158     (if (clause-valid solver clause)
 159         (push clause (sat-solver-new-clauses solver))
 160         (error 'invalid-clause :clause clause :solver solver)))
 161   (:method ((solver sat-solver) (clause vector))
 162     (add-clause solver (coerce clause 'list))))
 163
 164 (defgeneric add-clauses (solver clauses)
 165   (:documentation "Add CLAUSES to SOLVER's cnf formula. Clauses are consumed.")
 166   (:method ((solver sat-solver) (clauses list))
 167     (dolist (c clauses)
 168       (add-clause solver c))))
 169
 170 (defgeneric satisfiablep (solver &key assume)
 171   (:documentation "Check whether current CNF in SOLVER is satisfiable.
 172 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
 173 Returns T or NIL.")
 174   (:method ((solver sat-solver) &key (assume '()))
 175     (if (clause-valid solver assume) ;; misusing 'clause' concept here
 176         (progn
 177           (flush-to-backend solver)
 178           (satwrap.backend:satisfiablep (sat-solver-backend solver) assume))
 179         (error 'invalid-clause :clause assume :solver solver))))
 180
 181 (defgeneric solution (solver &key interesting-vars)
 182   (:documentation "Return solution for SOLVER. If unsat, return '(). If sat return
 183 sequence of 0/1 values for variables [1...N]. Keyword argument INTERESTING-VARS can be used to restrict the variables whose values are reported. Solution components will be in the same order that INTERESTING-VARS lists the variables in.")
 184   (:method ((solver sat-solver)
 185             &key (interesting-vars (iota (sat-solver-numvars solver))))
 186     (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
 187
 188 (defgeneric get-essential-variables (solver)
 189   (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
 190 Returns a list of literals fixed, sign according to phase.")
 191   (:method ((solver sat-solver))
 192     ;; The backend may define a specialized method, but then it has to
 193     ;; work on the one copy of data flushed to the solver. Precosat for example
 194     ;; does not allow that, so we define the universal implementation here instead of
 195     ;; a default implementation in the backend.
 196     (let ((have-specialized-method
 197            (find-method #'satwrap.backend:get-essential-variables
 198                         '()
 199                         `(,(class-of (sat-solver-backend solver)))
 200                         nil)))
 201       (if have-specialized-method
 202           (progn
 203             (flush-to-backend solver)
 204             (satwrap.backend:get-essential-variables (sat-solver-backend solver)))
 205           (let ((fixed '()))
 206             (loop :for var :of-type (integer 1) :in (iota (sat-solver-numvars solver))
 207                :as sat-for-+ := (satisfiablep solver :assume `(,var ,@fixed ))
 208                :as sat-for-- := (satisfiablep solver :assume `(,(- var) ,@fixed))
 209                :do (cond
 210                      ((and sat-for-+ (not sat-for--))
 211                       (push var fixed))
 212                      ((and (not sat-for-+) sat-for--)
 213                       (push (- var) fixed))))
 214             fixed)))))
 215
 216 \f
 217 (defmacro with-sat-solver ((name numatoms &key (backend *default-sat-backend* backend-given))
 218                            &body body)
 219   "Bind NAME to a fresh sat-solver with backend :BACKEND (default: *default-sat-backend*) and declare NUMATOMS variables numbered 1..NUMATOMS for the duration of BODY."
 220   `(let ((,name (make-sat-solver ,(if backend-given
 221                                       backend
 222                                       '*default-sat-backend*))))
 223      (loop :repeat ,numatoms :do (add-variable ,name))
 224      (locally
 225          ,@body)))
 226
 227 (defmacro with-index-hash ((mapping &key (test '#'eq)) objects &body body)
 228   "Execute BODY while binding MAPPING to a hash-table (with predicate
 229 TEST, defaults to #'cl:eq) mapping the elements of the sequence OBJECTS
 230 to integer 1..[length objects].
 231 Typically used to map objects to variables inside WITH-SAT-SOLVER."
 232   (let ((o (gensym "objects")))
 233     `(let* ((,o ,objects)
 234             (,mapping (etypecase ,o
 235                        (list (loop :with ht := (make-hash-table :test ,test)
 236                                 :for x :in ,o
 237                                 :for num :of-type fixnum :from 1
 238                                 :do (setf (gethash x ht) num)
 239                                 :finally (return ht)))
 240                        (vector (loop :with ht := (make-hash-table :test ,test)
 241                                   :for x :across ,o
 242                                   :for num :of-type fixnum :from 1
 243                                   :do (setf (gethash x ht) num)
 244                                   :finally (return ht))))))
 245        ,@body)))
 246 \f
 247 ;; convenience syntax for logical operations:
 248 (defun standardize (tree)
 249   "Convert tree of logical operations to elementary :NOT, :AND, :OR tree (preserving :ATOM).
 250 Supports :IMPLY, :IFF, binary :XOR, and :NOR. "
 251   (cond
 252     ((consp tree)
 253      (destructuring-bind (op . expr)
 254          tree
 255        (case op
 256          ((:IMPLY :IMPLIES)
 257           (if (= 2 (length expr))
 258               `(:OR (:NOT ,(standardize (car expr)))
 259                     ,(standardize (cadr expr)))
 260               (error "non-binary :IMPLY operation: ~A" tree)))
 261          (:IFF
 262           (if (= 2 (length expr))
 263               `(:AND ,(standardize `(:IMPLIES ,(car expr) ,(cadr expr)))
 264                      ,(standardize `(:IMPLIES ,(cadr expr) ,(car expr))))
 265               (error "non-binary :IFF operation: ~A" tree)))
 266          (:XOR
 267           (if (= 2 (length expr))
 268               (let ((e1 (standardize (first expr)))
 269                     (e2 (standardize (second expr))))
 270                 `(:OR (:AND ,e1 (:NOT ,e2))
 271                       (:AND ,e2 (:NOT ,e1))))
 272               (error "non-binary :XOR operation: ~A" tree)))
 273          (:NOR
 274           `(:AND ,@(mapcar #'(lambda (p) `(:NOT ,(standardize p))) expr)))
 275
 276          (T `(,op ,@(mapcar #'standardize expr))))))
 277     (T tree)))
 278
 279 (defun standard-tree->nnf (tree)
 280   "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree."
 281   (cond
 282     ((consp tree)
 283      (destructuring-bind (op . expr)
 284          tree
 285        (case op
 286          (:NOT (if (= 1 (length expr))
 287                    (let ((subexpr (first expr)))
 288                      (if (consp subexpr)
 289                          (case (first subexpr)
 290                            ;; double-not: drop 2 levels
 291                            (:NOT (standard-tree->nnf (cadr subexpr)))
 292                            ;; NOT AND:
 293                            (:AND `(:OR ,@(mapcar #'(lambda (c)
 294                                                      (standard-tree->nnf `(:NOT ,c)))
 295                                                  (cdr subexpr))))
 296                            ;; NOT OR:
 297                            (:OR  `(:AND ,@(mapcar #'(lambda (c)
 298                                                       (standard-tree->nnf `(:NOT ,c)))
 299                                                   (cdr subexpr))))
 300                            ;; `quoted' atom: keep
 301                            (:ATOM `(:NOT ,subexpr))
 302                            (otherwise `(:NOT ,subexpr)))
 303                          ;; non-quoted atom:
 304                          `(:NOT ,subexpr)))
 305                    (error "non-unary :NOT expression: ~W" tree)))
 306          ;; other operators: AND, OR, ATOM: descend
 307          (T
 308           `(,op ,@(mapcar #'standard-tree->nnf expr))))))
 309     ;; non-cons: stop
 310     (T tree)))
 311
 312 (defun crossprod (list-of-lists)
 313   "Return a list of all lists containing one element from each sublist of LIST-OF-LISTS."
 314   (reduce #'(lambda (collected term)
 315               (loop :for x :in term :appending
 316                  (loop :for tail :in collected
 317                     :collect `(,x ,@tail))))
 318           list-of-lists
 319           :initial-value '(())))
 320
 321 (defun is-cnf (tree)
 322   "Check that TREE is in CNF."
 323   (flet ((and-form (f)
 324            (and (consp f)
 325                 (eq :AND (car f))))
 326          (or-form (f)
 327            (and (consp f)
 328                 (eq :OR (car f))))
 329          (atomic (f)
 330            (if (consp f)
 331                (and (not (eq :OR (car f)))
 332                     (not (eq :AND (car f))))
 333                T)))
 334     (if (atomic tree)
 335         T
 336         (and (and-form tree)
 337              (every #'(lambda (c)
 338                         (or (atomic c)
 339                             (and (or-form c)
 340                                  (every #'atomic (cdr c)))))
 341                     (cdr tree))))))
 342
 343 (defun distribute (tree)
 344   "Pull out :ANDs to reduce standardized tree in NNF to CNF."
 345   (if (consp tree)
 346       (case (car tree)
 347         (:AND (let ((sub-cnfs (mapcar #'distribute (cdr tree))))
 348                 (assert (every #'is-cnf sub-cnfs)
 349                         (sub-cnfs)
 350                         "Not all in CNF: ~{~A~^~%~}" sub-cnfs)
 351                 (let (clauses)
 352                   (loop :for sub-cnf :in sub-cnfs
 353                      :if (and (consp sub-cnf)
 354                               (eq :AND (car sub-cnf)))
 355                      ;; AND(AND  ..) = AND ..
 356                      :do (dolist (clause (cdr sub-cnf))
 357                            (push clause clauses))
 358                      :else :do (push sub-cnf clauses))
 359                   `(:AND ,@clauses))))
 360         (:OR (let (ands)
 361                (dolist (term (mapcar #'distribute (cdr tree)))
 362                  (assert (is-cnf term)
 363                          (term)
 364                          "~A not in CNF" term)
 365                  (if (consp term)
 366                      (case (car term)
 367                        (:AND (push (cdr term) ands))
 368                        (:OR (dolist (c (cdr term))
 369                               (push `(,c) ands)))
 370                        (otherwise (push `(,term) ands)))
 371                      (push `(,term) ands)))
 372                (let ((clauses (crossprod ands)))
 373                  `(:AND ,@(mapcar #'(lambda (c)
 374                                       (if (not (consp c))
 375                                           c
 376                                           `(:OR ,@ (loop :for subterm :in c
 377                                                       :if (and (consp subterm)
 378                                                                (eq :OR (car subterm)))
 379                                                       ;; (OR(OR...)) == (OR ...)
 380                                                       :append (cdr subterm)
 381                                                       ;; if C is not an OR-clause
 382                                                       ;; it is considered atomic:
 383                                                       :else :append `(,subterm)))))
 384                                   clauses)))))
 385         (otherwise
 386          tree))
 387       tree))
 388
 389
 390 (defun tree->cnf (tree &optional (mapping #'cl:identity) (atom-test #'eql))
 391   "Convert TREE to CNF,  applying MAPPING to atoms and afterwards and removing duplicate literals in clauses using atom-test to test for equality. Also simplifies trivially fulfilled clauses to empty clause."
 392   (labels ((atomic (f)
 393              (if (consp f)
 394                  (and (not (eq :OR (car f)))
 395                       (not (eq :AND (car f))))
 396                  T))
 397            (map-literals (cnf)
 398              ;; destructively apply MAPPING
 399              (if (atomic cnf)
 400                  (setf cnf (funcall mapping cnf))
 401                  (setf (cdr cnf) ;; we must be looking at an AND
 402                        (mapcar #'(lambda (clause)
 403                                    (if (atomic clause)
 404                                        (funcall mapping clause)
 405                                        `(:OR ,@(mapcar #'(lambda (lit)
 406                                                            (funcall mapping lit))
 407                                                        (cdr clause)))))
 408                                (cdr cnf))))
 409              cnf)
 410            (negated-litp (lit)
 411              (and (consp lit) (eq :NOT (car lit))))
 412            (atom-for (lit)
 413              (if (consp lit)
 414                  (case (car lit)
 415                    (:NOT (atom-for (second lit)))
 416                    (:ATOM (second lit))
 417                    (otherwise lit))
 418                  lit))
 419            (duplicate-literalsp (l1 l2)
 420              (funcall atom-test (atom-for l1) (atom-for l2)))
 421            (trivial-clausep (c)
 422              (loop :for (lit . haystack) :on c
 423                 :as needle := (atom-for lit)
 424                 :as negated := (and (consp lit) (eq :NOT (car lit)))
 425                 :when (find-if #'(lambda (x)
 426                                    (and (if negated
 427                                             (not (negated-litp x))
 428                                             (negated-litp x))
 429                                         (funcall atom-test needle (atom-for x))))
 430                                haystack)
 431                 :return T
 432                 :finally (return NIL)))
 433            (clean-clauses (cnf)
 434              ;; destructively apply MAPPING
 435              (if (atomic cnf)
 436                  (setf cnf cnf)
 437                  (setf (cdr cnf) ;; we must be looking at an AND
 438                        (loop :for clause :in (cdr cnf)
 439                           :if (atomic clause)
 440                           :collect clause
 441                           :else :if (not (trivial-clausep clause))
 442                           :collect `(:OR ,@(remove-duplicates
 443                                             (cdr clause)
 444                                             :test #'duplicate-literalsp)))))
 445              cnf))
 446     (clean-clauses
 447      (map-literals
 448       (distribute
 449        (standard-tree->nnf
 450         (standardize tree)))))))
 451
 452
 453 (defgeneric add-formula (solver formula &key mapping atom-test)
 454   (:documentation "Add logical FORMULA to SOLVER.
 455 Formula is an expression tree that can contain high-level abbreviations :IMPLY, :IFF, :NOR and :XOR, as well as the basic :AND, :OR, :NOT. Everything else is considered an atom. Atoms can also be explicitly written as (:ATOM foo).
 456 All atoms will be mapped through MAPPING before being added to the solver to convert your favorite atoms to phased variables. MAPPING is a function of 1 argument, the atom. It defaults to  #'identity. Afterwards, clean clauses (removing duplicates and simplifying trivial clauses, comparing atoms using ATOM-TEST (default: #'eql).")
 457   (:method ((solver sat-solver) (formula list) &key (mapping #'identity) (atom-test #'eql))
 458     (dolist (c (cdr ;; drop outer :AND
 459                 (tree->cnf formula mapping atom-test)))
 460       (add-clause solver (cdr ;; drop :OR
 461                           c)))))
 462
 463 (defgeneric add-and (solver literals &key mapping)
 464   (:documentation "Add clauses for AND(literals) to SOLVER.")
 465   (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
 466     (add-formula solver `(:AND ,@literals) mapping)))
 467
 468 (defgeneric add-or (solver literals &key mapping)
 469   (:documentation "Add clauses for OR(literals) to SOLVER.")
 470   (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
 471     (add-formula solver `(:OR ,@literals) mapping)))
 472
 473 (defgeneric add-xor (solver literals &key mapping)
 474   (:documentation "Add clauses for binary XOR(literals) to SOLVER.")
 475   (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
 476     (add-formula solver `(:XOR ,@literals) mapping)))
 477
 478 (defgeneric add-if (solver lhs rhs &key mapping)
 479   (:documentation "Add clauses for lhs -> rhs to SOLVER.")
 480   (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity))
 481     (add-formula solver `(:IMPLIES ,lhs ,rhs) mapping)))
 482
 483 (defgeneric add-iff (solver lhs rhs &key mapping)
 484   (:documentation "Add clauses for lhs <-> rhs to SOLVER.")
 485   (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity))
 486     (add-formula solver `(:IFF ,lhs ,rhs) mapping)))