Stream: Coq users

Topic: psatz and coinor-csdp


view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 14:38):

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

view this post on Zulip Pierre Roux (Jan 15 2021 at 15:15):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:25):

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

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:25):

(thanks already for all the answers!)

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC