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
32 (in-package #:satwrap
)
34 (defun split-delimited-string (string char
)
35 "Return a list of the substrings of STRING that are separated by CHAR. Without CHAR."
36 (declare (type string string
)
37 (type character char
))
38 (let ((next-separator (position char string
:test
#'char
=)))
40 (cons (subseq string
0 next-separator
)
41 (split-delimited-string (subseq string
(1+ next-separator
))
45 (defgeneric read-dimacs
(solver source
)
46 (:documentation
"Read DIMACS-style sat problem from SOURCE into SOLVER.")
47 (:method
((solver sat-solver
) (source pathname
))
48 (with-open-file (f source
:direction
:input
)
49 (loop :as line
:= (read-line f nil nil nil
)
50 :as pieces
:= (split-delimited-string line
#\Space
)
52 :when
(string= "p" (first pieces
))
53 ;; format specification:
54 :do
(destructuring-bind (p format m n
)
57 (unless (string= "cnf" format
)
58 (error "Dimacs file not in CNF format: ~A" line
))
59 (setf (sat-solver-numvars solver
) (parse-integer m
))
62 :as var
:= (read f nil nil nil
)
66 (add-clause solver
(nreverse clause
))
69 :collect
(push var clause
))
70 (unless (= (parse-integer n
) (sat-solver-numclauses solver
))
71 (error "Dimacs file ends prematurely: parsed ~D clauses, expected ~A"
72 (sat-solver-numclauses solver
)
74 (setf (sat-solver-clauses solver
) (nreverse (sat-solver-clauses solver
)))
77 (defun make-sat-solver-for-dimacs-instance (source)
78 (read-dimacs (make-instance 'sat-solver
) source
))