Method and System for Satisfiability Solving taking advantage of Information derived from Circuit Structure and Binary-Decision-Diagram Sweeping
Original Publication Date: 2004-Oct-01
Included in the Prior Art Database: 2004-Oct-01
Proposed is a new method for selecting the next decision variable in a structural SAT solver. The next decision variable is selected from among those on the justification frontier using a score that includes circuit topology information together with partitioning information (cut-frontiers) obtained by propagating BDDs through the circuit using BDD-sweeping. This method prioritizes the vertices in the justification frontier based on the cut-levels identified by BDD-sweeping, which effectively localizes the search space for the SAT solver, helping it to solve the problem more quickly by potentially pruning large portions of the search space.