Applying CNF simplification techniques for SAT-based abstraction refinement
US7519931B1 · kind B1 · utility
1Cited by
1References
1Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Oct 13, 2008 |
| Grant date | Apr 14, 2009 |
| Priority date | — |
| Expiry date | Oct 13, 2028 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
The present embodiment keeps track of a set of resolution required for generating each one of the clauses added by the simplification Method. This information is used by the method that generates the unsat core in order to extract the original clauses that generated the simplified clauses. This work integrates resolution based CNF simplification technique inside the SAT-based abstraction refinement scheme in a unique way that overcomes the difficulties.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.