(defalias 'my-sat-ac3 #'my-sat-make-consistent)

(defun my-sat-make-consistent (clauses domains)
  "AC3 algorithm."
  (catch 'return
    (let ((domains (my-sat-domains-copy domains))) ;; TODO Do we need to?
      (named-let continue ((queue (my-sat-queue clauses)))
        (pcase queue
          ('() domains)                      ; Done.
          (`((,variable . ,clause) . ,queue) ; More to do.
           (progn
             (pcase (my-sat-revise variable clause domains)
               ('nil (continue queue domains)) ; No revision, continue.
               ('(t . ()) (throw 'return nil)) ; No solution, abort.
               (`(t . ,domain) ; Revision, update domains, queue neighbors, and continue.
                (progn
                  (setcdr (assoc variable domains) domain)
                  (let* ((neighbors (my-sat-queue-neighbors clause clauses))
                         (queue (delete-dups (append neighbors queue))))
                    (continue queue domains))))))))))))

(ert-deftest my-sat-make-consistent ()
  (should (equal (my-sat-make-consistent '((1 2) (3 4))
                                         '((1 . (0))
                                           (2 . (0 1))
                                           (3 . (0))
                                           (4 . (0 1))))
                 '((1 . (0))
                   (2 . (1))
                   (3 . (0))
                   (4 . (1))))))

(ert-deftest my-sat-make-consistent/no-solution ()
  (let ((domains '((1 . (0))
                   (2 . (0))
                   (3 . (0))
                   (4 . (0)))))
    (should-not (my-sat-make-consistent '((1 2) (3 4)) domains))))