|
From: John H. <Joh...@cl...> - 2006-07-20 23:31:27
|
Hi Steve, | The attached file gives two examples where including two algebraically | equivalent hypotheses causes REAL_SOS to hang. When you encounter strange behaviour in the SOS procedures, you may find it helpful to set: debugging := true;; Then you'll be able to see roughly where things are going wrong. In the two cases you cite, the SDP solver appears to solve the problem quite effectively at a moderate depth. ... Iter: 23 Ap: 1.00e+00 Pobj: 4.8441239e+05 Ad: 9.40e-01 Dobj: 4.8441243e+05 Iter: 24 Ap: 8.40e-01 Pobj: 4.8441239e+05 Ad: 9.54e-01 Dobj: 4.8441240e+05 Success: SDP solved Primal objective value: 4.8441239e+05 Dual objective value: 4.8441240e+05 Relative primal infeasibility: 6.18e-15 Relative dual infeasibility: 1.45e-10 Real Relative Gap: 1.93e-09 XZ Relative Gap: 2.24e-09 DIMACS error measures: 2.02e-14 0.00e+00 1.45e-10 0.00e+00 1.93e-09 2.24e-09 The problem comes later when HOL Light tries to round the floating-point vector returned by the SDP solver to rational numbers that make the necessary algebraic identity work exactly, not just approximately: Trying rounding with limit 1 Trying rounding with limit 2 Trying rounding with limit 3 Trying rounding with limit 4 Trying rounding with limit 5 Trying rounding with limit 6 Trying rounding with limit 7 Trying rounding with limit 8 Trying rounding with limit 9 Trying rounding with limit 10 Trying rounding with limit 11 Trying rounding with limit 12 ... None of the attempted roundings work, and so HOL Light just tries a larger depth limit for the overall process. This doesn't help; indeed it almost never does, so maybe I should make it just stop when rounding fails. The same thing keeps happening at larger and larger depth limits, and so one effectively has an infinite loop. (Though since each iteration needs more memory for the matrices, it should in theory run out of memory eventually.) | Is this problem because of something subtle in how REAL_SOS is implemented, | or is it just an old-fashioned bug? Essentially the former. It's not really easy to understand in a particular case where the numerical issues arise. I have long wanted to explore more intelligent approaches to rounding, but it's not entirely a trivial problem. For example, even if you know that one corner of a given unit hypercube will work, that doesn't help much when the dimension is 100. | In either case, how can I program to avoid it? I'm afraid I can't offer any especially satisfying answer. All the SOS stuff is still a prototype and experimental; dealing with its various shortcomings is a (very interesting) research project rather than merely a programming exercise. I expect I'll have the time and inclination to do more work on it myself one day, but don't hold your breath. John. |