Constraints partitioning for RTL Satis ability solving by YICES

This paper presents a hypergraph partitioning based constraints decomposition procedure to guide an RTL satisfiability solver. The constraints with their correlative variables drawn from the RTL circuit are modeled as a hypergraph and techniques based on hypergraph partitioning are employed to decompose constraints. This scheme solves the partitioned problems respectively and reconciles them via cut-set variables, which has led to pruning of the search space and results in solving the satisfiability problem efficiently. Comparison with the original SMT solver YICES shows that the procedure is fast and can significantly increase the performance of the RTL SAT engine.