Stream: Coq users

Topic: psatz and coinor-csdp

Pierre Roux (Jan 15 2021 at 10:43):

Paolo Giarrusso said:

a colleague noticed that even the following needs psatz, not just lra:

  q1, q : Q
  H : 0 <= q1 ∧ q1 <= 1
  H0 : 0 < q
  H1 : 0 < q * q1
  H2 : ¬ 0 < q * (1 - q1)
  ============================
  q1 == 1

Note that in this case nra does the job much faster and without requiring csdp (although adding csdp to the Coq Platform might still be of interest).

Paolo Giarrusso (Jan 15 2021 at 14:38):

@Pierre Roux cool! but I guess psatz still does more than nra?

Pierre Roux (Jan 15 2021 at 15:15):

I doubt nra implements an SDP solver or a CAD algorithm so certainly yes.

Pierre Roux (Jan 15 2021 at 15:17):

@Frédéric Besson would know better (I would guess nra is based on some interval arithmetic, but I never read the code)

Frédéric Besson (Jan 15 2021 at 15:33):

psatz and nra are using the same verifier back-end. You are right, only psatz is using csdp. It actually uses some code borrowed from J. Harrison.
Typically, nra blindly multiplies the hypotheses, develops them and consider the monomials as independent linear variables.

Paolo Giarrusso (Jan 15 2021 at 19:25):

and is psatz used in CI and maintained? I assume yes but colleagues were asking

Paolo Giarrusso (Jan 15 2021 at 19:25):

(thanks already for all the answers!)

Notification Bot (Jan 15 2021 at 20:04):

This topic was moved by Théo Zimmermann to #Coq Platform devs & users > psatz and coinor-csdp

Last updated: Oct 01 2023 at 18:01 UTC