(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))