Dynamic detection and removal of inactive clauses in SAT with application in image computation
US6496961B2 · kind B2 · utility
32Cited by
2References
13Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Jun 15, 2001 |
| Grant date | Dec 17, 2002 |
| Priority date | — |
| Expiry date | Jun 15, 2021 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldMeasurement
- WIPO sectorInstruments
Abstract
This disclosure teaches a method of Boolean satisfiability checking (SAT) for a circuit. The method comprises identifying inactive clauses in the conjunctive normal form (CNF) of the circuit and removing the inactive clauses from the CNF.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.