Relevancy propagation for efficient theory combination
US8140459B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Feb 21, 2008 |
| Grant date | Mar 20, 2012 |
| Priority date | — |
| Expiry date | Jun 1, 2030 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/02
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Relevancy propagation for efficient theory combination is described. In one implementation, an efficient SMT solver dynamically applies relevancy propagation to limit propagation of unnecessary constraints in a DPLL-based solver. This provides a drastic increase in speed and performance over conventional DPLL-based solvers. The relevancy propagation is guided by relevancy rules, which in one implementation emulate Tableau rules for limiting constraint propagation, while maintaining the performance of efficient DPLL-based solvers. An exemplary solver propagates truth assignments to constraints of a formula, and tracks which truth assignments are relevant for determining satisfiability of the formula. The solver propagates truth assignments that were marked relevant to a theory solver, while avoiding propagation of irrelevant truth assignments. The efficient SMT solver provides a drastic reduction in search space covered during quantifier instantiation and offers profound acceleration during bit-vectors reasoning.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.