Fix macro expansion time confusion in with-index-hash
[cl-satwrap.git] / satwrap.lisp
blobbc8649508e7841393019d7a46cead8550cb08d55
1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
2 ;;;
3 ;;; satwrap.lisp --- SAT solvers wrapped for CL
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.
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
24 ;; Commentary:
26 ;;
28 ;;; Code:
30 (eval-when (:compile-toplevel :load-toplevel)
31 (declaim (optimize (speed 3) (debug 1) (safety 1))))
34 (in-package #:satwrap)
36 (defvar *default-sat-backend* :minisat
37 "Name of the default backend to be used by make-sat-solver.")
39 (defparameter *satwrap-backends*
40 `((:precosat . ,(find-class 'satwrap.precosat:precosat-backend))
41 (:minisat . ,(find-class 'satwrap.minisat:minisat-backend)))
42 "Alist of symbolic name to backend class name for all supported backends.")
44 (defun describe-supported-backends ()
45 "Return a list of (designator . description) pairs of the supported backends"
46 (loop :for (key . class) :in *satwrap-backends*
47 :as descr := (let ((instance (make-instance class)))
48 (format nil "~A version ~A"
49 (satwrap.backend:sat-backend-name instance)
50 (satwrap.backend:sat-backend-version instance)))
51 :collect `(,key . ,descr)))
54 ;;; Frontend:
55 (defclass sat-solver ()
56 ((backend :initarg :backend :accessor sat-solver-backend)
57 (numvars :initform 0 :accessor sat-solver-numvars)
58 ;; CNF; split into 'old' and 'new' to allow incremental solving
59 (new-clauses :initform '() :accessor sat-solver-new-clauses)
60 (old-clauses :initform '() :accessor sat-solver-old-clauses)
62 (:default-initargs :backend (make-instance (cdr (assoc *default-sat-backend*
63 *satwrap-backends*))))
64 (:documentation "A Sat solver abstraction"))
66 (defmethod sat-solver-numclauses ((solver sat-solver))
67 (+ (length (sat-solver-new-clauses solver))
68 (length (sat-solver-old-clauses solver))
71 (defmethod print-object ((solver sat-solver) stream)
72 (print-unreadable-object (solver stream :type T :identity T)
73 (format stream "~D vars, ~D clauses, backend ~A"
74 (sat-solver-numvars solver)
75 (sat-solver-numclauses solver)
76 (sat-solver-backend solver))))
78 (defmethod clause-valid ((solver sat-solver) (clause list))
79 "Check that CLAUSE is a valid clause for SOLVER."
80 (loop
81 :with max := (sat-solver-numvars solver)
82 :with min := (- max)
83 :for v :in clause
84 :always (and (not (zerop v))
85 (<= min v max))))
87 (defmacro iota (n &optional (start 1))
88 "Return a list of the N sequential integers starting at START (default: 1)."
89 (let ((i (gensym "i")))
90 `(loop :repeat ,n
91 :for ,i :from ,start
92 :collect ,i)))
94 (define-condition satwrap-condition (error)
96 (:documentation "Superclass of all conditions raised by satwrap code."))
98 (define-condition invalid-clause (satwrap-condition)
99 ((solver :initarg :solver :reader invalid-clause-solver)
100 (clause :initarg :clause :reader invalid-clause-clause))
101 (:report (lambda (condition stream)
102 (format stream "Invalid clause ~A for solver ~A"
103 (invalid-clause-clause condition)
104 (invalid-clause-solver condition)))))
106 (define-condition invalid-backend (satwrap-condition)
107 ((name :initarg :name :reader invalid-backend-name))
108 (:report (lambda (condition stream)
109 (declare (special *satwrap-backends* *default-sat-backend*))
110 (format stream "Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
111 (invalid-backend-name condition)
112 (mapcar #'car *satwrap-backends*)
113 *default-sat-backend*))))
115 (defmethod flush-to-backend ((solver sat-solver))
116 "Populate backend, possibly flushing old backend contents."
117 (satwrap.backend:synchronize-backend (sat-solver-backend solver)
118 (sat-solver-numvars solver)
119 (sat-solver-new-clauses solver)
120 '() ;; deleted clauses, not yet supported
121 (sat-solver-old-clauses solver))
122 (loop :with deleted := '()
123 :for c :in (sat-solver-old-clauses solver)
124 :unless (find c deleted :test #'equal)
125 :do (push c (sat-solver-new-clauses solver)))
126 (setf (sat-solver-old-clauses solver) (sat-solver-new-clauses solver)
127 (sat-solver-new-clauses solver) '()))
130 (defun make-sat-solver (&optional (backend *default-sat-backend*))
131 "Return a new sat solver instance. Optional argument BACKEND can be used to
132 specify which backend should be used. It defaults to *default-sat-backend*."
133 (let ((be (assoc backend *satwrap-backends* :test #'eq)))
134 (if be
135 (make-instance 'sat-solver :backend (make-instance (cdr be)))
136 (error 'invalid-backend :name backend))))
138 (defgeneric add-variable (solver)
139 (:documentation "Add another variable to SOLVER. Returns new variable index.")
140 (:method ((solver sat-solver))
141 (incf (sat-solver-numvars solver))))
143 (defgeneric add-clause (solver clause)
144 (:documentation "Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
145 (:method ((solver sat-solver) (clause list))
146 (if (clause-valid solver clause)
147 (push clause (sat-solver-new-clauses solver))
148 (error 'invalid-clause :clause clause :solver solver)))
149 (:method ((solver sat-solver) (clause vector))
150 (add-clause solver (coerce clause 'list))))
152 (defgeneric add-clauses (solver clauses)
153 (:documentation "Add CLAUSES to SOLVER's cnf formula. Clauses are consumed.")
154 (:method ((solver sat-solver) (clauses list))
155 (dolist (c clauses)
156 (add-clause solver c))))
158 (defgeneric satisfiablep (solver &key assume)
159 (:documentation "Check whether current CNF in SOLVER is satisfiable.
160 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
161 Returns T or NIL.")
162 (:method ((solver sat-solver) &key (assume '()))
163 (if (clause-valid solver assume) ;; misusing 'clause' concept here
164 (progn
165 (flush-to-backend solver)
166 (satwrap.backend:satisfiablep (sat-solver-backend solver) assume))
167 (error 'invalid-clause :clause assume :solver solver))))
169 (defgeneric solution (solver &key interesting-vars)
170 (:documentation "Return solution for SOLVER. If unsat, return '(). If sat return
171 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.")
172 (:method ((solver sat-solver)
173 &key (interesting-vars (iota (sat-solver-numvars solver))))
174 (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
176 (defgeneric get-essential-variables (solver)
177 (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
178 Returns a list of literals fixed, sign according to phase.")
179 (:method ((solver sat-solver))
180 ;; The backend may define a specialized method, but then it has to
181 ;; work on the one copy of data flushed to the solver. Precosat for example
182 ;; does not allow that, so we define the universal implementation here instead of
183 ;; a default implementation in the backend.
184 (let ((have-specialized-method
185 (find-method #'satwrap.backend:get-essential-variables
187 `(,(class-of (sat-solver-backend solver)))
188 nil)))
189 (if have-specialized-method
190 (progn
191 (flush-to-backend solver)
192 (satwrap.backend:get-essential-variables (sat-solver-backend solver)))
193 (let ((fixed '()))
194 (loop :for var :of-type (integer 1) :in (iota (sat-solver-numvars solver))
195 :as sat-for-+ := (satisfiablep solver :assume `(,var ,@fixed ))
196 :as sat-for-- := (satisfiablep solver :assume `(,(- var) ,@fixed))
197 :do (cond
198 ((and sat-for-+ (not sat-for--))
199 (push var fixed))
200 ((and (not sat-for-+) sat-for--)
201 (push (- var) fixed))))
202 fixed)))))
205 (defmacro with-sat-solver ((name numatoms &key (backend *default-sat-backend* backend-given))
206 &body body)
207 "Bind NAME to a fresh sat-solver with backend :BACKEND (default: *default-sat-backend*) and declare NUMATOMS variables numbered 1..NUMATOMS for the duration of BODY."
208 `(let ((,name (make-sat-solver ,(if backend-given
209 backend
210 '*default-sat-backend*))))
211 (loop :repeat ,numatoms :do (add-variable ,name))
212 (locally
213 ,@body)))
215 (defmacro with-index-hash ((mapping &key (test 'eq)) objects &body body)
216 "Execute BODY while binding MAPPING to a hash-table (with predicate
217 TEST, defaults to #'cl:eq) mapping the elements of the sequence OBJECTS
218 to integer 1..[length objects].
219 Typically used to map objects to variables inside WITH-SAT-SOLVER."
220 (let ((o (gensym "objects")))
221 `(let* ((,o ,objects)
222 (,mapping (etypecase ,o
223 (list (loop :with ht := (make-hash-table :test #',test)
224 :for x :in ,o
225 :for num :of-type fixnum :from 1
226 :do (setf (gethash x ht) num)
227 :finally (return ht)))
228 (vector (loop :with ht := (make-hash-table :test #',test)
229 :for x :across ,o
230 :for num :of-type fixnum :from 1
231 :do (setf (gethash x ht) num)
232 :finally (return ht))))))
233 ,@body)))
235 ;; convenience syntax for logical operations:
236 (defun standardize (tree)
237 "Convert tree of logical operations to elementary :NOT, :AND, :OR tree (preserving :ATOM).
238 Supports :IMPLY, :IFF, binary :XOR, and :NOR. "
239 (cond
240 ((consp tree)
241 (destructuring-bind (op . expr)
242 tree
243 (case op
244 ((:IMPLY :IMPLIES)
245 (if (= 2 (length expr))
246 `(:OR (:NOT ,(standardize (car expr)))
247 ,(standardize (cadr expr)))
248 (error "non-binary :IMPLY operation: ~A" tree)))
249 (:IFF
250 (if (= 2 (length expr))
251 `(:AND ,(standardize `(:IMPLIES ,(car expr) ,(cadr expr)))
252 ,(standardize `(:IMPLIES ,(cadr expr) ,(car expr))))
253 (error "non-binary :IFF operation: ~A" tree)))
254 (:XOR
255 (if (= 2 (length expr))
256 (let ((e1 (standardize (first expr)))
257 (e2 (standardize (second expr))))
258 `(:OR (:AND ,e1 (:NOT ,e2))
259 (:AND ,e2 (:NOT ,e1))))
260 (error "non-binary :XOR operation: ~A" tree)))
261 (:NOR
262 `(:AND ,@(mapcar #'(lambda (p) `(:NOT ,(standardize p))) expr)))
264 (T `(,op ,@(mapcar #'standardize expr))))))
265 (T tree)))
267 (defun standard-tree->nnf (tree)
268 "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree."
269 (cond
270 ((consp tree)
271 (destructuring-bind (op . expr)
272 tree
273 (case op
274 (:NOT (if (= 1 (length expr))
275 (let ((subexpr (first expr)))
276 (if (consp subexpr)
277 (case (first subexpr)
278 ;; double-not: drop 2 levels
279 (:NOT (standard-tree->nnf (cadr subexpr)))
280 ;; NOT AND:
281 (:AND `(:OR ,@(mapcar #'(lambda (c)
282 (standard-tree->nnf `(:NOT ,c)))
283 (cdr subexpr))))
284 ;; NOT OR:
285 (:OR `(:AND ,@(mapcar #'(lambda (c)
286 (standard-tree->nnf `(:NOT ,c)))
287 (cdr subexpr))))
288 ;; `quoted' atom: keep
289 (:ATOM subexpr)
290 (otherwise `(:NOT ,subexpr)))
291 ;; non-quoted atom:
292 `(:NOT ,subexpr)))
293 (error "non-unary :NOT expression: ~W" tree)))
294 ;; other operators: AND, OR, ATOM: descend
296 `(,op ,@(mapcar #'standard-tree->nnf expr))))))
297 ;; non-cons: stop
298 (T tree)))
300 (defun crossprod (list-of-lists)
301 "Return a list of all lists containing one element from each sublist of LIST-OF-LISTS."
302 (reduce #'(lambda (collected term)
303 (loop :for x :in term :appending
304 (loop :for tail :in collected
305 :collect `(,x ,@tail))))
306 list-of-lists
307 :initial-value '(())))
309 (defun is-cnf (tree)
310 "Check that TREE is in CNF."
311 (flet ((and-form (f)
312 (and (consp f)
313 (eq :AND (car f))))
314 (or-form (f)
315 (and (consp f)
316 (eq :OR (car f))))
317 (atomic (f)
318 (if (consp f)
319 (and (not (eq :OR (car f)))
320 (not (eq :AND (car f))))
321 T)))
322 (if (atomic tree)
324 (and (and-form tree)
325 (every #'(lambda (c)
326 (or (atomic c)
327 (and (or-form c)
328 (every #'atomic (cdr c)))))
329 (cdr tree))))))
331 (defun distribute (tree)
332 "Pull out :ANDs to reduce standardized tree in NNF to CNF."
333 (if (consp tree)
334 (case (car tree)
335 (:AND (let ((sub-cnfs (mapcar #'distribute (cdr tree))))
336 (assert (every #'is-cnf sub-cnfs)
337 (sub-cnfs)
338 "Not all in CNF: ~{~A~^~%~}" sub-cnfs)
339 (let (clauses)
340 (loop :for sub-cnf :in sub-cnfs
341 :if (and (consp sub-cnf)
342 (eq :AND (car sub-cnf)))
343 ;; AND(AND ..) = AND ..
344 :do (dolist (clause (cdr sub-cnf))
345 (push clause clauses))
346 :else :do (push sub-cnf clauses))
347 `(:AND ,@clauses))))
348 (:OR (let (ands)
349 (dolist (term (mapcar #'distribute (cdr tree)))
350 (assert (is-cnf term)
351 (term)
352 "~A not in CNF" term)
353 (if (consp term)
354 (case (car term)
355 (:AND (push (cdr term) ands))
356 (:OR (dolist (c (cdr term))
357 (push `(,c) ands)))
358 (otherwise (push `(,term) ands)))
359 (push `(,term) ands)))
360 (let ((clauses (crossprod ands)))
361 `(:AND ,@(mapcar #'(lambda (c)
362 (if (not (consp c))
364 `(:OR ,@ (loop :for subterm :in c
365 :if (and (consp subterm)
366 (eq :OR (car subterm)))
367 ;; (OR(OR...)) == (OR ...)
368 :append (cdr subterm)
369 ;; if C is not an OR-clause
370 ;; it is considered atomic:
371 :else :append `(,subterm)))))
372 clauses)))))
373 (otherwise
374 tree))
375 tree))
378 (defun tree->cnf (tree &optional (mapping #'cl:identity) (atom-test #'eql))
379 "Convert TREE to CNF, applying MAPPING to atoms and afterwards and removing duplicate literals in clauses using atom-test to test for equality. Also simplifies trivially fulfilled clauses to empty clause."
380 (labels ((atomic (f)
381 (if (consp f)
382 (and (not (eq :OR (car f)))
383 (not (eq :AND (car f))))
385 (map-literals (cnf)
386 ;; destructively apply MAPPING
387 (if (atomic cnf)
388 (setf cnf (funcall mapping cnf))
389 (setf (cdr cnf) ;; we must be looking at an AND
390 (mapcar #'(lambda (clause)
391 (if (atomic clause)
392 (funcall mapping clause)
393 `(:OR ,@(mapcar #'(lambda (lit)
394 (funcall mapping lit))
395 (cdr clause)))))
396 (cdr cnf))))
397 cnf)
398 (negated-litp (lit)
399 (and (consp lit) (eq :NOT (car lit))))
400 (atom-for (lit)
401 (if (consp lit)
402 (case (car lit)
403 (:NOT (atom-for (second lit)))
404 (:ATOM (second lit))
405 (otherwise lit))
406 lit))
407 (duplicate-literalsp (l1 l2)
408 (funcall atom-test (atom-for l1) (atom-for l2)))
409 (trivial-clausep (c)
410 (loop :for (lit . haystack) :on c
411 :as needle := (atom-for lit)
412 :as negated := (and (consp lit) (eq :NOT (car lit)))
413 :when (find-if #'(lambda (x)
414 (and (if negated
415 (not (negated-litp x))
416 (negated-litp x))
417 (funcall atom-test needle (atom-for x))))
418 haystack)
419 :return T
420 :finally (return NIL)))
421 (clean-clauses (cnf)
422 ;; destructively apply MAPPING
423 (if (atomic cnf)
424 (setf cnf (funcall mapping cnf))
425 (setf (cdr cnf) ;; we must be looking at an AND
426 (loop :for clause :in (cdr cnf)
427 :if (atomic clause)
428 :collect (funcall mapping clause)
429 :else :if (not (trivial-clausep clause))
430 :collect `(:OR ,@(remove-duplicates
431 (cdr clause)
432 :test #'duplicate-literalsp)))))
433 cnf))
434 (clean-clauses
435 (map-literals
436 (distribute
437 (standard-tree->nnf
438 (standardize tree)))))))
441 (defgeneric add-formula (solver formula &key mapping atom-test)
442 (:documentation "Add logical FORMULA to SOLVER.
443 Formula is an expression tree that can contain high-level abbreviations :IMPLY, :IFF, :NOR and :XOR, as well as the basic :AND, :OR, :NOT. Everything else is considered an atom. Atoms can also be explicitly written as (:ATOM foo).
444 All atoms will be mapped through MAPPING before being added to the solver to convert your favorite atoms to phased variables. MAPPING is a function of 1 argument, the atom. It defaults to #'identity. Afterwards, clean clauses (removing duplicates and simplifying trivial clauses, comparing atoms using ATOM-TEST (default: #'eql).")
445 (:method ((solver sat-solver) (formula list) &key (mapping #'identity) (atom-test #'eql))
446 (add-clauses solver (tree->cnf formula mapping atom-test))))
448 (defgeneric add-and (solver literals &key mapping)
449 (:documentation "Add clauses for AND(literals) to SOLVER.")
450 (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
451 (add-formula solver `(:AND ,@literals) mapping)))
453 (defgeneric add-or (solver literals &key mapping)
454 (:documentation "Add clauses for OR(literals) to SOLVER.")
455 (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
456 (add-formula solver `(:OR ,@literals) mapping)))
458 (defgeneric add-xor (solver literals &key mapping)
459 (:documentation "Add clauses for binary XOR(literals) to SOLVER.")
460 (:method ((solver sat-solver) (literals list) &key (mapping #'identity))
461 (add-formula solver `(:XOR ,@literals) mapping)))
463 (defgeneric add-if (solver lhs rhs &key mapping)
464 (:documentation "Add clauses for lhs -> rhs to SOLVER.")
465 (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity))
466 (add-formula solver `(:IMPLIES ,lhs ,rhs) mapping)))
468 (defgeneric add-iff (solver lhs rhs &key mapping)
469 (:documentation "Add clauses for lhs <-> rhs to SOLVER.")
470 (:method ((solver sat-solver) (lhs list) (rhs list) &key (mapping #'identity))
471 (add-formula solver `(:IFF ,lhs ,rhs) mapping)))