Method, apparatus and product for SAT solving using templates clauses
US8407175B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 19, 2010 |
| Grant date | Mar 26, 2013 |
| Priority date | — |
| Expiry date | Mar 15, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/04
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method to solve a template SAT problem associated with a bounded model that is modeled checked, said method comprising: receiving the template SAT problem, the template SAT problem comprising a plurality of clauses including a template clause that represents a plurality of concrete clauses each associated with a different temporal shift, the template clause is associated with a literal; determining a value of the literal in a cycle based on the template clause and a temporal shift, said determining comprises: determining a concrete clause of the plurality of concrete clauses based on the template clause and the temporal shift; determining a new template clause based on at least two clauses; determining a deduced clause based on at least the value of the literal in the cycle; deducing a solution to the template SAT problem; and outputting the solution.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.