Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04) Paris, France February 16-February 20 ISBN: 0-7695-2085-5
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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb