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