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