Sciweavers

ICCAD
2001
IEEE

Faster SAT and Smaller BDDs via Common Function Structure

14 years 15 days ago
Faster SAT and Smaller BDDs via Common Function Structure
The increasing popularity of SAT and BDD techniques in verification and synthesis encourages the search for additional speed-ups. Since typical SAT and BDD algorithms are exponential in the worst-case, the structure of real-world instances is a natural source of improvements. While SAT and BDD techniques are often presented as mutually exclusive alternatives, our work points out that both can be improved via the use of the same structural properties of instances. Our proposed methods are based on efficient problem partitioning and can be easily applied as pre-processing with arbitrary SAT solvers and BDD packages without source code modifications. Finding a better variable-ordering is a well recognized problem for both SAT solvers and BDD packages. Currently, all leading edge variable-ordering algorithms are dynamic, in the sense that they are invoked many times in the course of the “host” algorithm that solves SAT or manipulates BDDs. Examples include the DLCS ordering for SAT so...
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2001
Where ICCAD
Authors Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Comments (0)