# US 7,610,570 B1 · Method and mechanism for using systematic local search for SAT solving

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 7,610,570 B1
- Document ID: US7610570B1
- Status: Granted
- Kind: B1
- Application number: 11/407,864
- Filed: 2006-04-19
- Granted: 2009-10-27
- Earliest claimed: 2006-04-19
- Assignees: Cadence Design Systems, Inc.
- Inventors: Evgueni Goldberg
- Web page: https://patentgrep.com/patent/US7610570B1

## CPC

- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

An improved method and mechanism for designing and verifying an electrical circuit design is provided using an improved SAT-solver which uses complete assignments and systematic local search to provides improved performance. In one approach, the sat-solver maintains a complete assignment that is changed one variable at a time. A variable is fixed within the falsified set of clauses.

## Claims

### Claim 1

A method for implementing an integrated circuit design, comprising:
identifying an integrated circuit design to operate upon with an electronic design automation tool, the electronic design automation tool comprising a SAT-solver mechanism;
converting the integrated circuit design into a formula for which Boolean satisfiability is addressed by the SAT-solver mechanism;
solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment; and
generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable.

### Claim 2 (depends on 1)

The method of claim 1 in which a variable x of a current complete assignment is fixed.

### Claim 3 (depends on 2)

The method of claim 2 further comprising visiting points after fixing x, in which all points visited after fixing x have the same value of x, until x is unfixed.

### Claim 4 (depends on 2)

The method of claim 2 in which a next variable to be fixed is chosen among variables of the clauses falsified by the current complete assignment.

### Claim 5 (depends on 1)

