blob: f633c317735b9885de8b2bf3f1097789a972a505 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(define-module (sat solver)
#:use-module (ice-9 popen)
#:use-module (ice-9 rdelim)
#:use-module (ice-9 format)
#:export (solve-sat
sat-context
make-sat-variable
add-clause))
(define last-variable (make-parameter 0))
(define sat-clauses (make-parameter '()))
(define (make-sat-variable)
(last-variable (1+ (last-variable)))
(last-variable))
(define (add-clause clause)
(sat-clauses (cons clause (sat-clauses))))
(define (vline->integers line)
(cdr
(map string->number
(string-split line #\space))))
(define (set-values! value-array values)
(for-each
(lambda (val)
;; If exactly zero, don't set anything
(cond
((> val 0)
(array-set! value-array #t val))
((< val 0)
(array-set! value-array #f (- val)))))
values))
(define* (solve-sat #:key (solver "kissat"))
;; Prepare CNF input
(with-output-to-file
"dimacs.cnf"
(lambda ()
(format #t "p cnf ~a ~a\n"
(last-variable)
(length (sat-clauses)))
(for-each (lambda (clause)
(format #t "~{~d ~}0\n" clause))
(sat-clauses))))
;; Run the solver and parse output
(let ((values (make-array 'none (list 0 (last-variable)))))
(let loop ((port (open-pipe* OPEN_READ solver "dimacs.cnf")))
(let ((line (read-line port)))
(unless (eof-object? line)
(cond
((char=? (string-ref line 0) #\v)
(set-values! values (vline->integers line)))
((string=? line "s UNSATISFIABLE")
(error "Unsatsfiable!")))
(loop port))))
values))
(define-syntax sat-context
(syntax-rules ()
((_ body ...)
(parameterize ((last-variable 0)
(sat-clauses '()))
body ...))))
|
