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
  31
  32 (in-package #:satwrap)
  33 \f
  34
  35 ;;; Frontend:
  36 (defclass sat-solver ()
  37   ((backend :initarg :backend :accessor sat-solver-backend)
  38    (numvars :initform 0 :accessor sat-solver-numvars)
  39    (clauses :initform '() :accessor sat-solver-clauses) ;; CNF
  40    )
  41   (:default-initargs :backend (make-instance (cdr (assoc *default-sat-backend*
  42                                                          *satwrap-backends*))))
  43   (:documentation "A Sat solver abstraction"))
  44
  45 (defmethod sat-solver-numclauses ((solver sat-solver))
  46   (length (sat-solver-clauses solver)))
  47
  48 (defmethod print-object ((solver sat-solver) stream)
  49   (print-unreadable-object (solver stream :type T :identity T)
  50     (format stream "~D vars, ~D clauses, backend ~A"
  51             (sat-solver-numvars solver)
  52             (sat-solver-numclauses solver)
  53             (sat-solver-backend solver))))
  54
  55 (defmethod clause-valid ((solver sat-solver) (clause list))
  56   "Check that CLAUSE is a valid clause for SOLVER."
  57   (loop
  58      :with max := (sat-solver-numvars solver)
  59      :with min := (- max)
  60      :for v :in clause
  61      :always (and (not (zerop v))
  62                   (<= min v max))))
  63
  64 (defmacro iota (n &optional (start 1))
  65   "Return a list of the N sequential integers starting at START (default: 1)."
  66   (let ((i (gensym "i")))
  67     `(loop :repeat ,n
  68         :for ,i :from ,start
  69         :collect ,i)))
  70
  71 (define-condition satwrap-condition (error)
  72   ()
  73   (:documentation "Superclass of all conditions raised by satwrap code."))
  74
  75 (define-condition invalid-clause (satwrap-condition)
  76   ((solver :initarg :solver :reader invalid-clause-solver)
  77    (clause :initarg :clause :reader invalid-clause-clause))
  78   (:report (lambda (condition stream)
  79              (format stream "Invalid clause ~A for solver ~A"
  80                      (invalid-clause-clause condition)
  81                      (invalid-clause-solver condition)))))
  82
  83 (define-condition invalid-backend (satwrap-condition)
  84   ((name :initarg :name :reader invalid-backend-name))
  85   (:report (lambda (condition stream)
  86              (declare (special *satwrap-backends* *default-sat-backend*))
  87              (format stream "Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
  88                      (invalid-backend-name condition)
  89                      (mapcar #'car *satwrap-backends*)
  90                      *default-sat-backend*))))
  91
  92 (defmethod flush-to-backend ((solver sat-solver))
  93   "Populate backend, possibly flushing old backend contents."
  94   (reinitialize-instance (sat-solver-backend solver))
  95   ;; declare proper number of variables
  96   (setf (satwrap.backend:numvars (sat-solver-backend solver))
  97         (sat-solver-numvars solver))
  98   (dolist (c (sat-solver-clauses solver))
  99     (satwrap.backend:add-clause (sat-solver-backend solver) c)))
 100
 101 \f
 102 (defvar *default-sat-backend* :precosat
 103   "Name of the default backend to be used by make-sat-solver.")
 104
 105 (defparameter *satwrap-backends*
 106   `((:precosat . ,(find-class 'satwrap.precosat:precosat-backend)))
 107   "Alist of symbolic name to backend class name for all supported backends.")
 108
 109 (defun make-sat-solver (&optional (backend *default-sat-backend*))
 110   "Return a new sat solver instance. Optional argument BACKEND can be used to
 111 specify which backend should be used. It defaults to *default-sat-backend*."
 112   (let ((be (assoc backend *satwrap-backends*)))
 113     (if be
 114         (make-instance 'sat-solver :backend (make-instance (cdr be)))
 115         (error 'invalid-backend :name backend))))
 116
 117 (defgeneric add-variable (solver)
 118   (:documentation "Add another variable to SOLVER. Returns new variable index.")
 119   (:method ((solver sat-solver))
 120     (incf (sat-solver-numvars solver))))
 121
 122 (defgeneric add-clause (solver clause)
 123   (:documentation "Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
 124   (:method ((solver sat-solver) (clause list))
 125     (if (clause-valid solver clause)
 126         (push clause (sat-solver-clauses solver))
 127         (error 'invalid-clause :clause clause :solver solver)))
 128   (:method ((solver sat-solver) (clause vector))
 129     (add-clause solver (coerce clause 'list))))
 130
 131 (defgeneric satisfiablep (solver &key assume)
 132   (:documentation "Check whether current CNF in SOLVER is satisfiable.
 133 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
 134 Returns T or NIL.")
 135   (:method ((solver sat-solver) &key (assume '()))
 136     (if (clause-valid solver assume) ;; misusing 'clause' concept here
 137         (progn
 138           (flush-to-backend solver)
 139           (satwrap.backend:satisfiablep (sat-solver-backend solver) assume))
 140         (error 'invalid-clause :clause assume :solver solver))))
 141
 142 (defgeneric solution (solver &key interesting-vars)
 143   (:documentation "Return solution for SOLVER. If unsat, return '(). If sat return
 144 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.")
 145   (:method ((solver sat-solver)
 146             &key (interesting-vars (iota (sat-solver-numvars solver))))
 147     (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
 148
 149