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* :precosat
  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   "Alist of symbolic name to backend class name for all supported backends.")
  42
  43 \f
  44 ;;; Frontend:
  45 (defclass sat-solver ()
  46   ((backend :initarg :backend :accessor sat-solver-backend)
  47    (numvars :initform 0 :accessor sat-solver-numvars)
  48    (clauses :initform '() :accessor sat-solver-clauses) ;; CNF
  49    )
  50   (:default-initargs :backend (make-instance (cdr (assoc *default-sat-backend*
  51                                                          *satwrap-backends*))))
  52   (:documentation "A Sat solver abstraction"))
  53
  54 (defmethod sat-solver-numclauses ((solver sat-solver))
  55   (length (sat-solver-clauses solver)))
  56
  57 (defmethod print-object ((solver sat-solver) stream)
  58   (print-unreadable-object (solver stream :type T :identity T)
  59     (format stream "~D vars, ~D clauses, backend ~A"
  60             (sat-solver-numvars solver)
  61             (sat-solver-numclauses solver)
  62             (sat-solver-backend solver))))
  63
  64 (defmethod clause-valid ((solver sat-solver) (clause list))
  65   "Check that CLAUSE is a valid clause for SOLVER."
  66   (loop
  67      :with max := (sat-solver-numvars solver)
  68      :with min := (- max)
  69      :for v :in clause
  70      :always (and (not (zerop v))
  71                   (<= min v max))))
  72
  73 (defmacro iota (n &optional (start 1))
  74   "Return a list of the N sequential integers starting at START (default: 1)."
  75   (let ((i (gensym "i")))
  76     `(loop :repeat ,n
  77         :for ,i :from ,start
  78         :collect ,i)))
  79
  80 (define-condition satwrap-condition (error)
  81   ()
  82   (:documentation "Superclass of all conditions raised by satwrap code."))
  83
  84 (define-condition invalid-clause (satwrap-condition)
  85   ((solver :initarg :solver :reader invalid-clause-solver)
  86    (clause :initarg :clause :reader invalid-clause-clause))
  87   (:report (lambda (condition stream)
  88              (format stream "Invalid clause ~A for solver ~A"
  89                      (invalid-clause-clause condition)
  90                      (invalid-clause-solver condition)))))
  91
  92 (define-condition invalid-backend (satwrap-condition)
  93   ((name :initarg :name :reader invalid-backend-name))
  94   (:report (lambda (condition stream)
  95              (declare (special *satwrap-backends* *default-sat-backend*))
  96              (format stream "Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
  97                      (invalid-backend-name condition)
  98                      (mapcar #'car *satwrap-backends*)
  99                      *default-sat-backend*))))
 100
 101 (defmethod flush-to-backend ((solver sat-solver))
 102   "Populate backend, possibly flushing old backend contents."
 103   (reinitialize-instance (sat-solver-backend solver))
 104   ;; declare proper number of variables
 105   (setf (satwrap.backend:numvars (sat-solver-backend solver))
 106         (sat-solver-numvars solver))
 107   (dolist (c (sat-solver-clauses solver))
 108     (satwrap.backend:add-clause (sat-solver-backend solver) c)))
 109
 110 \f
 111 (defun make-sat-solver (&optional (backend *default-sat-backend*))
 112   "Return a new sat solver instance. Optional argument BACKEND can be used to
 113 specify which backend should be used. It defaults to *default-sat-backend*."
 114   (let ((be (assoc backend *satwrap-backends* :test #'eq)))
 115     (if be
 116         (make-instance 'sat-solver :backend (make-instance (cdr be)))
 117         (error 'invalid-backend :name backend))))
 118
 119 (defgeneric add-variable (solver)
 120   (:documentation "Add another variable to SOLVER. Returns new variable index.")
 121   (:method ((solver sat-solver))
 122     (incf (sat-solver-numvars solver))))
 123
 124 (defgeneric add-clause (solver clause)
 125   (:documentation "Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
 126   (:method ((solver sat-solver) (clause list))
 127     (if (clause-valid solver clause)
 128         (push clause (sat-solver-clauses solver))
 129         (error 'invalid-clause :clause clause :solver solver)))
 130   (:method ((solver sat-solver) (clause vector))
 131     (add-clause solver (coerce clause 'list))))
 132
 133 (defgeneric satisfiablep (solver &key assume)
 134   (:documentation "Check whether current CNF in SOLVER is satisfiable.
 135 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
 136 Returns T or NIL.")
 137   (:method ((solver sat-solver) &key (assume '()))
 138     (if (clause-valid solver assume) ;; misusing 'clause' concept here
 139         (progn
 140           (flush-to-backend solver)
 141           (satwrap.backend:satisfiablep (sat-solver-backend solver) assume))
 142         (error 'invalid-clause :clause assume :solver solver))))
 143
 144 (defgeneric solution (solver &key interesting-vars)
 145   (:documentation "Return solution for SOLVER. If unsat, return '(). If sat return
 146 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.")
 147   (:method ((solver sat-solver)
 148             &key (interesting-vars (iota (sat-solver-numvars solver))))
 149     (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
 150
 151 (defgeneric get-essential-variables (solver)
 152   (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
 153 Returns a list of literals fixed, sign according to phase.")
 154   (:method ((solver sat-solver))
 155     ;; The backend may define a specialized method, but then it has to
 156     ;; work on the one copy of data flushed to the solver. Precosat for example
 157     ;; does not allow that, so we define the universal implementation here instead of
 158     ;; a default implementation in the backend.
 159     (let ((have-specialized-method
 160            (find-method #'satwrap.backend:get-essential-variables
 161                         '()
 162                         `(,(class-of (sat-solver-backend solver)))
 163                         nil)))
 164       (if have-specialized-method
 165           (progn
 166             (flush-to-backend solver)
 167             (satwrap.backend:get-essential-variables (sat-solver-backend solver)))
 168           (let ((fixed '()))
 169             (loop :for var :of-type (integer 1) :in (iota (sat-solver-numvars solver))
 170                :as res-for-+ := (satisfiablep solver :assume `(,var ,@fixed))
 171                :as res-for-- := (satisfiablep solver :assume `(,(- var) ,@fixed))
 172                :do (cond
 173                      ((and res-for-+ (not res-for--))
 174                       (push var fixed))
 175                      ((and (not res-for-+) res-for--)
 176                       (push (- var) fixed))))
 177             fixed)))))
 178
 179 \f
 180 (defmacro with-sat-solver ((name numatoms &key (backend *default-sat-backend*))
 181                            &body body)
 182   "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."
 183   `(let ((,name (make-sat-solver ,backend)))
 184      (loop :repeat ,numatoms :do (add-variable ,name))
 185      (locally
 186          ,@body)))
 187
 188 (defmacro with-index-hash ((mapping &key (test 'cl:eq)) objects &body body)
 189   "Execute BODY while binding MAPPING to a hash-table (with predicate
 190 TEST, defaults to #'cl:eq) mapping the elements of the sequence OBJECTS
 191 to integer 1..[length objects].
 192 Typically used to map objects to variables inside WITH-SAT-SOLVER."
 193   (let ((o (gensym "objects")))
 194     `(let* ((,o ,objects)
 195             (,mapping (etypecase ,o
 196                        (list (loop :with ht := (make-hash-table :test ,test)
 197                                 :for x :in ,o
 198                                 :for num :of-type fixnum :from 1
 199                                 :do (setf (gethash x ht) num)
 200                                 :finally (return ht)))
 201                        (vector (loop :with ht := (make-hash-table :test ,test)
 202                                   :for x :across ,o
 203                                   :for num :of-type fixnum :from 1
 204                                   :do (setf (gethash x ht) num)
 205                                   :finally (return ht))))))
 206        ,@body)))