Iterative abstraction using SAT-based BMC with proof analysis
US7742907B2 · kind B2 · utility
15Cited by
4References
7Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Jan 23, 2004 |
| Grant date | Jun 22, 2010 |
| Priority date | — |
| Expiry date | May 14, 2026 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method of obtaining a resolution-based proof of unsatisfiability using a SAT procedure for a hybrid Boolean constraint problem comprising representing constraints as a combination of clauses and interconnected gates. The proof is obtained as a combination of clauses, circuit gates and gate connectivity constraints sufficient for unsatisfiability.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.