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).
@Pierre Roux cool! but I guess
psatz still does more than
nra implements an SDP solver or a CAD algorithm so certainly yes.
@Frédéric Besson would know better (I would guess
nra is based on some interval arithmetic, but I never read the code)
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.
psatz used in CI and maintained? I assume yes but colleagues were asking
(thanks already for all the answers!)
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