1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
3 ;;; satwrap.lisp --- SAT solvers wrapped for CL
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))))
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
)))
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."
81 :with max
:= (sat-solver-numvars solver
)
84 :always
(and (not (zerop v
))
87 (defmethod clause-valid ((solver sat-solver
) (clause vector
))
88 "Check that CLAUSE is a valid clause for SOLVER."
90 :with max
:= (sat-solver-numvars solver
)
93 :always
(and (not (zerop v
))
96 (defmacro iota
(n &optional
(start 1))
97 "Return a list of the N sequential integers starting at START (default: 1)."
98 (let ((i (gensym "i")))
103 (define-condition satwrap-condition
(error)
105 (:documentation
"Superclass of all conditions raised by satwrap code."))
107 (define-condition invalid-clause
(satwrap-condition)
108 ((solver :initarg
:solver
:reader invalid-clause-solver
)
109 (clause :initarg
:clause
:reader invalid-clause-clause
))
110 (:report
(lambda (condition stream
)
111 (format stream
"Invalid clause ~A for solver ~A"
112 (invalid-clause-clause condition
)
113 (invalid-clause-solver condition
)))))
115 (define-condition invalid-backend
(satwrap-condition)
116 ((name :initarg
:name
:reader invalid-backend-name
))
117 (:report
(lambda (condition stream
)
118 (declare (special *satwrap-backends
* *default-sat-backend
*))
119 (format stream
"Invalid backend ~S specified. Supported: ~{~S~^, ~}, default ~S."
120 (invalid-backend-name condition
)
121 (mapcar #'car
*satwrap-backends
*)
122 *default-sat-backend
*))))
124 (defmethod flush-to-backend ((solver sat-solver
))
125 "Populate backend, possibly flushing old backend contents."
126 (satwrap.backend
:synchronize-backend
(sat-solver-backend solver
)
127 (sat-solver-numvars solver
)
128 (sat-solver-new-clauses solver
)
129 '() ;; deleted clauses, not yet supported
130 (sat-solver-old-clauses solver
))
131 (loop :with deleted
:= '()
132 :for c
:in
(sat-solver-old-clauses solver
)
133 :unless
(find c deleted
:test
#'equal
)
134 :do
(push c
(sat-solver-new-clauses solver
)))
135 (setf (sat-solver-old-clauses solver
) (sat-solver-new-clauses solver
)
136 (sat-solver-new-clauses solver
) '()))
139 (defun make-sat-solver (&optional
(backend *default-sat-backend
*))
140 "Return a new sat solver instance. Optional argument BACKEND can be used to
141 specify which backend should be used. It defaults to *default-sat-backend*."
142 (let ((be (assoc backend
*satwrap-backends
* :test
#'eq
)))
144 (make-instance 'sat-solver
:backend
(make-instance (cdr be
)))
145 (error 'invalid-backend
:name backend
))))
147 (defgeneric add-variable
(solver)
148 (:documentation
"Add another variable to SOLVER. Returns new variable index.")
149 (:method
((solver sat-solver
))
150 (incf (sat-solver-numvars solver
))))
152 (defgeneric add-clause
(solver clause
)
153 (:documentation
"Add CLAUSE to SOLVER's cnf formula. Clause is consumed.")
154 (:method
((solver sat-solver
) (clause list
))
155 (if (clause-valid solver clause
)
156 (push clause
(sat-solver-new-clauses solver
))
157 (error 'invalid-clause
:clause clause
:solver solver
)))
158 (:method
((solver sat-solver
) (clause vector
))
159 (add-clause solver
(coerce clause
'list
))))
161 (defgeneric add-clauses
(solver clauses
)
162 (:documentation
"Add CLAUSES to SOLVER's cnf formula. Clauses are consumed.")
163 (:method
((solver sat-solver
) (clauses list
))
165 (add-clause solver c
))))
167 (defgeneric satisfiablep
(solver &key assume
)
168 (:documentation
"Check whether current CNF in SOLVER is satisfiable.
169 Keyword argument :ASSUME can provide a sequence of literals assumed TRUE or FALSE.
171 (:method
((solver sat-solver
) &key
(assume '()))
172 (if (clause-valid solver assume
) ;; misusing 'clause' concept here
174 (flush-to-backend solver
)
175 (satwrap.backend
:satisfiablep
(sat-solver-backend solver
) assume
))
176 (error 'invalid-clause
:clause assume
:solver solver
))))
178 (defgeneric solution
(solver &key interesting-vars
)
179 (:documentation
"Return solution for SOLVER. If unsat, return '(). If sat return
180 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.")
181 (:method
((solver sat-solver
)
182 &key
(interesting-vars (iota (sat-solver-numvars solver
))))
183 (satwrap.backend
:solution
(sat-solver-backend solver
) interesting-vars
)))
185 (defgeneric get-essential-variables
(solver)
186 (:documentation
"Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
187 Returns a list of literals fixed, sign according to phase.")
188 (:method
((solver sat-solver
))
189 ;; The backend may define a specialized method, but then it has to
190 ;; work on the one copy of data flushed to the solver. Precosat for example
191 ;; does not allow that, so we define the universal implementation here instead of
192 ;; a default implementation in the backend.
193 (let ((have-specialized-method
194 (find-method #'satwrap.backend
:get-essential-variables
196 `(,(class-of (sat-solver-backend solver
)))
198 (if have-specialized-method
200 (flush-to-backend solver
)
201 (satwrap.backend
:get-essential-variables
(sat-solver-backend solver
)))
203 (loop :for var
:of-type
(integer 1) :in
(iota (sat-solver-numvars solver
))
204 :as sat-for-
+ := (satisfiablep solver
:assume
`(,var
,@fixed
))
205 :as sat-for--
:= (satisfiablep solver
:assume
`(,(- var
) ,@fixed
))
207 ((and sat-for-
+ (not sat-for--
))
209 ((and (not sat-for-
+) sat-for--
)
210 (push (- var
) fixed
))))
214 (defmacro with-sat-solver
((name numatoms
&key
(backend *default-sat-backend
* backend-given
))
216 "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."
217 `(let ((,name
(make-sat-solver ,(if backend-given
219 '*default-sat-backend
*))))
220 (loop :repeat
,numatoms
:do
(add-variable ,name
))
224 (defmacro with-index-hash
((mapping &key
(test 'eq
)) objects
&body body
)
225 "Execute BODY while binding MAPPING to a hash-table (with predicate
226 TEST, defaults to #'cl:eq) mapping the elements of the sequence OBJECTS
227 to integer 1..[length objects].
228 Typically used to map objects to variables inside WITH-SAT-SOLVER."
229 (let ((o (gensym "objects")))
230 `(let* ((,o
,objects
)
231 (,mapping
(etypecase ,o
232 (list (loop :with ht
:= (make-hash-table :test
#',test
)
234 :for num
:of-type fixnum
:from
1
235 :do
(setf (gethash x ht
) num
)
236 :finally
(return ht
)))
237 (vector (loop :with ht
:= (make-hash-table :test
#',test
)
239 :for num
:of-type fixnum
:from
1
240 :do
(setf (gethash x ht
) num
)
241 :finally
(return ht
))))))
244 ;; convenience syntax for logical operations:
245 (defun standardize (tree)
246 "Convert tree of logical operations to elementary :NOT, :AND, :OR tree (preserving :ATOM).
247 Supports :IMPLY, :IFF, binary :XOR, and :NOR. "
250 (destructuring-bind (op . expr
)
254 (if (= 2 (length expr
))
255 `(:OR
(:NOT
,(standardize (car expr
)))
256 ,(standardize (cadr expr
)))
257 (error "non-binary :IMPLY operation: ~A" tree
)))
259 (if (= 2 (length expr
))
260 `(:AND
,(standardize `(:IMPLIES
,(car expr
) ,(cadr expr
)))
261 ,(standardize `(:IMPLIES
,(cadr expr
) ,(car expr
))))
262 (error "non-binary :IFF operation: ~A" tree
)))
264 (if (= 2 (length expr
))
265 (let ((e1 (standardize (first expr
)))
266 (e2 (standardize (second expr
))))
267 `(:OR
(:AND
,e1
(:NOT
,e2
))
268 (:AND
,e2
(:NOT
,e1
))))
269 (error "non-binary :XOR operation: ~A" tree
)))
271 `(:AND
,@(mapcar #'(lambda (p) `(:NOT
,(standardize p
))) expr
)))
273 (T `(,op
,@(mapcar #'standardize expr
))))))
276 (defun standard-tree->nnf
(tree)
277 "Move NOTs inward. Input must be AND/OR/NOT-only; returns NNF tree."
280 (destructuring-bind (op . expr
)
283 (:NOT
(if (= 1 (length expr
))
284 (let ((subexpr (first expr
)))
286 (case (first subexpr
)
287 ;; double-not: drop 2 levels
288 (:NOT
(standard-tree->nnf
(cadr subexpr
)))
290 (:AND
`(:OR
,@(mapcar #'(lambda (c)
291 (standard-tree->nnf
`(:NOT
,c
)))
294 (:OR
`(:AND
,@(mapcar #'(lambda (c)
295 (standard-tree->nnf
`(:NOT
,c
)))
297 ;; `quoted' atom: keep
298 (:ATOM
`(:NOT
,subexpr
))
299 (otherwise `(:NOT
,subexpr
)))
302 (error "non-unary :NOT expression: ~W" tree
)))
303 ;; other operators: AND, OR, ATOM: descend
305 `(,op
,@(mapcar #'standard-tree-
>nnf expr
))))))
309 (defun crossprod (list-of-lists)
310 "Return a list of all lists containing one element from each sublist of LIST-OF-LISTS."
311 (reduce #'(lambda (collected term
)
312 (loop :for x
:in term
:appending
313 (loop :for tail
:in collected
314 :collect
`(,x
,@tail
))))
316 :initial-value
'(())))
319 "Check that TREE is in CNF."
328 (and (not (eq :OR
(car f
)))
329 (not (eq :AND
(car f
))))
337 (every #'atomic
(cdr c
)))))
340 (defun distribute (tree)
341 "Pull out :ANDs to reduce standardized tree in NNF to CNF."
344 (:AND
(let ((sub-cnfs (mapcar #'distribute
(cdr tree
))))
345 (assert (every #'is-cnf sub-cnfs
)
347 "Not all in CNF: ~{~A~^~%~}" sub-cnfs
)
349 (loop :for sub-cnf
:in sub-cnfs
350 :if
(and (consp sub-cnf
)
351 (eq :AND
(car sub-cnf
)))
352 ;; AND(AND ..) = AND ..
353 :do
(dolist (clause (cdr sub-cnf
))
354 (push clause clauses
))
355 :else
:do
(push sub-cnf clauses
))
358 (dolist (term (mapcar #'distribute
(cdr tree
)))
359 (assert (is-cnf term
)
361 "~A not in CNF" term
)
364 (:AND
(push (cdr term
) ands
))
365 (:OR
(dolist (c (cdr term
))
367 (otherwise (push `(,term
) ands
)))
368 (push `(,term
) ands
)))
369 (let ((clauses (crossprod ands
)))
370 `(:AND
,@(mapcar #'(lambda (c)
373 `(:OR
,@ (loop :for subterm
:in c
374 :if
(and (consp subterm
)
375 (eq :OR
(car subterm
)))
376 ;; (OR(OR...)) == (OR ...)
377 :append
(cdr subterm
)
378 ;; if C is not an OR-clause
379 ;; it is considered atomic:
380 :else
:append
`(,subterm
)))))
387 (defun tree->cnf
(tree &optional
(mapping #'cl
:identity
) (atom-test #'eql
))
388 "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."
391 (and (not (eq :OR
(car f
)))
392 (not (eq :AND
(car f
))))
395 ;; destructively apply MAPPING
397 (setf cnf
(funcall mapping cnf
))
398 (setf (cdr cnf
) ;; we must be looking at an AND
399 (mapcar #'(lambda (clause)
401 (funcall mapping clause
)
402 `(:OR
,@(mapcar #'(lambda (lit)
403 (funcall mapping lit
))
408 (and (consp lit
) (eq :NOT
(car lit
))))
412 (:NOT
(atom-for (second lit
)))
416 (duplicate-literalsp (l1 l2
)
417 (funcall atom-test
(atom-for l1
) (atom-for l2
)))
419 (loop :for
(lit . haystack
) :on c
420 :as needle
:= (atom-for lit
)
421 :as negated
:= (and (consp lit
) (eq :NOT
(car lit
)))
422 :when
(find-if #'(lambda (x)
424 (not (negated-litp x
))
426 (funcall atom-test needle
(atom-for x
))))
429 :finally
(return NIL
)))
431 ;; destructively apply MAPPING
434 (setf (cdr cnf
) ;; we must be looking at an AND
435 (loop :for clause
:in
(cdr cnf
)
438 :else
:if
(not (trivial-clausep clause
))
439 :collect
`(:OR
,@(remove-duplicates
441 :test
#'duplicate-literalsp
)))))
447 (standardize tree
)))))))
450 (defgeneric add-formula
(solver formula
&key mapping atom-test
)
451 (:documentation
"Add logical FORMULA to SOLVER.
452 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).
453 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).")
454 (:method
((solver sat-solver
) (formula list
) &key
(mapping #'identity
) (atom-test #'eql
))
455 (dolist (c (cdr ;; drop outer :AND
456 (tree->cnf formula mapping atom-test
)))
457 (add-clause solver
(cdr ;; drop :OR
460 (defgeneric add-and
(solver literals
&key mapping
)
461 (:documentation
"Add clauses for AND(literals) to SOLVER.")
462 (:method
((solver sat-solver
) (literals list
) &key
(mapping #'identity
))
463 (add-formula solver
`(:AND
,@literals
) mapping
)))
465 (defgeneric add-or
(solver literals
&key mapping
)
466 (:documentation
"Add clauses for OR(literals) to SOLVER.")
467 (:method
((solver sat-solver
) (literals list
) &key
(mapping #'identity
))
468 (add-formula solver
`(:OR
,@literals
) mapping
)))
470 (defgeneric add-xor
(solver literals
&key mapping
)
471 (:documentation
"Add clauses for binary XOR(literals) to SOLVER.")
472 (:method
((solver sat-solver
) (literals list
) &key
(mapping #'identity
))
473 (add-formula solver
`(:XOR
,@literals
) mapping
)))
475 (defgeneric add-if
(solver lhs rhs
&key mapping
)
476 (:documentation
"Add clauses for lhs -> rhs to SOLVER.")
477 (:method
((solver sat-solver
) (lhs list
) (rhs list
) &key
(mapping #'identity
))
478 (add-formula solver
`(:IMPLIES
,lhs
,rhs
) mapping
)))
480 (defgeneric add-iff
(solver lhs rhs
&key mapping
)
481 (:documentation
"Add clauses for lhs <-> rhs to SOLVER.")
482 (:method
((solver sat-solver
) (lhs list
) (rhs list
) &key
(mapping #'identity
))
483 (add-formula solver
`(:IFF
,lhs
,rhs
) mapping
)))