Re: [Hol-info] Another REAL_SOS "gotcha"

[John H. <Joh...@cl...>]

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.