Patent Document ID: 7610570
Application ID: 11407864
Patent Flag: 1

Claim One:
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.