A Novel SAT All-Solutions Solver for Efficient Preimage Computation

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.

• Type: Conference
• Year: 2004
• Where: DATE
• Authors: Bin Li, Michael S. Hsiao, Shuo Sheng
• Keywords: DATE 2004, Hardware, Primary Input Variables, Smaller Cut Sets, Success-driven Learning Algorithm