Back to results
US 7,249,333 B2Granted
Quantified boolean formula (QBF) solver
AssigneeMicrosoft Corporation
InventorsYuan Yu, Lintao Zhang
Life of this patent
Estimating the term…
Loading patent…
Loading patent…
AssigneeMicrosoft Corporation
InventorsYuan Yu, Lintao Zhang
Estimating the term…
Quantified Boolean formula (QBF) techniques are used in determining QBF satisfiability. A QBF is broken into component parts that are analyzable by a satisfiability (SAT) solver. Each component is then independently, and perhaps in parallel, analyzed for satisfiability. If a component is unsatisfiable, then it is determined that the QBF is unsatisfiable, and the analysis is stopped. If a component is satisfiable, then an assignment corresponding to the satisfiable component is noted. If a component is satisfiable, then it is appended to another untested component to provide a combination component, and the satisfiability of the combination component is analyzed. Such appending and analysis is repeated until the QBF is completed and determined to be satisfiable or determined to be unsatisfiable.
A method of solving a quantified Boolean formula (QBF), comprising:
A computer-implemented quantified Boolean formula (QBF) solver system, comprising:
A computer readable medium having stored thereon computer executable instructions for performing a method of solving a quantified Boolean formula (QBF), the method comprising:
Dependencies are inferred from the claim text.