Template clauses based SAT techniques
US9646252B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Feb 14, 2013 |
| Grant date | May 9, 2017 |
| Priority date | — |
| Expiry date | Mar 21, 2035 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/04
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A CNF formula comprises at least one template clause representing a set of concrete clauses, each associated with a different temporal shift. The template clause is utilized by a SAT solver in determining satisfiability of the CNF formula. The template clause may be utilized to reduce amount of storage resources required for performing the satisfiability analysis. The template clause may in some cases increase feasibility of determining satisfiability. The template clause may in some cases reduce required time to determine satisfiability. The template clause may be utilized in incremental SAT solving to reuse deduced relations between literals that are applicable to additional cycles, such as invariants originating from a transition relation of a model.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.