Checking satisfiability of a conjunction of BDDs

Procedures for Boolean satis ability most commonly work with Conjunctive Normal Form. Powerful SAT techniques based on implications and con icts can be retained when the usual CNF clauses are replaced with BDDs. BDDs provide more powerful implication analysis, which can reduce the computational e ort required to determine satis ability.

• Type: Conference
• Year: 2003
• Where: DAC
• Authors: Robert F. Damiano, James H. Kukula
• Keywords: Boolean Satis Ability, DAC 2003, Design Automation, Powerful Implication Analysis