发明授权
US07742907B2 Iterative abstraction using SAT-based BMC with proof analysis
失效
使用基于SAT的BMC进行迭代抽象与证明分析
- 专利标题： Iterative abstraction using SAT-based BMC with proof analysis
- 专利标题（中）： 使用基于SAT的BMC进行迭代抽象与证明分析
-
申请号： US10762499申请日： 2004-01-23
-
公开(公告)号： US07742907B2公开(公告)日： 2010-06-22
- 发明人: Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar
- 申请人： Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar
- 申请人地址： US NJ Princeton
- 专利权人： NEC Laboratories America, Inc.
- 当前专利权人： NEC Laboratories America, Inc.
- 当前专利权人地址： US NJ Princeton
- 代理商 Joseph J. Kolodka
- 主分类号： G06F17/50
- IPC分类号： G06F17/50 ; G06F9/45
摘要：
A method of obtaining a resolution-based proof of unsatisfiability using a SAT procedure for a hybrid Boolean constraint problem comprising representing constraints as a combination of clauses and interconnected gates. The proof is obtained as a combination of clauses, circuit gates and gate connectivity constraints sufficient for unsatisfiability.
公开/授权文献
信息查询
