1. A method for deciding the satisfiability of a non-linear real decision problem, comprising: generating a Boolean abstraction of non-Boolean constraints for the problem by determining symbolic bounds on real variables set forth in the problem; separating linear and non-linear constraints; determining feasibility of linear constraints using a simplex-based linear solver; if the linear constraints are feasible, determining feasibility of non-linear constraints using a non-linear solver which employs interval constraint propagation (ICP); and validating solution boxes obtained from the non-linear solver using the simplex-based linear solver; learning at least one linear constraint for each solution box that is determined infeasible; repeating said step of determining feasibility of non-linear constraints using the non-linear constraints and the learned constraints; and refining the Boolean abstraction by adding a theory lemma if the solution boxes cannot be validated.