Invention Grant
US07742907B2 Iterative abstraction using SAT-based BMC with proof analysis
失效
使用基于SAT的BMC进行迭代抽象与证明分析
- Patent Title: Iterative abstraction using SAT-based BMC with proof analysis
- Patent Title (中): 使用基于SAT的BMC进行迭代抽象与证明分析
-
Application No.: US10762499Application Date: 2004-01-23
-
Publication No.: US07742907B2Publication Date: 2010-06-22
- Inventor: Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar
- Applicant: Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar
- Applicant Address: US NJ Princeton
- Assignee: NEC Laboratories America, Inc.
- Current Assignee: NEC Laboratories America, Inc.
- Current Assignee Address: US NJ Princeton
- Agent Joseph J. Kolodka
- Main IPC: G06F17/50
- IPC: G06F17/50 ; G06F9/45
Abstract:
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.
Public/Granted literature
- US20040230407A1 Iterative abstraction using SAT-based BMC with proof analysis Public/Granted day:2004-11-18
Information query
