Rudy's OBTF

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

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