Case Number 101002 - State Based Propositional Satisfiability Solver
Contact: Geoffrey Pinski
Description: In many computer related fields, such as the design of Very Large Scale Integrated Circuits, computer programs are used to solve crucial problems such as determining whether a given circuit design meets precise specifications. Since the magnitude of such problems is increasing at an enormous rate, current software is rapidly becoming incapable of meeting industrial needs. More alarming, future software will be inadequate without breakthroughs in the design of algorithms for certain computationally intensive problems.
One of those problems, called CSP, is to determine whether some set of input values to a collection of Boolean functions will cause those functions to evaluate to a particular given set of output values. Current methods for solving such problems are either based on Binary Decision Diagrams (BDDs) or search-based Solvers (SAT). Both methods have advantages and drawbacks. BDDs can be combined easily and eliminate duplicate and redundant substructures but must be completely constructed before results can be obtained and their ultimate size may be impractical to achieve. SAT search structures may be much smaller than BDD structures and only need to be partially built in many cases but the building process is much slower, typically, than for BDDs.
The subject matter of the proposed patent is a methodology for solving CSP problems using a combination of BDD and SAT techniques. The methodology constructs a state-based structure, obtained by considering every BDD for every Boolean function, assigns values to the states of the structure during an extensive precomputation phase, and uses this information to guide a SAT search.
The key benefit of the discovery is to retain the advantages of SAT search techniques but drastically speed up and make more effective the building process.
1. Some problems, currently requiring days or weeks to solve using conventional methods, will be solved in a reasonable amount of time using the discovery. This will allow faster turn-around in the design and verification of integrated circuits. The result is a reduction in design costs.
2. An emerging class of problems which admits amortization of pre-processing costs over many runs with different input will be effectively solved by the new methodology.
Two Issued US patents - 6,912,700 & 7,380,224