Practice implementation: Emacs Lisp

• Solver: Solving
  

  (defun my-sat-solve (clauses &optional all-solutions-p)
    "Solve a Boolean satisfaction problem.
  
  Returns a list containing one solution, or all solutions if
  ALL-SOLUTIONS is non-nil.
  
  The problem is specified as CNF (Conjunctive Normal Form), that is
  conjunctions of disjunctions.  Each clause is a list of integers
  representing literals, possibly negated."
    (let* ((domains (my-sat-domains clauses))
           (domains (my-sat-search clauses domains all-solutions-p)))
      (mapcar #'my-sat-solution domains)))
  

• Solver: Creating domains
  

  (defun my-sat-domains (clauses)
    (mapcar (lambda (variable) (cons variable '(0 1)))
            (delete-dups (mapcar #'abs (apply #'append clauses)))))
  

  (ert-deftest my-sat-domains/no-clauses ()
    (should (equal (my-sat-domains '()) '())))
  
  (ert-deftest my-sat-domains/single-clause ()
    (should (equal (my-sat-domains '((1)))
                   '((1 . (0 1)))))
    (should (equal (my-sat-domains '((1 2)))
                   '((1 . (0 1))
                     (2 . (0 1))))))
  
  (ert-deftest my-sat-domains/multiple-clauses ()
    (should (equal (my-sat-domains '((1) (2)))
                   '((1 . (0 1))
                     (2 . (0 1)))))
    (should (equal (my-sat-domains '((1) (1 2) (3)))
                   '((1 . (0 1))
                     (2 . (0 1))
                     (3 . (0 1))))))
  
  (ert-deftest my-sat-domains/negated-literals ()
    (should (equal (my-sat-domains '((1 -2) (-1 2)))
                   '((1 . (0 1))
                     (2 . (0 1))))))
  

• Solver: Extracting solutions
  

  (defun my-sat-solution (domains)
    "Return the solution contained in DOMAINS, if any.
  Returns a sorted alist with variables and their values."
    (catch 'abort
      (mapcar (pcase-lambda (`(,variable . (,value ,other-value)))
                (if other-value (throw 'abort nil)
                  (cons variable value)))
              (sort domains))))
  

  (ert-deftest my-sat-solution ()
    (should (equal (my-sat-solution '((1 . (0)))) '((1 . 0))))
    (should (equal (my-sat-solution '((1 . (0)) (2 . (1)))) '((1 . 0) (2 . 1)))))
  
  (ert-deftest my-sat-solution/trivial ()
    ;; Two perspectives, single truth: trivially solved or no solution.
    (should (equal (my-sat-solution '()) '()))
    (should-not (my-sat-solution '())))
  
  (ert-deftest my-sat-solution/unsolved ()
    (should-not (my-sat-solution '((1 . (0 1)) (2 . (1)))))
    (should-not (my-sat-solution '((1 . (0)) (2 . (0 1))))))
  
  (ert-deftest my-sat-solution/unfeasible ()
    (should-not (my-sat-solution '((1 . (0 1)) (2 . ()))))
    (should-not (my-sat-solution '((1 . ()) (2 . (0 1))))))
  

• Search
  
  • depth-first search
  • branching strategy

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

• Search: Branching
  

  (defun my-sat-domains-copy (domains &optional branch)
    "Return a deep copy of DOMAINS.
  
  DOMAINS is an alist from variable numbers (positive integers) to
  domains (lists).
  
  With BRANCH, constrain the first undecided variable to BRANCH."
    (let ((copy (copy-tree domains)))
      (when branch
        (setcdr (rassoc '(0 1) copy)
                (list branch)))
      copy))
  

  (ert-deftest my-sat-domains-copy/empty ()
    (should-not (my-sat-domains-copy '())))
  
  (ert-deftest my-sat-domains-copy/single-member ()
    (should (equal (my-sat-domains-copy '((1 . (0 1))))
                   '((1 . (0 1))))))
  
  (ert-deftest my-sat-domains-copy/single-member/pointer ()
    (let ((original '((1 . (0 1)))))
      (should-not (eq (my-sat-domains-copy original) original))))
  
  (ert-deftest my-sat-domains-copy/multiple-members ()
    (should (equal (my-sat-domains-copy '((1 . (0 1)) (2 . (0))))
                   '((1 . (0 1)) (2 . (0))))))
  
  (ert-deftest my-sat-domains-copy/branch/first ()
    (should (equal (my-sat-domains-copy '((1 . (0 1)) (2 . (0 1))) 1)
                   '((1 . (1)) (2 . (0 1))))))
  
  (ert-deftest my-sat-domains-copy/branch/second ()
    (should (equal (my-sat-domains-copy '((1 . (0)) (2 . (0 1))) 0)
                   '((1 . (0)) (2 . (0))))))
  

• Search: Detecting dead-ends
  

  (defun my-sat-unfeasible-p (domains)
    "Return non-nil if DOMAINS cannot possibly lead to a solution."
    (rassoc nil domains))
  
  (ert-deftest my-sat-unfeasible-p ()
    (should (my-sat-unfeasible-p '((1 . ()))))
    (should (my-sat-unfeasible-p '((1 . (0 1)) (2 . ())))))
  
  (ert-deftest my-sat-unfeasible-p/nil ()
    (should-not (my-sat-unfeasible-p '())) ;; Trivially solved.
    (should-not (my-sat-unfeasible-p '((1 . (0 1)) (2 . (0 1)))))
    (should-not (my-sat-unfeasible-p '((1 . (0)) (2 . (1))))))
  

• Search: Detecting solutions
  

  (defun my-sat-solved-p (domains)
    "Return non-nil if DOMAINS contain the solution."
    (all (pcase-lambda (`(_variable . (_value ,other-value)))
           (not other-value))
         domains))
  

  (ert-deftest my-sat-solved-p ()
    (should (my-sat-solved-p '())) ;; Trivially solved.
    (should (my-sat-solved-p '((1 . (0)))))
    (should (my-sat-solved-p '((1 . (0)) (2 . (1))))))
  
  (ert-deftest my-sat-solved-p/nil ()
    (should-not (my-sat-solved-p '((1 . (0 1)) (2 . (1)))))
    (should-not (my-sat-solved-p '((1 . (0)) (2 . (0 1))))))
  

• Arc consistency
  

  AC3 algorithm

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

• Arc consistency: Creating queue
  

  AC3 queue of variable-clause pairs

  (defun my-sat-queue (clauses)
    "Return a list of all variable-clause pairs in CLAUSES."
    (mapcan (lambda (clause)
              (mapcar (lambda (literal)
                        (let ((variable (abs literal)))
                          (cons variable clause)))
                      clause))
            clauses))
  

  (ert-deftest my-sat-queue ()
    (should (equal (my-sat-queue '((1 2) (2 3)))
                   '((1 . (1 2))
                     (2 . (1 2))
                     (2 . (2 3))
                     (3 . (2 3))))))
  
  (ert-deftest my-sat-queue/negated-literals ()
    (should (equal (my-sat-queue '((1 -2 3)))
                   '((1 . (1 -2 3))
                     (2 . (1 -2 3))
                     (3 . (1 -2 3))))))
  

• Arc consistency: Re-queuing neighbors
  

  ;;; 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
  
                    ;; Input clause.
                    '(1 -2)
  
                    ;; Input clauses.
                    '((1 -2)
                      (-1 2 3)
                      (4)
                      (-2)))
  
                   ;; Expected output.
                   '((1 . (-1 2 3))
                     (2 . (-1 2 3))
                     (3 . (-1 2 3))
                     (2 . (-2))))))
  

• Arc consistency: Revising domains
  

  (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:
        ;; - literal +VARIABLE if VALUE = 1
        ;; - literal -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 . ()))))