UC Santa Cruz

We study the problem of enumerating the satisfying assignments of smooth multivalued d-DNNF circuits in sum order. We measure the cost in terms of a preprocessing phase and the delay between consecutive answers, charging for both the size of the circuit and the number of variables. Producing each answer as a complete assignment takes time linear in the number of variables. We propose an algorithmic framework that avoids this cost by producing answers in an implicit representation. After preprocessing quasilinear in the size of the circuit, the delay for tree-shaped circuits is logarithmic in the number of answers already produced and independent of the number of variables. For general circuits, preprocessing incurs an additional factor of the number of variables, and one further term remains in the delay, logarithmic in the number of variables. An answer can be recovered explicitly from its implicit representation in additional linear time.