发明名称 |
Applying CNF simplification techniques for SAT-based abstraction refinement |
摘要 |
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.
|
申请公布号 |
US7441216(B1) |
申请公布日期 |
2008.10.21 |
申请号 |
US20080060260 |
申请日期 |
2008.03.31 |
申请人 |
INTERNATIONAL BUSINESS MACHINES CORPORATION |
发明人 |
SHACHAM OHAD;BAR-ILAN OMER;FUHRMANN ODED |
分类号 |
G06F17/50 |
主分类号 |
G06F17/50 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|