;;; Wandering through the search space.

(defalias 'my-sat-mac #'my-sat-search)

(defun my-sat-search (clauses domains &optional all-solutions-p branch)
  "Return a list of domains revised to solutions.

If ALL-SOLUTIONS-P is non-nil, returns all solutions.  Otherwise,
returns a single solution, if some exists.

Implements the MAC (Maintaining Arc Consistency) algorithm."
  (let ((domains (my-sat-domains-copy domains branch)))
    (if-let* ((domains (my-sat-make-consistent clauses domains)))
        (cond ((my-sat-unfeasible-p domains) nil)
              ((my-sat-solved-p domains) (list domains))
              (t (let* ((branch-0 (my-sat-search clauses domains all-solutions-p 0))
                        (branch-1 (and (or (not branch-0) all-solutions-p)
                                       (my-sat-search clauses domains all-solutions-p 1))))
                   (append branch-0 branch-1)))))))