Method and mechanism for using systematic local search for SAT solving

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.

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.

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.

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.

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.