(q-sat x) finds a satisfying assignment for the UBDD x, if
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
(defun q-sat (x)
(declare (xargs :guard t))
(if (atom x)
(if (eq (cdr x) nil)
(cons t (q-sat (car x)))
(cons nil (q-sat (cdr x))))))
(implies (and (ubddp x) x)
(eval-bdd x (q-sat x))))