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 :
https://search.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=1835656
بازگشت