发明名称 |
Integrating interval constraint propagation with nonlinear real arithmetic |
摘要 |
A system and method for deciding the satisfiability of a non-linear real decision problem is disclosed. Linear and non-linear constraints associated with the problem are separated. The feasibility of the linear constraints is determined using a linear solver. The feasibility of the non-linear constraints is determined using a non-linear solver which employs interval constraint propagation. The interval solutions obtained from the non-linear solver are validated using the linear solver. If the solutions cannot be validated, linear constraints are learned to refine a search space associated with the problem. The learned constraints and the non-linear constraints are iteratively solved using the non-linear solver until either a feasible solution is obtained or no solution is possible.
|
申请公布号 |
US8538900(B2) |
申请公布日期 |
2013.09.17 |
申请号 |
US20100966710 |
申请日期 |
2010.12.13 |
申请人 |
GANAI MALAY K.;GAO SICUN;IVANCIC FRANJO;GUPTA AARTI;NEC LABORATORIES AMERICA, INC. |
发明人 |
GANAI MALAY K.;GAO SICUN;IVANCIC FRANJO;GUPTA AARTI |
分类号 |
G06F15/18;G06F7/60 |
主分类号 |
G06F15/18 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|