TY - GEN
T1 - Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems
AU - Gao, Sicun
AU - Ganai, Malay
AU - Ivančić, Franjo
AU - Gupta, Aarti
AU - Sankaranarayanan, Sriram
AU - Clarke, Edmund M.
PY - 2010
Y1 - 2010
N2 - We propose a novel integration of interval constraint propagation (ICP) with SMT solvers for linear real arithmetic (LRA) to decide nonlinear real arithmetic problems. We use ICP to search for interval solutions of the nonlinear constraints, and use the LRA solver to either validate the solutions or provide constraints to incrementally refine the search space for ICP. This serves the goal of separating the linear and nonlinear solving stages, and we show that the proposed methods preserve the correctness guarantees of ICP. Experimental results show that such separation is useful for enhancing efficiency.
AB - We propose a novel integration of interval constraint propagation (ICP) with SMT solvers for linear real arithmetic (LRA) to decide nonlinear real arithmetic problems. We use ICP to search for interval solutions of the nonlinear constraints, and use the LRA solver to either validate the solutions or provide constraints to incrementally refine the search space for ICP. This serves the goal of separating the linear and nonlinear solving stages, and we show that the proposed methods preserve the correctness guarantees of ICP. Experimental results show that such separation is useful for enhancing efficiency.
UR - http://www.scopus.com/inward/record.url?scp=79958759616&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79958759616&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:79958759616
SN - 9780983567806
T3 - Formal Methods in Computer Aided Design, FMCAD 2010
SP - 81
EP - 89
BT - Formal Methods in Computer Aided Design, FMCAD 2010
T2 - Formal Methods in Computer Aided Design, FMCAD 2010
Y2 - 20 October 2010 through 23 October 2010
ER -