Abstract
In this paper, we introduce a novel preimage computation technique that directly computes the circuit cofactors without an explicit search for any satisfiable solution. We use an implicit search on the primary inputs of a sequential circuit to compute all the circuit cofactors for the target preimage. In order to alleviate the computational cost, aggressive learning techniques are introduced that reason on the search-states by analyzing the relations among circuit cofactors. Such analysis generates search-state induced clauses that directly help to prune the cofactor space during preimage computation and to perform non-chronological backtracking. Experimental results show that a significant improvement can be achieved in both performance and capacity as compared to the existing techniques.