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

Volume

1

fYear

2004

fDate

16-20 Feb. 2004

Firstpage

272

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe Conference and Exhibition, 2004. Proceedings

ISSN

1530-1591

Print_ISBN

0-7695-2085-5

Type

conf

DOI

10.1109/DATE.2004.1268860

Filename

1268860