University of Cincinnati
PO Box 210829 Cincinnati, OH 452210829 Overnight Mail Address: 51 Goodman Dr., Suite 240 Cincinnati, OH 45219 

Case Number 101002  State Based Propositional Satisfiability SolverContact: Geoffrey PinskiEmail: pinskig@ucmail.uc.edu Phone: 5135585696  
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 searchbased 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 statebased 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. Advantages 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 turnaround 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 preprocessing 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 For more information please contact Geoffrey Pinski at 5135585696 or pinskig@ucmail.uc.edu 