loading...
A Novel SAT All-Solutions Solver for Efficient Preimage Computation
Paris, France February 16-February 20
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268860Design, Automation and Test in Europe ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Bin Li, Michael S. Hsiao, Shuo Sheng, "A Novel SAT All-Solutions Solver for Efficient Preimage Computation," Design, Automation and Test in Europe Conference and Exhibition, vol. 1, pp. 10272, Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/DATE.2004.1268860,
author = {Bin Li and Michael S. Hsiao and Shuo Sheng},
title = {A Novel SAT All-Solutions Solver for Efficient Preimage Computation},
journal ={Design, Automation and Test in Europe Conference and Exhibition},
volume = {1},
year = {2004},
issn = {1530-1591},
pages = {10272},
doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268860},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Design, Automation and Test in Europe Conference and Exhibition
TI - A Novel SAT All-Solutions Solver for Efficient Preimage Computation
SN - 1530-1591
SP
EP
A1 - Bin Li,
A1 - Michael S. Hsiao,
A1 - Shuo Sheng,
PY - 2004
KW - null
VL - 1
JA - Design, Automation and Test in Europe Conference and Exhibition
ER -
 
Bin Li, Virginia Tech.
Michael S. Hsiao, Virginia Tech.
Shuo Sheng, Mentor Graphics Corporation
In this paper, we present a novel all-solutions preimage SAT solver, SOLALL, with the following features: (1) a new success-driven learning algorithm employing smaller cut sets; (2) a marked CNF database non-trivially combining success/conflict-driven learning; (3) quantified-jump-back dynamically quantifying primary input variables from the preimage; (4) improved free BDD built on the fly, saving memory and avoiding inclusion of PI variables; finally, (5) a practical method of storing all solutions into a canonical OBDD format. Experimental results demonstrated the efficiency of the proposed approach for very large sequential circuits.
Citation:
Bin Li, Michael S. Hsiao, Shuo Sheng, "A Novel SAT All-Solutions Solver for Efficient Preimage Computation," date, vol. 1, pp.10272, Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.