MathProgBase interface

[mlubin]

Very cool to see this hooked up through MathProgBase. I'm not familiar at all with SMT solvers, could you explain or point me to a reference on which classes of problems DReal can solve? Can it solve nonconvex problems to a global optimum?

Also, let us know of any difficulties you've had with the MathProgBase interface and if there are structures which you'd like to communicate which aren't currently supported. I'm guessing that the boolean logic aspect is missing.

CC @IainNZ @joehuchette @tkelman

[IainNZ]

I was just talking to @jakebolewski at lunch about SMT, really cool to see this. My understanding is limited too, I didn't realize they could do nonlinear math on reals until I saw this.

[zenna]

It can solve a slightly relaxed version of your problem to a global minimum. Your problem can be an arbitrary boolean combination of arbitrary nonlinear functions, both continuous and discontinuous. DReal is a satisfiability solver. You can (and we do) view optimization as a satisfiability problem.

That is, an optimisation problem has the form does there exist some x such that forall y f(x) <= f(y). You could literally write that as a program in DReal, e.g:

using DReal

f(x) = x^2+cos(x)
x = Var(Float64)
y = ForallVar(Float64)
add!(f(x) <= f(y))
is_satisfiable()
optimal_sol = model(x)

There are a few other ways to do it. If you use the minimize function, currently that solves it by asking a series of satisfiability problems, basically doing a binary bisection search in the cost space.

As @IainNZ just said, most SMT solvers are linear, we are working on nonlinear solving.

One other difference is that the constraints you can compose are much more general than you normally think of in constrained optimization.

Of course this is all in principle, performance will depend on the problem, and there are surely many bugs :-).

[tkelman]

This is very cool indeed. Are you translating from MathProgBase format into the standard SMT-LIB format that Z3 and Gecode could also use? Extending the MPB nonlinear API to include logical constraints, then teaching JuMP or an extension to handle them probably wouldn't be too hard.

[zenna]

No I'm using the DReal c-api. I get the expression using obj_expr and just evaluate it using DReal replacing all the variables in the expression with DReal vars.

https://github.com/dreal/DReal.jl/blob/master/src/SolverInterface.jl#L94

[scungao]

Hi All,

Thanks a lot for your interest. Indeed, SMT with nonlinear real constraints is relatively new. To solve these formulas in general one needs to work in the framework of delta-decision procedures (http://arxiv.org/abs/1204.3513), which basically allows one to deal with numerical errors in a logically rigorous way. Our solver dReal (http://dreal.github.io/) implements algorithms in this framework and have been used to solve quite some difficult problems (for instance, constraints mixing differential equations and logic). Some published applications are:

http://dl.acm.org/citation.cfm?doid=2562059.2562139 http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9457 http://dl.acm.org/citation.cfm?doid=2728606.2728609 http://dl.acm.org/citation.cfm?doid=2728606.2728625 http://dl.acm.org/citation.cfm?doid=2728606.2728634

The optimization solver is an on-going work right now and we'd love to hear feedbacks.

On Fri, Jul 10, 2015 at 1:03 AM, Zenna Tavares notifications@github.com wrote:

No I'm using the DReal c-api. I get the expression using obj_expr and just evaluate it using DReal replacing all the variables in the expression with DReal vars.

https://github.com/dreal/DReal.jl/blob/master/src/SolverInterface.jl#L94

— Reply to this email directly or view it on GitHub https://github.com/dreal/DReal.jl/issues/12#issuecomment-120227212.