Rudy’s OBTF Rudolf Adamkovič

Home / Computer science / SAT solver / Practice implementation: Emacs Lisp


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

© 2025 Rudolf Adamkovič under GNU General Public License version 3.
Made with Emacs and secret alien technologies of yesteryear.