Title :
Speeding up SAT for EDA
Author :
Pilarski, Slawomir ; Hu, Gracia
Author_Institution :
Synopsys Inc., Beaverton, OR, USA
Abstract :
This paper presents performance results for a new SAT solver designed specifically for EDA applications. The new solver significantly outperforms most efficient SAT solvers-Chaff, SATO, and GRASP-on a large set of benchmarks. Performance improvements for standard benchmark groups vary from 1.5× to 60×. They were achieved through a new decision-making strategy and more efficient Boolean constraint propagation (BCP)
Keywords :
Boolean algebra; computability; decision theory; electronic design automation; search problems; Boolean constraint propagation; Boolean satisfiability problem; EDA applications; SAT solver; decision-making strategy; performance improvements; standard benchmark groups; Automatic testing; Benchmark testing; Business continuity; Circuits; Decision making; Design automation; Electronic design automation and methodology; Europe; Packaging machines;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-7695-1471-5
DOI :
10.1109/DATE.2002.998437