Title :
A novel SAT all-solutions solver for efficient preimage computation
Author :
Li, Bin ; Hsiao, Michael S. ; Sheng, Shuo
Author_Institution :
Dept. of Electr. & Comput. Eng., Virginia Tech., Blacksburg, VA, USA
Abstract :
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.
Keywords :
binary decision diagrams; computability; sequential circuits; BDD; OBDD format; PI variables; SAT; SOLALL; all-solutions solver; cut sets; efficient preimage computation; learning algorithm; marked CNF database; primary input variables; quantified-jump-back; sequential circuits; success-conflict-driven learning; Automatic test pattern generation; Binary decision diagrams; Boolean functions; Circuit testing; Data structures; Explosions; Graphics; Input variables; Sequential circuits; Spatial databases;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings
Print_ISBN :
0-7695-2085-5
DOI :
10.1109/DATE.2004.1268860
