Method and system for non-linear state based satisfiability

• US 6,912,700 B1
• Filed: 06/06/2002
• Issued: 06/28/2005
• Est. Priority Date: 06/06/2001
• Status: Expired due to Fees

• Current Assignee: National Security Agency, University of Cincinnati
• Original Assignee: The United States of America As Represented By The Director National Security Agency, University of Cincinnati
• Inventors: Franco, John V., Schlipf, John, Dransfield, Michael R., VanFleet, W. Mark
• Primary Examiner(s): Smith, Matthew
• Assistant Examiner(s): Kik, Phallaka
• Application Number:
  US10/164,203
• Time in Patent Office: 1,118 Days
• Field of Search: 716/5, 716/2, 716/3, 716/7, 716/18, 703/16, 706/13, 706/16, 706/33, 706/45
• US Class Current: 716/103
• CPC Class Codes: G06F 17/11 for solving equations , e.g. nonlinear equations, general mathematical optimization problems optimization specially adapted for a specific administrative, business or logistic context G06Q10/04
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A computerized method and system for solving non-linear Boolean equations is disclosed comprising at least partially solving a Boolean function; developing at least one inference regarding said Boolean function and saving said inference to a state machine; and accessing said inference from said state machine to develop at least one heuristic for determining whether said Boolean function is satisfiable.

Claims

1. A computerized method for utilizing at least one state machine to solve a non-linear Boolean equation comprising:

partially solving said non-linear Boolean equation to determine at least one pre-computed search inference relating to said non-linear Boolean equation;

storing at least one precomputed search inference relating to said Boolean equation in said at least one state machine;

accessing said at least one search inference from said state machine to develop at least one heuristic for solving said non-linear Boolean equation;

iteratively searching for a solution to said equation by utilizing at least one heuristic developed from said at least one inference stored in said state machine.

2. A method as claimed in claim 1 wherein said non-linear Boolean equation is translated into a set of functions and wherein said functions are represented in a Binary Decision Diagram and further wherein said partial solving step comprises solving each function in said set of functions for all possible inputs.

3. A method as claimed in claim 1 further including the steps of computing a score for each of said at least one inference wherein said score is stored and associated with said at least one inference and wherein said score indicates a desirability of using said associated inference in said determining step.

4. A method as claimed in claim 3 wherein a set of heuristics is developed from said at least one inference in an order according to said score associated with said at least one inference.

5. A method as claimed in claim 1 wherein said state machine comprises at least one inference for a user domain relating to said non-linear Boolean equation.

6. A method as claimed in claim 5 wherein said state machine further comprises a computer readable data storage location for storing any linear inferences developed in said partial solving step.

7. A method as claimed in claim 1 wherein said state machine utilizes a technique selected from a group of autarkies, lemmas, and/or pruning to reduce a set of inferences associated with a user domain associated with said non-linear Boolean function.

8. A computerized method for verifying that a circuit expression for a microprocessor matches a specification associated with said microprocessor comprising:

transforming said specification into a conjunction of logical expressions;

combining said conjunction with said circuit expression to produce a verification equation;

analyzing said verification equation via a Binary Decision Diagram;

partitioning said verification equation into a set of functions representing said verification equation;

processing each function in said set of functions for all possible inputs;

storing at least one inference developed from said processing step in a state machine;

iteratively searching for a solution to said equation by utilizing at least one heuristic developed from said at least one inference stored in said state machine.

9. A method as claimed in 8 wherein said searching step does not comprise translating said equation into Conjunctive Normal Format.

10. A computer system for solving a non-linear Boolean equation comprising a pre-processor, a state machine and a search engine wherein

A. said pre-processor is configured to perform the steps of translating said Boolean equation into a set of functions;

2. solving said set of functions for all possible inputs;

B. said state machine is configured to store a set of at least one inferences developed from said solving step wherein said inferences are associated with a respective function in said set of functions;

C. a search engine configured to search for a solution to said Boolean equation using a set of heuristics developed from said set of inferences.