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.
Method and System for Satisfiability Solving taking advantage of Information derived from Circuit Structure and Binary -Decision-Diagram Sweeping
Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, timing analysis, and false-path analysis, require Boolean reasoning on problems derived from circuit structures. The two main approaches used for such applications are Binary Decision Diagrams (BDDs) and Satisfiability (SAT) solving. The former converts the problem into a functionally canonical form, while the latter systematically searches for a consistent assignment of values for the variables of the problem. Typically, SAT solvers are based on the Davis-Putnam procedure that attempts to find a consistent assignment using a branch-and-bound approach. Unsatisfiability is proven if the SAT solver exhaustively enumerates all possible cases without finding a satisfying assignment. Most SAT solvers work on a Conjunctive Normal Form (CNF) representation of the problem, and are not implemented as native circuit-based solvers. Such solvers do not take advantage of the circuit information such as connectivity, topology etc. to their advantage to aid in the SAT-solving process. While structural SAT solvers exist, such as Automatic Test Pattern Generation (ATPG) tools they are typically application specific. While they do take advantage of structural information since they operate on the circuit structure directly, they do not go beyond simply looking at the connectivity.
The three main steps of the SAT process are: Imply, Decide, and Backtrack. "Imply" propagates all implications based on the current variable assignments. For example, a logical '1' at the output of an AND gate implies that all its inputs must also assume a logical '1' value, and a logical '0' at any input of an AND gate implies that the output must also assume a logical '0' value. Once all implications have been made, "Decide" selects a variable not yet assigned and picks a value (logical '0' or logical '1') to assign to it. The assignment is made and "Imply" is again called. This process repeats until all variables are assigned or a conflict is detected, for example if all inputs of an AND gate are logical '1' but the output is required to be logical '0', in which case the search must backtrack to undo a previous decision. Most modern SAT solvers will analyze the conflict to identify the earliest decision responsible for the conflict (non-chronological backtracking) and record the condition(s) leading to the conflict in the form of a learned clause, which can reduce the number of cases that must be explicitly enumerated by the SAT solver and thus greatly improve its performance. In an ATPG tool or structural SAT solver, each vertex in the circuit graph is generally considered a variable, and the "Decide" step often restricts the variable selection to those vertices on a "justification frontier". The justification frontie...