loading...
An Efficient Sequential SAT Solver With Improved Search Strategies
Munich, Germany March 07-March 11
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2005.55Design, Automation and Test in Europe ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
F. Lu, University of California at Santa Barbara
M. K. Iyer, University of California at Santa Barbara
G. Parthasarathy, University of California at Santa Barbara
L.-C. Wang, University of California at Santa Barbara
K.-T. Cheng, University of California at Santa Barbara
K. C. Chen, Cadence Corporation
A sequential SAT solver Satori was recently proposed as an alternative to combinational SAT in verification applications. This paper describes the design of Seq-SAT - an efficient sequential SAT solver with improved search strategies over Satori. The major improvements include (1) a new and better heuristic for minimizing the set of assignments to state variables, (2) a new priority-based search strategy and a flexible sequential search framework which integrates different search strategies, and (3) a decision variable selection heuristic more suitable for solving the sequential problems. We present experimental results to demonstrate that our sequential SAT solver can achieve orders-of-magnitude speedup over Satori.
We plan to release the source code of Seq-SAT along with this paper.
Citation:
F. Lu, M. K. Iyer, G. Parthasarathy, L.-C. Wang, K.-T. Cheng, K. C. Chen, "An Efficient Sequential SAT Solver With Improved Search Strategies," date, vol. 2, pp.1102-1107, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005
Usage of this product signifies your acceptance of the Terms of Use.