SAT-based image computation with application in reachability analysis
US6728665B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Oct 23, 2000 |
| Grant date | Apr 27, 2004 |
| Priority date | — |
| Expiry date | Aug 14, 2022 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method of performing image or pre-image computation for a system is disclosed. The method comprises representing the system by a finite state model; representing state sets using Binary Decision Diagrams (BDDs); performing a satisfiabilty checking (SAT) based backtrack search algorithm, wherein, the SAT decomposes the search over an entire solution space into multiple sub-problems, and wherein a BDD-based image computation is used to solve each sub-problem by enumerating multiple solutions from the solution space. Further, a method for pruning a search space in a SAT procedure is disclosed. The method comprises using BDD Bounding against an implicit disjunction or conjunction of a given set of BDDs; continuing search if a partial assignment of variables satisfies the implicit disjunction or conjunction, and backtracking if a partial assignment of variables does not satisfy the implicit disjunction or conjunction.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.