The method of claim 1 in which the Boolean constraint propagation (BCP) procedure is invoked if there is a clause C of the current formula such that all literals of (but one are set to 0 by fixed assignments and a variable x of C is not fixed yet.

### Claim 6 (depends on 5)

The method of claim 5 in which the BCP procedure fixes x at a value satisfying the clause C.

### Claim 7 (depends on 5)

The method of claim 5 in which a current point p changes its value in variable x if the BCP procedure fixes x at the value that disagrees with the value of x corresponding to p.

### Claim 8 (depends on 2)

The method of claim 2 in which a conflict occurs if all literals of a clause of a current formula are set to 0 by fixed assignments.

### Claim 9 (depends on 8)

The method of claim 8 in which a conflict clause is generated and added to the current formula.

### Claim 10 (depends on 2)

The method of claim 2 in which the choice of the variable to fix is based on activity of literals of variables.

### Claim 11 (depends on 10)

The method of claim 10 in which the activity of the literals and/or the variable is computed based on the presence of the literals and/or the variables in clauses involved in conflicts.

### Claim 12 (depends on 2)

The method of claim 2 in which an active literal lit(x) of the variable x chosen among clauses falsified by the current assignment is set to 1 and the assignment to x setting lit(x) to 1 is fixed.

### Claim 13 (depends on 12)

The method of claim 12 in which a current point p does not change if its assignment to x sets lit(x) to 1.

### Claim 14 (depends on 12)

The method of claim 12 which a current point p changes its value in the variable x, if its current assignment to x sets lit(x) to 0.

### Claim 15 (depends on 1)

The method of claim 1 which is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 16 (depends on 1)

The method of claim 1 in which the SAT-solver performs one or more restarts.

### Claim 17 (depends on 16)

The method of claim 16 in which a new iteration based upon the one or more restarts uses a last point reached in a previous iteration as an initial point.

### Claim 18 (depends on 16)

The method of claim 16 in which a restart is performed if a threshold value is exceeded.

### Claim 19 (depends on 18)

The method of claim 18 in which the threshold value corresponds to a number of conflicts.

### Claim 20 (depends on 1)

The method of claim 1 in which the SAT-solver does not perform a restart.

### Claim 21 (depends on 1)

The method of claim 1 in which decision making is local.

### Claim 22

A method for operating a SAT-solver, comprising:
receiving a formula for which Boolean satisfiability is to be addressed;
solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment;
generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable; and
storing results of solving the Boolean satisfiability in a computer readable medium.

### Claim 23 (depends on 22)

The method of claim 22 in which a variable x of a current complete assignment is fixed.

### Claim 24 (depends on 23)

The method of claim 23 further comprising visiting points after fixing x, in which all points visited after fixing x have the same value of x, until x is unfixed.

### Claim 25 (depends on 23)

The method of claim 23 in which a next variable to be fixed is chosen among variables of the clauses falsified by the current complete assignment.

### Claim 26 (depends on 23)

The method of claim 23 in which a conflict occurs if all literals of a clause of a current formula are set to 0 by fixed assignments.

### Claim 27 (depends on 26)

The method of claim 26 in which a conflict clause is generated and added to the current formula.

### Claim 28 (depends on 23)

The method of claim 23 in which the choice of the variable to fix is based on activity of literals of variables.

### Claim 29 (depends on 23)

The method of claim 23 in which an active literal lit(x) of the variable x chosen among clauses falsified by the current assignment is set to 1 and the assignment to x setting lit(x) to 1 is fixed.

### Claim 30 (depends on 22)

The method of claim 22 in which the electronic design automation tool is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 31 (depends on 22)

The method of claim 22 in which the SAT-solver performs one or more restarts.

### Claim 32 (depends on 31)

The method of claim 31 in which a new iteration based upon the one or more restarts uses a last point reached in a previous iteration as an initial point.

### Claim 33 (depends on 31)

The method of claim 31 in which a restart is performed if a threshold value is exceeded.

### Claim 34 (depends on 22)

The method of claim 22 in which the SAT-solver does not perform a restart.

### Claim 35

A system for implementing an integrated circuit design, comprising:
means for identifying an integrated circuit design to operate upon with an electronic design automation tool, the electronic design automation tool comprising a SAT-solver mechanism;
means for converting the integrated circuit design into a formula for which Boolean satisfiability is addressed by the SAT-solver mechanism;
means for solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment; and
means for generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable.

### Claim 36 (depends on 35)

The system of claim 35 in which a variable x of a current complete assignment is fixed.

### Claim 37 (depends on 35)

The system of claim 35 in which the system is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 38 (depends on 35)

The system of claim 35 in which a system local search is performed.

### Claim 39

A computer program product that includes a computer readable medium, the computer readable medium comprising a plurality of computer instructions which, when executed by a processor, cause the processor to execute performing a method for implementing an integrated circuit design, the process comprising:
identifying an integrated circuit design to operate upon with an electronic design automation tool, the electronic design automation tool comprising a SAT-solver mechanism;
converting the integrated circuit design into a formula for which Boolean satisfiability is addressed by the SAT-solver mechanism;
solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment; and
generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable.

### Claim 40 (depends on 39)

The computer program product of claim 39 in which a variable x of a current complete assignment is fixed.

### Claim 41 (depends on 39)

The computer program product of claim 39 in which the electronic design automation tool is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 42 (depends on 39)

The computer program product of claim 39 in which a system local search is performed.

### Claim 43

A system for operating a SAT-solver, comprising:
means for receiving a formula for which Boolean satisfiability is to be addressed; and
means for solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment; and
means for generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable.

### Claim 44 (depends on 43)

The system of claim 43 in which a variable x of a current complete assignment is fixed.

### Claim 45 (depends on 43)

The system of claim 43 in which the system is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 46 (depends on 43)

The system of claim 43 in which a system local search is performed.

### Claim 47

A computer program product that includes a computer readable medium, the computer readable medium comprising a plurality of computer instructions which, when executed by a processor, cause the processor to execute performing a method for operating a SAT-solver, the process comprising:
receiving a formula for which Boolean satisfiability is to be addressed;
solving the Boolean satisfiability using complete assignments, wherein Boolean constraint propagation is performed to solve the Boolean satisfiability, the Boolean constraint propagation fixing variables and making a decision assignment fixing a variable at a value satisfying an active literal, where literal activity is computed based on conflict clauses and the variable to be assigned is chosen from clauses falsified by the current complete assignment; and
generating a conflict clause for the formula if a conflict occurs, wherein a determination is made whether the conflict clause is empty or not empty, and where upon determining that the conflict clause is not empty returning to an earlier fixed variable and unfixing the earlier fixed variable as well as unfixing assignments made after the earlier fixed variable.

### Claim 48 (depends on 47)

The computer program product of claim 47 in which a variable x of a current complete assignment is fixed.

### Claim 49 (depends on 47)

The computer program product of claim 47 in which the process is performing synthesis, automatic test pattern generation (ATPG), verification, or simulation for the integrated circuit design.

### Claim 50 (depends on 47)

The computer program product of claim 47 in which a system local search is performed.