发明名称 |
TEMPLATE CLAUSES BASED SAT TECHNIQUES |
摘要 |
A CNF formula comprises at least one template clause representing a set of concrete clauses, each associated with a different temporal shift. The template clause is utilized by a SAT solver in determining satisfiability of the CNF formula. The template clause may be utilized to reduce amount of storage resources required for performing the satisfiability analysis. The template clause may in some cases increase feasibility of determining satisfiability. The template clause may in some cases reduce required time to determine satisfiability. The template clause may be utilized in incremental SAT solving to reuse deduced relations between literals that are applicable to additional cycles, such as invariants originating from a transition relation of a model.
|
申请公布号 |
US2011178970(A1) |
申请公布日期 |
2011.07.21 |
申请号 |
US20100689247 |
申请日期 |
2010.01.19 |
申请人 |
INTERNATIONAL BUSINESS MACHINES CORPORATION |
发明人 |
FUHRMANN ODED;SHACHAM OHAD |
分类号 |
G06N5/02 |
主分类号 |
G06N5/02 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|