		Search-engine friendly clone of the ACL2 documentation.

Ubdds

Bdd-sat-dfs

(bdd-sat-dfs x) finds a satisfying assignment for the UBDD x, if one exists. It works even if x is not a well-formed UBDD, but it might be slow in that case.

Definitions and Theorems

Function: bdd-sat-dfs

(defun bdd-sat-dfs (x)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (let* ((a (car x)) (d (cdr x)))
      (cond ((and (atom a) a) '(t))
            ((and (atom d) d) '(nil))
            (t (let ((rec1 (bdd-sat-dfs a)))
                 (if rec1 (cons t rec1)
                   (let ((rec2 (bdd-sat-dfs d)))
                     (and rec2 (cons nil rec2))))))))))

Theorem: bdd-sat-dfs-produces-satisfying-assign

(defthm bdd-sat-dfs-produces-satisfying-assign
  (implies (bdd-sat-dfs x)
           (eval-bdd x (bdd-sat-dfs x))))

Theorem: bdd-sat-dfs-not-satisfying-when-nil

(defthm bdd-sat-dfs-not-satisfying-when-nil
  (implies (and (consp x) (not (bdd-sat-dfs x)))
           (not (eval-bdd x vars))))

Theorem: bdd-sat-dfs-correct

(defthm bdd-sat-dfs-correct
  (implies (eval-bdd x vars)
           (eval-bdd x (bdd-sat-dfs x))))