1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
3 ;;; dimacs.lisp --- DIMACS read/write procedures
5 ;; Copyright (C) 2010 Utz-Uwe Haus <lisp@uuhaus.de>
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.
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.
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
30 (eval-when (:compile-toplevel
:load-toplevel
)
31 (declaim (optimize (speed 3) (debug 1) (safety 1))))
33 (in-package #:satwrap
)
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
=)))
41 (cons (subseq string
0 next-separator
)
42 (split-delimited-string (subseq string
(1+ next-separator
))
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
))
54 :when
(string= "p" (first pieces
))
55 ;; format specification:
56 :do
(destructuring-bind (p format m n
)
59 (unless (string= "cnf" format
)
60 (error "Dimacs file not in CNF format: ~A" line
))
61 (setf (sat-solver-numvars solver
) (parse-integer m
))
64 :as var
:= (read f nil nil nil
)
68 (add-clause solver
(nreverse clause
))
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
)
76 (setf (sat-solver-new-clauses solver
) (nreverse (sat-solver-new-clauses solver
)))
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
)))))
91 (defun make-sat-solver-for-dimacs-instance (source)
92 (read-dimacs (make-instance 'sat-solver
) source
))