Verifying models and optima

[FilippoBiga]

Hi!

I have a series of optimization problems for which I would like to check (with an external solver) the correctness of both the models and the optima produced by dReal. However, as far as I understand, dReal provides the guarantee that any point in the bounding box satisfies the delta-weakened version of the formula, and not the formula itself, so simply forcing the assignments to either the lower or upper bounds in the bounding box would be incorrect.

What is the best way to check the models and optima, starting from the model (bounding box) produced by dReal as output, without any inherent knowledge of the formula itself (this has to be done for thousands of instances)?

[scungao]

Hi,

Note that precisely checking the optima without any error is an undecidable problem (think about checking whether an expression for computing pi is exactly pi), so the delta-weakened guarantee is pretty much the most you can hope for in general, unless there are special structures (local convexity etc) in your models.

[FilippoBiga]

Thank you for your answer. Yes, I do understand that exact checking is an undecidable problem, and unfortunately I did not explain clearly what I meant by checking the optima. With other exact solvers, once they produce an optimum, I can check the optimality guarantee they provide by verifying whether forcing an inequality constraint ((assert (< objective value_obtained)), in the case of (minimize objective)) makes the problem unsatisfiable. Is there any way for me to perform the same kind of verification with dReal, with regards to the original formula, and not the delta-weakened version?

Same goes for the model. Starting from the bounding box produced by dReal, how do I verify that the assignment is correct within the bounds provided, with regards to the original formula?

Thank you in advance!

[scungao]

You can check optimality of the solution using the assertion that you mentioned, and expect an unsat result over the domain. If you get unsat, then the guarantee is on the original unperturbed formula. But it’s also possible that you get delta-sat. So your best bet is to numerically-strengthen the solution and check (e.g. for minimization, check the result minus some epsilon is globally less than all values of the function).

For the solutions in a box, no matter how small the box is finding a solution is as hard as the general problem (undecidable).

On Oct 1, 2019, at 00:26, Filippo Bigarella notifications@github.com wrote:

Thank you for your answer. Yes, I do understand that exact checking is an undecidable problem, and unfortunately I did not explain clearly what I meant by checking the optima. With other exact solvers, once they produce an optimum, I can check the optimality guarantee they provide by verifying whether forcing an inequality constraint ((assert (< objective value_obtained))) makes the problem unsatisfiable. Is there any way for me to perform the same kind of verification with dReal, with regards to the original formula, and not the delta-weakened version?

Same goes for the model. Starting from the bounding box produced by dReal, how do I verify that the assignment is correct within the bounds provided, with regards to the original formula?

Thank you in advance!

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[FilippoBiga]

I do have another question, which is related to the aforementioned situation: I cannot understand the result produced by dreal on the following smt2 code:

(set-info :smt-lib-version |2.6|)
(set-logic QF_NRA)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(declare-fun v7 () Real)
(declare-fun v8 () Real)
(declare-fun v9 () Real)
(declare-fun v10 () Real)
(declare-fun v11 () Real)
(declare-fun v12 () Real)
(assert (and (= (* v2 v5) 0.0) (= (* v1 v9) v5) (< 0.0 v2) (< 0.0 v1) (<= 0.0 v3) (<= 0.0 v7) (<= 0.0 v10) (<= 0.0 v12) (<= (* v4 v4) (* v3 v7)) (<= (* v5 v5) (* v10 v3)) (<= (* v6 v6) (* v12 v3)) (<= (* v8 v8) (* v10 v7)) (<= (* v9 v9) (* v12 v7)) (<= (* v11 v11) (* v10 v12)) (<= (+ (* v10 (* v4 v4)) (* (* v5 v5) v7) (* v3 (* v8 v8))) (+ (* v10 v3 v7) (* 2.0 v4 v5 v8))) (<= (+ (* v12 (* v4 v4)) (* (* v6 v6) v7) (* v3 (* v9 v9))) (+ (* v12 v3 v7) (* 2.0 v4 v6 v9))) (<= (+ (* (* v11 v11) v3) (* v12 (* v5 v5)) (* v10 (* v6 v6))) (+ (* v10 v12 v3) (* 2.0 v11 v5 v6))) (<= (+ (* (* v11 v11) v7) (* v12 (* v8 v8)) (* v10 (* v9 v9))) (+ (* v10 v12 v7) (* 2.0 v11 v8 v9))) (<= (+ (* v10 v12 (* v4 v4)) (* (* v11 v11) v3 v7) (* v12 (* v5 v5) v7) (* v10 (* v6 v6) v7) (* 2.0 v11 v4 v6 v8) (* v12 v3 (* v8 v8)) (* 2.0 v11 v4 v5 v9) (* 2.0 v5 v6 v8 v9) (* v10 v3 (* v9 v9))) (+ (* (* v11 v11) (* v4 v4)) (* v10 v12 v3 v7) (* 2.0 v11 v5 v6 v7) (* 2.0 v12 v4 v5 v8) (* (* v6 v6) (* v8 v8)) (* 2.0 v10 v4 v6 v9) (* 2.0 v11 v3 v8 v9) (* (* v5 v5) (* v9 v9))))))
(minimize v6)
(check-sat)
(exit)

