Implementing Symbolic Simulation Using SAT Solvers by Variables Partition

Although parametric representations and reparameterizations are used, the bottleneck of symbolic simulation is still the blowup of BDDs which may grow rapidly with the increase of simulation steps. In this paper, we implement symbolic simulation using SAT solvers with variables partition which reduces the sizes of BDDs and remains enough coverage while lowering backtracks of SAT solvers. This method partitions a big CNF into two smaller subsets A and B, and then divides the variables into three disjoint sets. Through the constraint that the symbolic values are only assigned to the variables which occur in both A and B, the symbolic simulation implemented by SAT solvers obtains both the fewer backtracks and lower memory occupation. This method is proved to be sound and complete.