Q-sat
(q-sat x) finds a satisfying assignment for the UBDD x, if
one exists.
Assuming x is a well-formed UBDD, the only time there isn't
a satisfying assignment is when x represents the constant false function,
i.e., when x is nil. In any other case it's easy to construct some
list of values for which eval-bdd returns true.
BOZO naming. This shouldn't start with q- since it's constructing a
list of values instead of a UBDD.
Definitions and Theorems
Function: q-sat
(defun q-sat (x)
(declare (xargs :guard t))
(if (atom x)
nil
(if (eq (cdr x) nil)
(cons t (q-sat (car x)))
(cons nil (q-sat (cdr x))))))
Theorem: q-sat-correct
(defthm q-sat-correct
(implies (and (ubddp x) x)
(eval-bdd x (q-sat x))))
