diff options
Diffstat (limited to 'guile')
-rw-r--r-- | guile/sat/helpers.scm | 19 | ||||
-rw-r--r-- | guile/sat/solver.scm | 49 |
2 files changed, 68 insertions, 0 deletions
diff --git a/guile/sat/helpers.scm b/guile/sat/helpers.scm new file mode 100644 index 0000000..6729382 --- /dev/null +++ b/guile/sat/helpers.scm @@ -0,0 +1,19 @@ +(define-module (sat helpers) + #:use-module (sat solver) + #:use-module (srfi srfi-1) + #:export (exactly-one-true)) + +(define (exactly-one-true v) + + ;; At least one of 'v' must be true + (add-clause v) + + ;; At least one of each pair in 'v' must be false + (pair-for-each + (lambda (v1p) + (for-each + (lambda (v2) + (add-clause (list (- (car v1p)) (- v2)))) + (cdr v1p))) + v)) + diff --git a/guile/sat/solver.scm b/guile/sat/solver.scm new file mode 100644 index 0000000..24eb7b1 --- /dev/null +++ b/guile/sat/solver.scm @@ -0,0 +1,49 @@ +(define-module (sat solver) + #:use-module (ice-9 popen) + #:use-module (ice-9 rdelim) + #:use-module (ice-9 format) + #:export (solve-sat + make-sat-variable + add-clause)) + + +(define last-variable (make-parameter #f)) +(define sat-clauses (make-parameter #f)) + + +(define (make-sat-variable) + (unless (last-variable) + (error "make-variable used outside solve-sat")) + (last-variable (1+ (last-variable))) + (last-variable)) + + +(define (add-clause clause) + (sat-clauses (cons clause (sat-clauses)))) + + +(define (write-dimacs n-variables clauses) + (with-output-to-file + "dimacs.cnf" + (lambda () + (format #t "p cnf ~a ~a\n" + n-variables + (length clauses)) + (for-each (lambda (clause) + (format #t "~{~d ~}0\n" clause)) + clauses))) + (let loop ((port (open-pipe* OPEN_READ "kissat" "dimacs.cnf"))) + (let ((line (read-line port))) + (unless (eof-object? line) + (format #t "Line '~a'\n" line) + (loop port))))) + + +(define-syntax solve-sat + (syntax-rules () + ((_ body ...) + (parameterize ((last-variable 0) + (sat-clauses '())) + body ... + (write-dimacs (last-variable) + (sat-clauses)))))) |