Rendered at 07:04:56 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
nigardev 3 days ago [-]
sos decompositions are elegant but the search is exp-time-complete. how do you prune the search space in practice? also, how does the python backend communicate with lean - pipe through or something else
mmaaz 12 hours ago [-]
great q! there's a variety of levers here. for one, it uses newton polytope pruning to prune the monomial basis -- this often helps a lot in practice, especially for sparse polynomials. also, both the lean and python interfaces allow to pass degree bounds in the case of a ratio of SOS, as well as a template for the denominator (e.g., ax^2 + ay^2), which also cuts down on the monomials, as well as possibly introducing affine constraints tying coefficients together. of course, in the positivstellensatz case, you can also specify the degree bound.
I wrote about all these tricks here https://mmaaz.ca/writings/sostactic.html.
and yeah, there is a clli interface for the python backend, the lean interface calls the cli.