As we can see, the objective function here is (minimize v6). However, when executed with the following parameters: ``, the following output is produced by dreal:

delta-sat with delta = 0.001
v1 : [1.797693134862315708e+308, 1.797693134862315708e+308]
v2 : [1.797693134862315708e+308, 1.797693134862315708e+308]
v3 : [8.426686569667105817e+306, 8.426686569667105817e+306]
v4 : [1.376358806378960218e+308, 1.376358806378960218e+308]
v5 : [0, 0]
v6 : [4.213343284833553907e+307, 4.213343284833553907e+307]
v7 : [1.797693134862315708e+308, 1.797693134862315708e+308]
v8 : [-4.213343284833553907e+307, -4.213343284833553907e+307]
v9 : [0, 0]
v10 : [4.213343284833553907e+307, 4.213343284833553907e+307]
v11 : [1.71342626916564445e+308, 1.71342626916564445e+308]
v12 : [1.797693134862315708e+308, 1.797693134862315708e+308]

However, the value for v6 has clearly not been minimized: we can check this by asking any other SMT solver the satisfiability of the aforementioned problem, by imposing the assignment of v6 to 0:

(set-info :smt-lib-version |2.6|)
(set-logic QF_NRA)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(declare-fun v7 () Real)
(declare-fun v8 () Real)
(declare-fun v9 () Real)
(declare-fun v10 () Real)
(declare-fun v11 () Real)
(declare-fun v12 () Real)
(assert (and (= (* v2 v5) 0.0) (= (* v1 v9) v5) (< 0.0 v2) (< 0.0 v1) (<= 0.0 v3) (<= 0.0 v7) (<= 0.0 v10) (<= 0.0 v12) (<= (* v4 v4) (* v3 v7)) (<= (* v5 v5) (* v10 v3)) (<= (* v6 v6) (* v12 v3)) (<= (* v8 v8) (* v10 v7)) (<= (* v9 v9) (* v12 v7)) (<= (* v11 v11) (* v10 v12)) (<= (+ (* v10 (* v4 v4)) (* (* v5 v5) v7) (* v3 (* v8 v8))) (+ (* v10 v3 v7) (* 2.0 v4 v5 v8))) (<= (+ (* v12 (* v4 v4)) (* (* v6 v6) v7) (* v3 (* v9 v9))) (+ (* v12 v3 v7) (* 2.0 v4 v6 v9))) (<= (+ (* (* v11 v11) v3) (* v12 (* v5 v5)) (* v10 (* v6 v6))) (+ (* v10 v12 v3) (* 2.0 v11 v5 v6))) (<= (+ (* (* v11 v11) v7) (* v12 (* v8 v8)) (* v10 (* v9 v9))) (+ (* v10 v12 v7) (* 2.0 v11 v8 v9))) (<= (+ (* v10 v12 (* v4 v4)) (* (* v11 v11) v3 v7) (* v12 (* v5 v5) v7) (* v10 (* v6 v6) v7) (* 2.0 v11 v4 v6 v8) (* v12 v3 (* v8 v8)) (* 2.0 v11 v4 v5 v9) (* 2.0 v5 v6 v8 v9) (* v10 v3 (* v9 v9))) (+ (* (* v11 v11) (* v4 v4)) (* v10 v12 v3 v7) (* 2.0 v11 v5 v6 v7) (* 2.0 v12 v4 v5 v8) (* (* v6 v6) (* v8 v8)) (* 2.0 v10 v4 v6 v9) (* 2.0 v11 v3 v8 v9) (* (* v5 v5) (* v9 v9))))))
(assert (= v6 0))
(check-sat)
(exit)

This is correctly reported as sat by MathSAT, Z3 and CVC4. Am I misinterpreting dreal's results? What is the right way to make dreal produce the correct value for the objective function, if we should not make assumptions on the values included in the model?

[soonho-tri]

@FilippoBiga , I am investigating #154 which shows a similar problem in handling optimization problems. I'll get back to you later.

[soonho-tri]

@FilippoBiga , please check my comment, https://github.com/dreal/dreal4/issues/154#issuecomment-663894782 and subscribe #122 if you want to get updates on this matter.