make augmented compute_sos fast

src/certify.jl

@@ -5,80 +5,50 @@ function augment_columns!(Q::AbstractMatrix)
     return Q
 end
 
-function _fma_SOS_thr!(
+function __sos_via_sqr!(
-    result::AbstractVector{T},
+    res::StarAlgebras.AlgebraElement,
-    mstructure::AbstractMatrix{<:Integer},
+    P::AbstractMatrix;
-    Q::AbstractMatrix{T},
+    augmented::Bool
-    acc_matrix=zeros(T, size(mstructure)...),
+)
-) where {T}
+    StarAlgebras.zero!(res)
-
+    A = parent(res)
-    s1, s2 = size(mstructure)
+    b = basis(A)
-
+    @assert size(A.mstructure) == size(P)
-    @inbounds for k = 1:s2
+    e = b[one(b[1])]
-        let k = k, s1 = s1, s2 = s2, Q = Q, acc_matrix = acc_matrix
+
-            Threads.@threads for j = 1:s2
+    for i in axes(A.mstructure, 1)
-                for i = 1:s1
+        x = StarAlgebras._istwisted(A.mstructure) ? StarAlgebras.star(b[i]) : b[i]
-                    @inbounds acc_matrix[i, j] =
+        for j in axes(A.mstructure, 2)
-                        muladd(Q[i, k], Q[j, k], acc_matrix[i, j])
+            p = P[i, j]
-                end
+            xy = b[A.mstructure[i, j]]
-            end
+            # either result += P[x,y]*(x*y)
-        end
+            res[xy] += p
-    end
+            if augmented
-
+                # or result += P[x,y]*(1-x)*(1-y) == P[x,y]*(2-x-y+xy)
-    @inbounds for j = 1:s2
+                y = b[j]
-        for i = 1:s1
+                res[e] += p
-            result[mstructure[i, j]] += acc_matrix[i, j]
+                res[x] -= p
-        end
+                res[y] -= p
-    end
+            end
-
+        end
-    return result
+    end
-end
+
-
+    return res
-function _cnstr_sos!(res::StarAlgebras.AlgebraElement, Q::AbstractMatrix, cnstrs)
+end
+
+function __sos_via_cnstr!(res::StarAlgebras.AlgebraElement, Q²::AbstractMatrix, cnstrs)
     StarAlgebras.zero!(res)
-    Q² = Q' * Q
     for (g, A_g) in cnstrs
         res[g] = dot(A_g, Q²)
     end
     return res
 end
 
-function _augmented_sos!(res::StarAlgebras.AlgebraElement, Q::AbstractMatrix)
-    A = parent(res)
-    StarAlgebras.zero!(res)
-    Q² = Q' * Q
-
-    N = LinearAlgebra.checksquare(A.mstructure)
-    augmented_basis = [A(1) - A(b) for b in @view basis(A)[1:N]]
-    tmp = zero(res)
-
-    for (j, y) in enumerate(augmented_basis)
-        for (i, x) in enumerate(augmented_basis)
-            # res += Q²[i, j] * x * y
-
-            StarAlgebras.mul!(tmp, x, y)
-            StarAlgebras.mul!(tmp, tmp, Q²[i, j])
-            StarAlgebras.add!(res, res, tmp)
-        end
-    end
-    return res
-end
-
 function compute_sos(A::StarAlgebras.StarAlgebra, Q::AbstractMatrix; augmented::Bool)
-    if augmented
+    Q² = Q' * Q
-        z = zeros(eltype(Q), length(basis(A)))
+    res = StarAlgebras.AlgebraElement(zeros(eltype(Q²), length(basis(A))), A)
-        res = StarAlgebras.AlgebraElement(z, A)
+    res = __sos_via_sqr!(res, Q², augmented=augmented)
-        return _augmented_sos!(res, Q)
+    return res
-        cnstrs = constraints(basis(A), A.mstructure; augmented=true)
-        return _cnstr_sos!(res, Q, cnstrs)
-    else
-        @assert size(A.mstructure) == size(Q)
-        z = zeros(eltype(Q), length(basis(A)))
-
-        _fma_SOS_thr!(z, A.mstructure, Q)
-
-        return StarAlgebras.AlgebraElement(z, A)
-    end
 end
 
 function sufficient_λ(residual::StarAlgebras.AlgebraElement, λ; halfradius)
@@ -159,7 +129,7 @@ function certify_solution(
         true, compute_sos(parent(elt), Q_int, augmented=augmented)
     end
 
-    @info "Checking in $(eltype(sos_int)) arithmetic with" λ
+    @info "Checking in $(eltype(sos_int)) arithmetic with" λ_int
 
     λ_certified =
         sufficient_λ(elt, orderunit, λ_int, sos_int, halfradius=halfradius)

test/1712.07167.jl

@@ -6,37 +6,20 @@ function check_positivity(elt, unit, wd; upper_bound=Inf, halfradius=2, optimize
     @time status, _ = PropertyT.solve(sos_problem, optimizer)
 
     Q = let Ps = Ps
-        flPs = [real.(sqrt(JuMP.value.(P))) for P in Ps]
+        Qs = [real.(sqrt(JuMP.value.(P))) for P in Ps]
-        PropertyT.reconstruct(flPs, wd)
+        PropertyT.reconstruct(Qs, wd)
     end
 
     λ = JuMP.value(sos_problem[:λ])
 
-    sos = let RG = parent(elt), Q = Q
+    certified, λ_cert = PropertyT.certify_solution(
-        z = zeros(eltype(Q), length(basis(RG)))
+        elt,
-        res = AlgebraElement(z, RG)
+        unit,
-        cnstrs = PropertyT.constraints(basis(RG), RG.mstructure, augmented=true)
+        λ,
-        PropertyT._cnstr_sos!(res, Q, cnstrs)
+        Q,
-    end
+        halfradius=2
-
+    )
-    residual = elt - λ * unit - sos
+    return status, certified, λ_cert
-    λ_fl = PropertyT.sufficient_λ(residual, λ, halfradius=2)
-
-    λ_fl < 0 && return status, false, λ_fl
-
-    sos = let RG = parent(elt), Q = [PropertyT.IntervalArithmetic.@interval(q) for q in Q]
-        z = zeros(eltype(Q), length(basis(RG)))
-        res = AlgebraElement(z, RG)
-        cnstrs = PropertyT.constraints(basis(RG), RG.mstructure, augmented=true)
-        PropertyT._cnstr_sos!(res, Q, cnstrs)
-    end
-
-    λ_int = PropertyT.IntervalArithmetic.@interval(λ)
-
-    residual_int = elt - λ_int * unit - sos
-    λ_int = PropertyT.sufficient_λ(residual_int, λ_int, halfradius=2)
-
-    return status, λ_int > 0, PropertyT.IntervalArithmetic.inf(λ_int)
 end
 
 @testset "1712.07167 Examples" begin