BDD construction for all solutions SAT and efficient caching mechanism
Takahisa Toda, Koji Tsuda · 2015
We improve an existing OBDD-based method of computing all total satisfying assignments of a Boolean formula, where an OBDD means an ordered binary decision diagram that is not necessarily reduced. To do this, we introduce lazy caching and finer caching by effectively using unit propagation. We implement our methods on top of a modern SAT solver, and show by experiments that lazy caching significantly accelerates the original method and finer caching in turn reduces an OBDD size.