(defun my-sat-revise-to-empty (variable clause domains)
  "Attempt to revise the DOMAIN of VARIABLE in CLAUSE down to nothing.

Return a cons cell with t and the revised domain of VARIABLE, or nil if
no revision is possible.  DOMAINS is an alist of all variable domains
that are lists."
  (if

      ;; Check if CLAUSE contains contradictory literals for VARIABLE:
      ;; both +VARIABLE and -VARIABLE.
      (and
       (any (lambda (literal) (eq literal (+ variable))) clause)
       (any (lambda (literal) (eq literal (- variable))) clause))

      ;; The CLAUSE is *self-contradictory*!
      ;; Return a domain, revised to nothing.
      (cons t '())))

(defun my-sat-revise-to-value (value variable clause domains)
  "Attempt to revise the DOMAIN of VARIABLE in CLAUSE to VALUE.

Return a cons cell with t and the revised domain of VARIABLE, or nil if
no revision is possible.  DOMAINS is an alist of all variable domains
that are lists."

  ;; Abort if there is nothing to revise.
  (let ((domain (alist-get variable domains)))
    (unless (or (null domain)
                (equal domain (list value)))

      ;; Compute the "deciding literal" from VARIABLE and VALUE:
      ;; +VARIABLE if VALUE = 1
      ;; -VARIABLE if VALUE = 0.
      (let ((literal (pcase value
                       (0 (- variable))
                       (1 (+ variable))
                       (_ (error "Invalid value")))))
        (if (and

             ;; Ensure the CLAUSE contains the "deciding literal".
             (any (lambda (literal*) (= literal* literal)) clause)

             ;; Ensure every literal in CLAUSE is one of:
             ;; - the "deciding literal"
             ;; - effective 0 as a positive literal with domain {0}
             ;; - effective 0 as a negative literal with domain {1}.
             (all (lambda (literal*)
                    (or (= literal* literal)
                        (let ((domain (alist-get (abs literal*) domains)))
                          (or (and (> literal* 0) (equal domain '(0)))
                              (and (< literal* 0) (equal domain '(1)))))))
                  clause))

            ;; VARIABLE value is *forced* to have the given VALUE!
            ;; Return a domain, revised to only VALUE or nothing.
            (cons t (if (member value domain) (list value) '())))))))

(defun my-sat-revise (variable clause domains)
  "Revise the DOMAIN of VARIABLE in CLAUSE, given all DOMAINS.

Return a cons cell with t and the revised domain of VARIABLE, or nil if
no revision is possible."
  (or (my-sat-revise-to-empty variable clause domains)
      (my-sat-revise-to-value 0 variable clause domains)
      (my-sat-revise-to-value 1 variable clause domains)))

(ert-deftest my-sat-revise/regression ()
  (should-not (my-sat-revise 2 '(-2 -3) '((2 . (0)) (3 . (0))))))

(ert-deftest my-sat-revise/no-change ()
  (should-not (my-sat-revise 1 '(1) '((1 . (1)))))
  (should-not (my-sat-revise 2 '(1 2) '((1 . (1)) (2 . (1))))))

(ert-deftest my-sat-revise/no-change/regression ()
  (should-not (my-sat-revise 2 '(-1 -2) '((1 . (0)) (2 . (0 1))))))

(ert-deftest my-sat-revise/revise-to-0 ()
  (should (equal (my-sat-revise 1 '(-1 2) '((1 . (0 1)) (2 . (0))))
                 '(t . (0)))))

(ert-deftest my-sat-revise/revise-to-0/invalid ()
  (should (equal (my-sat-revise 1 '(-1) '((1 . (1))))
                 '(t . ()))))

(ert-deftest my-sat-revise/revise-to-1 ()
  (should (equal (my-sat-revise 1 '(1 2) '((1 . (0 1)) (2 . (0))))
                 '(t . (1)))))

(ert-deftest my-sat-revise/revise-to-1/invalid ()
  (should (equal (my-sat-revise 1 '(1) '((1 . (0))))
                 '(t . ()))))

(ert-deftest my-sat-revise-duplicate ()
  (should (equal (my-sat-revise 1 '(1 1) '((1 . (0 1))))
                 '(t . (1)))))

(ert-deftest my-sat-revise/contradiction ()
  (should (equal (my-sat-revise 1 '(1 -1) '((1 . (0 1))))
                 '(t . ()))))