;;; Extending the queue of variable-clause pairs.

(defun my-sat-queue-neighbors (clause clauses)
  "Return the neighbors of CLAUSE VARIABLE within all CLAUSES.

Neighbors are variables in CLAUSES other than CLAUSE that share at least
one variable with CLAUSE."

  ;; Collect all variables mentioned in CLAUSE.
  (let ((variables (delete-dups (mapcar #'abs clause))))

    ;; Consider all CLAUSES.
    (mapcan (lambda (clause*)
              (if (and

                   ;; Consider all CLAUSES except CLAUSE.
                   (not (equal clause* clause))

                   ;; Consider all CLAUSES that share variable(s) with CLAUSE.
                   (any (lambda (literal)
                          (member (abs literal) variables))
                        clause*))

                  ;; Map literals to variable-clause pairs.
                  (mapcar (lambda (literal)
                            (cons (abs literal) clause*))
                          clause*)))

            clauses)))

(ert-deftest my-sat-neighbors ()
  (should (equal (my-sat-queue-neighbors '(1 -2) '((1 -2)
                                                   (-1 2 3)
                                                   (4)
                                                   (-2)))
                 '((1 . (-1 2 3))
                   (2 . (-1 2 3))
                   (3 . (-1 2 3))
                   (2 . (-2))))))