Hybrid BDD and all-sat method for model checking and other application

We present a new hybrid BDD and SAT-based algorithm for model checking. Our algorithm is based on backward search, where each pre-image computation consists of an ecient All-SAT proce-dure. The All-SAT procedure exploits a graph representation of the model to dynamically prune the search space, thus preventing un-necessary search in large sub-spaces, and for identifying independent sub-problems. Apart from the SAT mechanisms, BDD structures are used for storing the input to, and output of the pre-image compu-tation. In this way, our hybrid approach enjoys the benets of both worlds: on the one hand, basing the pre-image computation on SAT technology avoids expensive BDD quantication operations and the corresponding state space blow up. On the other hand, our model checking framework still enjoys the advantages of symbolic space re-duction in holding intermediate images. Furthermore, our All-SAT analyzes the model and avoids redundant exploration of sub-spaces that are completely full with solutions, paying in these cases for the instantiation of a single assignment only. We implemented our algorithm using the zCha SAT solver and the CUDD BDD library. Our experimental results are encouraging, proving that there is a potential for substantial improvement over existing model checking schemes. 1 Te ch ni o