Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

DAC
2003
ACM

favoriteEmaildiscussreport

139views Computer Architecture» more DAC 2003»

Checking satisfiability of a conjunction of BDDs

14 years 5 months ago

Checking satisfiability of a conjunction of BDDs

Download research.synopsys.com

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.

Robert F. Damiano, James H. Kukula

Real-time Traffic

Boolean Satis Ability | DAC 2003 | Design Automation | Powerful Implication Analysis |

claim paper

Related Content

» Extending Existential Quantification in Conjunctions of BDDs

» CirCUs A Satisfiability Solver Geared towards Bounded Model Checking

» Learning from BDDs in SATbased bounded model checking

» On the Relation between SAT and BDDs for Equivalence Checking

» Extended Resolution Proofs for Conjoining BDDs

» GradedCTL Satisfiability and Symbolic Model Checking

» Abstraction and BDDs Complement SATBased BMC in DiVer

» Using Combinatorial Optimization Methods for Quantification Scheduling

» Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points

Post Info
More Details (n/a)

Added	13 Nov 2009
Updated	13 Nov 2009
Type	Conference
Year	2003
Where	DAC
Authors	Robert F. Damiano, James H. Kukula

Comments (0)