DocumentCode
1835656
Title
Checking satisfiability of a conjunction of BDDs
Author
Damiano, Robert ; Kukula, James
Author_Institution
Adv. Technol. Group, Synopsis Inc., Hillsboro, OR, USA
fYear
2003
fDate
2-6 June 2003
Firstpage
818
Lastpage
823
Abstract
Procedures for Boolean satisfiability most commonly work with Conjunctive Normal Form. Powerful SAT techniques based on implications and conflicts can be retained when the usual CNF clauses are replaced with BDDs. BDDs provide more powerful implication analysis, which can reduce the computational effort required to determine satisfiability.
Keywords
Boolean functions; binary decision diagrams; computability; BDD; Boolean satisfiability; CNF; SAT technique; binary decision diagram; conjunctive normal form; implication analysis; Automatic test pattern generation; Binary decision diagrams; Boolean functions; Data structures; Design automation; Engines; Formal languages; History; Logic; Permission;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2003. Proceedings
Print_ISBN
1-58113-688-9
Type
conf
DOI
10.1109/DAC.2003.1219131
Filename
1219131
Link To Document