dimacs.lisp

   1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
   2 ;;;
   3 ;;; dimacs.lisp --- DIMACS read/write procedures
   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 (in-package #:satwrap)
  34 \f
  35 (defun split-delimited-string (string char)
  36   "Return a list of the substrings of STRING that are separated by CHAR. Without CHAR."
  37   (declare (type string string)
  38            (type character char))
  39   (let ((next-separator (position char string :test #'char=)))
  40     (if next-separator
  41         (cons (subseq string 0 next-separator)
  42               (split-delimited-string (subseq string (1+ next-separator))
  43                                       char))
  44         `(,string))))
  45
  46 (defgeneric read-dimacs (solver source)
  47   (:documentation "Read DIMACS-style sat problem from SOURCE into SOLVER.")
  48   (:method ((solver sat-solver) (source pathname))
  49     (with-open-file (f source :direction :input)
  50       (loop :as line := (read-line f nil nil nil)
  51          :as pieces := (and line
  52                             (split-delimited-string line #\Space))
  53          :while line
  54          :when (string= "p" (first pieces))
  55          ;; format specification:
  56          :do (destructuring-bind (p format m n)
  57                  pieces
  58                (declare (ignore p))
  59                (unless (string= "cnf" format)
  60                  (error "Dimacs file not in CNF format: ~A" line))
  61                (setf (sat-solver-numvars solver) (parse-integer m))
  62                (loop
  63                   :with clause := '()
  64                   :as var := (read f nil nil nil)
  65                   :while var
  66                   :if (= 0 var)
  67                   :do (progn
  68                         (add-clause solver (nreverse clause))
  69                         (setf clause '()))
  70                   :else
  71                   :collect (push var clause))
  72                (unless (= (parse-integer n) (sat-solver-numclauses solver))
  73                  (error "Dimacs file ends prematurely: parsed ~D clauses, expected ~A"
  74                         (sat-solver-numclauses solver)
  75                         n)))))
  76     (setf (sat-solver-new-clauses solver) (nreverse (sat-solver-new-clauses solver)))
  77     solver))
  78
  79 (defgeneric write-dimacs (solver dst &key comments)
  80   (:documentation "Write DIMACS-STYLE sat problem of SOLVER to DST.")
  81   (:method ((solver sat-solver) (dst pathname) &key (comments "Generated by cl-satwrap"))
  82     (with-open-file (f dst :direction :output :if-exists :supersede)
  83       ;; See CLHS 22.3.3. example:
  84       (format f "~&c ~{~<~%c ~1:;~A~>~^ ~}~%" (split-delimited-string comments #\Space))
  85       (format f "~&p cnf ~D ~D~%"
  86               (sat-solver-numvars solver)
  87               (sat-solver-numclauses solver))
  88       (format f "~{~&~{~D~^ ~} 0~%~}" (sat-solver-old-clauses solver))
  89       (format f "~{~&~{~D~^ ~} 0~%~}" (sat-solver-new-clauses solver)))))
  90
  91 (defun make-sat-solver-for-dimacs-instance (source)
  92   (read-dimacs (make-instance 'sat-solver) source))