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