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 (defmacro iota (n &optional (start 1))
  88   "Return a list of the N sequential integers starting at START (default: 1)."
  89   (let ((i (gensym "i")))
  90     `(loop :repeat ,n
  91         :for ,i :from ,start
  92         :collect ,i)))
  93
  94 (define-condition satwrap-condition (error)
  95   ()
  96   (:documentation "Superclass of all conditions raised by satwrap code."))
  97
  98 (define-condition invalid-clause (satwrap-condition)
  99   ((solver :initarg :solver :reader invalid-clause-solver)
 100    (clause :initarg :clause :reader invalid-clause-clause))
 101   (:report (lambda (condition stream)
 102              (format stream "Invalid clause ~A for solver ~A"
 103                      (invalid-clause-clause condition)
 104                      (invalid-clause-solver condition)))))
 105
 106 (define-condition invalid-backend (satwrap-condition)
 107   ((name :initarg :name :reader invalid-backend-name))
 108   (:report (lambda (condition stream)
 109              (declare (special *satwrap-backends* *default-sat-backend*))
 110              (format stream "Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
 111                      (invalid-backend-name condition)
 112                      (mapcar #'car *satwrap-backends*)
 113                      *default-sat-backend*))))
 114
 115 (defmethod flush-to-backend ((solver sat-solver))
 116   "Populate backend, possibly flushing old backend contents."
 117   (satwrap.backend:synchronize-backend (sat-solver-backend solver)
 118                                        (sat-solver-numvars solver)
 119                                        (sat-solver-new-clauses solver)
 120                                        '() ;; deleted clauses, not yet supported
 121                                        (sat-solver-old-clauses solver))
 122   (loop :with deleted := '()
 123      :for c :in (sat-solver-old-clauses solver)
 124      :unless (find c deleted :test #'equal)
 125      :do (push c (sat-solver-new-clauses solver)))
 126   (setf (sat-solver-old-clauses solver) (sat-solver-new-clauses solver)
 127         (sat-solver-new-clauses solver) '()))
 128
 129 \f
 130 (defun make-sat-solver (&optional (backend *default-sat-backend*))
 131   "Return a new sat solver instance. Optional argument BACKEND can be used to
 132 specify which backend should be used. It defaults to *default-sat-backend*."
 133   (let ((be (assoc backend *satwrap-backends* :test #'eq)))
 134     (if be
 135         (make-instance 'sat-solver :backend (make-instance (cdr be)))
 136         (error 'invalid-backend :name backend))))
 137
 138 (defgeneric add-variable (solver)
 139   (:documentation "Add another variable to SOLVER. Returns new variable index.")
 140   (:method ((solver sat-solver))
 141     (incf (sat-solver-numvars solver))))
 142
 143 (defgeneric add-clause (solver clause)
 144   (:documentation "Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
 145   (:method ((solver sat-solver) (clause list))
 146     (if (clause-valid solver clause)
 147         (push clause (sat-solver-new-clauses solver))
 148         (error 'invalid-clause :clause clause :solver solver)))
 149   (:method ((solver sat-solver) (clause vector))
 150     (add-clause solver (coerce clause 'list))))
 151
 152 (defgeneric add-clauses (solver clauses)
 153   (:documentation "Add CLAUSES to SOLVER's cnf formula. Clauses are consumed.")
 154   (:method ((solver sat-solver) (clauses list))
 155     (dolist (c clauses)
 156       (add-clause solver c))))
 157
 158 (defgeneric satisfiablep (solver &key assume)
 159   (:documentation "Check whether current CNF in SOLVER is satisfiable.
 160 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
 161 Returns T or NIL.")
 162   (:method ((solver sat-solver) &key (assume '()))
 163     (if (clause-valid solver assume) ;; misusing 'clause' concept here
 164         (progn
 165           (flush-to-backend solver)
 166           (satwrap.backend:satisfiablep (sat-solver-backend solver) assume))
 167         (error 'invalid-clause :clause assume :solver solver))))
 168
 169 (defgeneric solution (solver &key interesting-vars)
 170   (:documentation "Return solution for SOLVER. If unsat, return '(). If sat return
 171 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.")
 172   (:method ((solver sat-solver)
 173             &key (interesting-vars (iota (sat-solver-numvars solver))))
 174     (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
 175
 176 (defgeneric get-essential-variables (solver)
 177   (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
 178 Returns a list of literals fixed, sign according to phase.")
 179   (:method ((solver sat-solver))
 180     ;; The backend may define a specialized method, but then it has to
 181     ;; work on the one copy of data flushed to the solver. Precosat for example
 182     ;; does not allow that, so we define the universal implementation here instead of
 183     ;; a default implementation in the backend.
 184     (let ((have-specialized-method
 185            (find-method #'satwrap.backend:get-essential-variables
 186                         '()
 187                         `(,(class-of (sat-solver-backend solver)))
 188                         nil)))
 189       (if have-specialized-method
 190           (progn
 191             (flush-to-backend solver)
 192             (satwrap.backend:get-essential-variables (sat-solver-backend solver)))
 193           (let ((fixed '()))
 194             (loop :for var :of-type (integer 1) :in (iota (sat-solver-numvars solver))
 195                :as sat-for-+ := (satisfiablep solver :assume `(,var ,@fixed ))
 196                :as sat-for-- := (satisfiablep solver :assume `(,(- var) ,@fixed))
 197                :do (cond
 198                      ((and sat-for-+ (not sat-for--))
 199                       (push var fixed))
 200                      ((and (not sat-for-+) sat-for--)
 201                       (push (- var) fixed))))
 202             fixed)))))
 203
 204 \f
 205 (defmacro with-sat-solver ((name numatoms &key (backend *default-sat-backend* backend-given))
 206                            &body body)
 207   "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."
 208   `(let ((,name (make-sat-solver ,(if backend-given
 209                                       backend
 210                                       '*default-sat-backend*))))
 211      (loop :repeat ,numatoms :do (add-variable ,name))
 212      (locally
 213          ,@body)))
 214
 215 (defmacro with-index-hash ((mapping &key (test 'cl:eq)) objects &body body)
 216   "Execute BODY while binding MAPPING to a hash-table (with predicate
 217 TEST, defaults to #'cl:eq) mapping the elements of the sequence OBJECTS
 218 to integer 1..[length objects].
 219 Typically used to map objects to variables inside WITH-SAT-SOLVER."
 220   (let ((o (gensym "objects")))
 221     `(let* ((,o ,objects)
 222             (,mapping (etypecase ,o
 223                        (list (loop :with ht := (make-hash-table :test ,test)
 224                                 :for x :in ,o
 225                                 :for num :of-type fixnum :from 1
 226                                 :do (setf (gethash x ht) num)
 227                                 :finally (return ht)))
 228                        (vector (loop :with ht := (make-hash-table :test ,test)
 229                                   :for x :across ,o
 230                                   :for num :of-type fixnum :from 1
 231                                   :do (setf (gethash x ht) num)
 232                                   :finally (return ht))))))
 233        ,@body)))
 234 \f
 235 ;; convenience syntax for logical operations:
 236 (defun standardize  (tree)
 237   "Convert to NOT, AND, OR (preserving :ATOM)"
 238   (cond
 239     ((consp tree)
 240      (destructuring-bind (op . expr)
 241          tree
 242        (case op
 243          ((:IMPLY :IMPLIES)
 244           (if (= 2 (length expr))
 245               `(:OR (:NOT ,(standardize (car expr)))
 246                     ,(standardize (cadr expr)))
 247               (error "barf")))
 248          (:IFF
 249           (if (= 2 (length expr))
 250               `(:AND ,(standardize `(:IMPLIES ,(car expr) ,(cadr expr)))
 251                      ,(standardize `(:IMPLIES ,(cadr expr) ,(car expr))))
 252               (error "barf")))
 253          (T `(,op ,@(standardize expr))))))
 254     (T tree)))
 255
 256 (defun move-nots (tree)
 257   "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree."
 258   (cond
 259     ((consp tree)
 260      (destructuring-bind (op . expr)
 261          tree
 262        (case op
 263          (:NOT (if (= 1 (length expr))
 264                    (let ((subexpr (first expr)))
 265                      (if (consp subexpr)
 266                          (case (first subexpr)
 267                            ;; double-not: drop 2 levels
 268                            (:NOT (move-nots (cdr subexpr)))
 269                            ;; NOT AND:
 270                            (:AND `(:OR ,@(mapcar #'(lambda (c)
 271                                                      (move-nots `(:NOT ,c)))
 272                                                  (cdr subexpr))))
 273                            ;; NOT OR:
 274                            (:OR  `(:AND ,@(mapcar #'(lambda (c)
 275                                                       (move-nots `(:NOT ,c)))
 276                                                   (cdr subexpr))))
 277                            ;; `quoted' atom: keep
 278                            (:ATOM subexpr)
 279                            (otherwise `(:NOT ,subexpr)))
 280                          ;; non-quoted atom:
 281                          `(:NOT ,subexpr)))
 282                    (error "non-unary :NOT expression: ~W" tree)))
 283          ;; other operators: AND, OR, ATOM: descend
 284          (T
 285           `(,op ,@(mapcar #'move-nots expr))))))
 286     ;; non-cons: stop
 287     (T tree)))
 288
 289 (defun crossprod (list-of-lists)
 290   (reduce #'(lambda (collected term)
 291               (loop :for x :in term :appending
 292                  (loop :for tail :in collected
 293                     :collect `(,x ,@tail))))
 294           list-of-lists
 295           :initial-value '(())))
 296
 297 (defun is-cnf (tree)
 298   "Check that TREE is in CNF."
 299   (flet ((and-form (f)
 300            (and (consp f)
 301                 (eq :AND (car f))))
 302          (or-form (f)
 303            (and (consp f)
 304                 (eq :OR (car f))))
 305          (atomic (f)
 306            (if (consp f)
 307                (and (not (eq :OR (car f)))
 308                     (not (eq :AND (car f))))
 309                T)))
 310     (if (atomic tree)
 311         T
 312         (and (and-form tree)
 313              (every #'(lambda (c)
 314                         (or (atomic c)
 315                             (and (or-form c)
 316                                  (every #'atomic (cdr c)))))
 317                     (cdr tree))))))
 318
 319 (defun distribute2 (tree)
 320   (if (consp tree)
 321       (case (car tree)
 322         (:AND (let ((subtrees (mapcar #'distribute2 (cdr tree))))
 323                 (assert (every #'is-cnf subtrees))
 324                 `(:AND ,@(apply #'append subtrees))))
 325         (:OR (let ((subtrees (mapcar #'distribute2 (cdr tree))))
 326                (assert (every #'is-cnf subtree))
 327                `(:AND ))))
 328       .
 329       tree))
 330
 331 (defun distribute (tree)
 332   "Pull out ANDs and unite sequential OR/OR or AND/AND. Input must be in NNF. Returns
 333 CNF of TREE."
 334   (if (consp tree)
 335       (destructuring-bind (op . expr)
 336           tree
 337         (case op
 338           (:OR (let (ands ors others)
 339                  (dolist (term (mapcar #'distribute expr))
 340                    (if (consp term)
 341                        (case (car term)
 342                          (:OR (push term ors))
 343                          (:AND (push term ands))
 344                          (otherwise (push term others)))
 345                        (push term others)))
 346                                         ;                (break "~A ~A ~A" ands ors others)
 347                  (if ands
 348                      (distribute
 349                       (let ((terms (mapcar #'(lambda (or-clause)
 350                                                `(:OR ,@(mapcar #'cdr ors)
 351                                                      ,@others
 352                                                      ,@or-clause))
 353                                            (crossprod (mapcar #'cdr ands)))))
 354                         (break "~A" `(:AND ,@terms))
 355                         `(:AND ,@terms)))
 356                      `(:OR ,@others ,@(mapcar #'cdr ors)))))
 357           (:AND (let ((subexpr '()))
 358                   (dolist (e expr)
 359                     (if (consp e)
 360                         (case (first e)
 361                           (:AND (dolist (f (cdr e))
 362                                   (push (distribute f) subexpr)))
 363                           (:OR  (push (mapcar #'distribute (cdr e)) subexpr))
 364                           (otherwise (push e subexpr)))
 365                         (push e subexpr)))
 366                   `(:AND ,@subexpr)))
 367           (otherwise
 368            ;; :NOT, :ATOM or implicit leaf: keep
 369            tree)))
 370       tree))
 371
 372 (defun tree->cnf (tree)
 373   (labels (
 374
 375            )
 376     (distribute
 377      (move-nots
 378       (standardize tree))))
 379   ;;   (cond
 380   ;;     ((consp tree)
 381   ;;      (destructuring-bind (op . expr)
 382   ;;     tree
 383   ;;        (case op
 384   ;;     ((:IMPLY :IMPILES)
 385   ;;      (if (= 2 (length expr))
 386   ;;          (tree->cnf `(:OR (:NOT ,(car expr)) ,(cadr expr)))
 387   ;;          (error "barf")))
 388   ;;     (:IFF
 389   ;;      (if (= 2 (length expr))
 390   ;;          (tree->cnf `(:AND (:IMPLIES ,(car expr) ,(cadr expr))
 391   ;;                            (:IMPLIES ,(cadr expr) ,(car expr))))
 392   ;;          (error "barf")))
 393   ;;     (:)
 394
 395   ;;     (:AND (mapcar #'tree->cnf expr))
 396   ;;     (:OR  (tree->cnf `(:NOT (:AND (:NOT ,expr)))))
 397   ;;     (:NOT (if (= 1 (length expr))
 398   ;;               ()
 399   ;;             (error)) (mapcar ))))
 400   ;;      )
 401   ;;     ((and lis)))
 402   )
 403
 404 (defun tree->cnf (tree)
 405   (etypecase tree
 406     (number `(,tree))
 407     (cons (case (car tree)
 408             (:AND
 409              ;; flatten:
 410              `(,(apply #'append (mapcar #'tree->cnf (cdr tree)))))
 411             (:NOT
 412              (if (= 2 (length tree))
 413                  (let ((expr (cdr tree)))
 414                    (cond
 415                      ;; we prefer AND by swapping NOT AND to AND NOT
 416                      ((eq :AND (car expr))
 417                       (tree->cnf `(:AND (mapcar #'- (tree->cnf (cdr expr))))))
 418                      ((eq :OR (car expr))
 419                       (tree->cnf `(:AND )))
 420                      ((numberp expr) (- expr))
 421                      (T (error "unsupported"))))
 422                  `(,(mapcar #'(lambda (clause) (mapcar #'- clause))
 423                              (tree->cnf (cadr tree))))
 424                  (error "non-unary :NOT expression: ~A" tree)))
 425
 426
 427
 428             (:OR (tree->cnf `(:NOT (:AND ,(cdr tree)))))
 429             (:XOR
 430              (if (= 3 (length tree))
 431                  (let ((a (cadr tree))
 432                        (b (caddr tree)))
 433                    (tree->cnf `(:AND (:OR ,a ,b)
 434                                      (:OR (:NOT ,a) (:NOT ,b)))))
 435                  (error "non-binary :XOR expression: ~A" tree)))
 436             ((:IMPLIES :IMPLY)
 437              (if (= 3 (length tree))
 438                  (tree->cnf `(:OR (:NOT ,(cadr tree))
 439                                   (caddr tree)))
 440                  (error "non-binary :IMPLIES expression: ~A" tree)))
 441             (:IFF
 442              (if (= 3 (length tree))
 443                  (let ((a (cadr tree))
 444                        (b (caddr tree)))
 445                    (tree->cnf `(:AND (:IMPLIES ,a ,b)
 446                                      (:IMPLIES ,b ,a))))
 447                  (error "non-binary :IFF expression: ~A" tree)))
 448             (otherwise
 449              (error "unsupported expression: ~A" tree))))
 450     (T (error "Formula contains unsupported expression: ~A" tree))))
 451
 452 (defmacro build-cnf (tree)
 453   `(tree->cnf ',tree))
 454
 455 (defun make-and-cnf (literals)
 456   (mapcar #'list literals))
 457 (defun make-or-cnf (literals)
 458   literals)
 459 (defun negate-cnf (list-of-clauses)
 460   (mapcar #'(lambda (c) (mapcar #'- c)) list-of-clauses))
 461 (defun make-xor-cnf (a b)
 462   (make-or-cnf)`(,a ,(- b))
 463   literals)
 464
 465 (defgeneric add-and (solver literals)
 466   (:documentation "Add clauses for AND(literals) to SOLVER."))
 467 (defgeneric add-or (solver literals)
 468   (:documentation "Add clauses for OR(literals) to SOLVER."))
 469 (defgeneric add-xor (solver literals)
 470   (:documentation "Add clauses for XOR(literals) to SOLVER."))
 471 (defgeneric add-if (solver lhs rhs)
 472   (:documentation "Add clauses for lhs -> rhs to SOLVER."))
 473 (defgeneric add-iff (solver lhs rhs)
 474   (:documentation "Add clauses for lhs <-> rhs to SOLVER."))