Partition-based decision heuristics for SAT and image computation using SAT and BDDs
US6651234B2 · kind B2 · utility
32Cited by
3References
27Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Nov 1, 2001 |
| Grant date | Nov 18, 2003 |
| Priority date | — |
| Expiry date | Nov 1, 2021 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for Boolean Satisfiability (SAT). The method comprises using a variable decision heuristic in a SAT algorithm and pruning the search space of SAT using said decision heuristic. The decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and the partitioning is induced by a separator set. An image computaion method that uses the disclosed method for solving the SAT.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.