mirror of
https://github.com/kalmarek/PropertyT.jl.git
synced 2024-11-26 00:55:27 +01:00
cosmetic changes (mostly empty lines)
This commit is contained in:
parent
ed910ccde5
commit
70c160411d
@ -14,7 +14,7 @@ struct Naive{El} <: Settings
|
|||||||
S::Vector{El}
|
S::Vector{El}
|
||||||
radius::Int
|
radius::Int
|
||||||
upper_bound::Float64
|
upper_bound::Float64
|
||||||
|
|
||||||
solver::JuMP.OptimizerFactory
|
solver::JuMP.OptimizerFactory
|
||||||
warmstart::Bool
|
warmstart::Bool
|
||||||
end
|
end
|
||||||
@ -26,7 +26,7 @@ struct Symmetrized{El} <: Settings
|
|||||||
autS::Group
|
autS::Group
|
||||||
radius::Int
|
radius::Int
|
||||||
upper_bound::Float64
|
upper_bound::Float64
|
||||||
|
|
||||||
solver::JuMP.OptimizerFactory
|
solver::JuMP.OptimizerFactory
|
||||||
warmstart::Bool
|
warmstart::Bool
|
||||||
end
|
end
|
||||||
@ -87,39 +87,43 @@ function warmstart(sett::Settings)
|
|||||||
return ws
|
return ws
|
||||||
end
|
end
|
||||||
|
|
||||||
function approximate_by_SOS(sett::Naive,
|
function approximate_by_SOS(sett::Naive,
|
||||||
elt::GroupRingElem, orderunit::GroupRingElem;
|
elt::GroupRingElem, orderunit::GroupRingElem;
|
||||||
solverlog=tempname()*".log")
|
solverlog=tempname()*".log")
|
||||||
|
|
||||||
|
isdir(fullpath(sett)) || mkpath(fullpath(sett))
|
||||||
|
|
||||||
@info "Creating SDP problem..."
|
@info "Creating SDP problem..."
|
||||||
SDP_problem = SOS_problem(elt, orderunit, upper_bound=sett.upper_bound)
|
SDP_problem = SOS_problem(elt, orderunit, upper_bound=sett.upper_bound)
|
||||||
@info Base.repr(SDP_problem)
|
@info Base.repr(SDP_problem)
|
||||||
|
|
||||||
@info "Logging solver's progress into $solverlog"
|
@info "Logging solver's progress into $solverlog"
|
||||||
|
|
||||||
ws = warmstart(sett)
|
ws = warmstart(sett)
|
||||||
@time status, ws = PropertyT.solve(solverlog, SDP_problem, sett.solver, ws)
|
@time status, ws = PropertyT.solve(solverlog, SDP_problem, sett.solver, ws)
|
||||||
@info "Optimization finished:" status
|
@info "Optimization finished:" status
|
||||||
|
|
||||||
P = value.(SDP_problem[:P])
|
P = value.(SDP_problem[:P])
|
||||||
λ = value(SDP_problem[:λ])
|
λ = value(SDP_problem[:λ])
|
||||||
|
|
||||||
if any(isnan.(P))
|
if any(isnan.(P))
|
||||||
@warn "The solution seems to contain NaNs. Not overriding warmstart.jld"
|
@warn "The solution seems to contain NaNs. Not overriding warmstart.jld"
|
||||||
else
|
else
|
||||||
save(filename(sett, :warmstart), "warmstart", (ws.primal, ws.dual, ws.slack), "P", P, "λ", λ)
|
save(filename(sett, :warmstart), "warmstart", (ws.primal, ws.dual, ws.slack), "P", P, "λ", λ)
|
||||||
end
|
end
|
||||||
|
|
||||||
save(filename(sett, :warmstart, date=true),
|
save(filename(sett, :warmstart, date=true),
|
||||||
"warmstart", (ws.primal, ws.dual, ws.slack), "P", P, "λ", λ)
|
"warmstart", (ws.primal, ws.dual, ws.slack), "P", P, "λ", λ)
|
||||||
|
|
||||||
return λ, P
|
return λ, P
|
||||||
end
|
end
|
||||||
|
|
||||||
function approximate_by_SOS(sett::Symmetrized,
|
function approximate_by_SOS(sett::Symmetrized,
|
||||||
elt::GroupRingElem, orderunit::GroupRingElem;
|
elt::GroupRingElem, orderunit::GroupRingElem;
|
||||||
solverlog=tempname()*".log")
|
solverlog=tempname()*".log")
|
||||||
|
|
||||||
|
isdir(fullpath(sett)) || mkpath(fullpath(sett))
|
||||||
|
|
||||||
if !isfile(filename(sett, :OrbitData))
|
if !isfile(filename(sett, :OrbitData))
|
||||||
isdefined(parent(orderunit), :basis) || throw("You need to define basis of Group Ring to compute orbit decomposition!")
|
isdefined(parent(orderunit), :basis) || throw("You need to define basis of Group Ring to compute orbit decomposition!")
|
||||||
orbit_data = OrbitData(parent(orderunit), sett.autS)
|
orbit_data = OrbitData(parent(orderunit), sett.autS)
|
||||||
@ -131,30 +135,30 @@ function approximate_by_SOS(sett::Symmetrized,
|
|||||||
@info "Creating SDP problem..."
|
@info "Creating SDP problem..."
|
||||||
SDP_problem, varP = SOS_problem(elt, orderunit, orbit_data, upper_bound=sett.upper_bound)
|
SDP_problem, varP = SOS_problem(elt, orderunit, orbit_data, upper_bound=sett.upper_bound)
|
||||||
@info Base.repr(SDP_problem)
|
@info Base.repr(SDP_problem)
|
||||||
|
|
||||||
@info "Logging solver's progress into $solverlog"
|
@info "Logging solver's progress into $solverlog"
|
||||||
|
|
||||||
ws = warmstart(sett)
|
ws = warmstart(sett)
|
||||||
@time status, ws = PropertyT.solve(solverlog, SDP_problem, sett.solver, ws)
|
@time status, ws = PropertyT.solve(solverlog, SDP_problem, sett.solver, ws)
|
||||||
@info "Optimization finished:" status
|
@info "Optimization finished:" status
|
||||||
|
|
||||||
λ = value(SDP_problem[:λ])
|
λ = value(SDP_problem[:λ])
|
||||||
Ps = [value.(P) for P in varP]
|
Ps = [value.(P) for P in varP]
|
||||||
|
|
||||||
if any(any(isnan.(P)) for P in Ps)
|
if any(any(isnan.(P)) for P in Ps)
|
||||||
@warn "The solution seems to contain NaNs. Not overriding warmstart.jld"
|
@warn "The solution seems to contain NaNs. Not overriding warmstart.jld"
|
||||||
else
|
else
|
||||||
save(filename(sett, :warmstart), "warmstart", (ws.primal, ws.dual, ws.slack), "Ps", Ps, "λ", λ)
|
save(filename(sett, :warmstart), "warmstart", (ws.primal, ws.dual, ws.slack), "Ps", Ps, "λ", λ)
|
||||||
end
|
end
|
||||||
|
|
||||||
save(filename(sett, :warmstart, date=true),
|
save(filename(sett, :warmstart, date=true),
|
||||||
"warmstart", (ws.primal, ws.dual, ws.slack), "Ps", Ps, "λ", λ)
|
"warmstart", (ws.primal, ws.dual, ws.slack), "Ps", Ps, "λ", λ)
|
||||||
|
|
||||||
@info "Reconstructing P..."
|
@info "Reconstructing P..."
|
||||||
@time P = reconstruct(Ps, orbit_data)
|
@time P = reconstruct(Ps, orbit_data)
|
||||||
|
|
||||||
return λ, P
|
return λ, P
|
||||||
end
|
end
|
||||||
|
|
||||||
###############################################################################
|
###############################################################################
|
||||||
#
|
#
|
||||||
@ -167,21 +171,21 @@ function certify_SOS_decomposition(elt::GroupRingElem, orderunit::GroupRingElem,
|
|||||||
separator = "-"^76
|
separator = "-"^76
|
||||||
@info "$separator\nChecking in floating-point arithmetic..." λ
|
@info "$separator\nChecking in floating-point arithmetic..." λ
|
||||||
eoi = elt - λ*orderunit
|
eoi = elt - λ*orderunit
|
||||||
|
|
||||||
@info("Computing sum of squares decomposition...")
|
@info("Computing sum of squares decomposition...")
|
||||||
@time residual = eoi - compute_SOS(parent(eoi), augIdproj(Q))
|
@time residual = eoi - compute_SOS(parent(eoi), augIdproj(Q))
|
||||||
|
|
||||||
L1_norm = norm(residual,1)
|
L1_norm = norm(residual,1)
|
||||||
certified_λ = λ - 2.0^(2ceil(log2(R)))*L1_norm
|
floatingpoint_λ = λ - 2.0^(2ceil(log2(R)))*L1_norm
|
||||||
|
|
||||||
info_strs = ["Numerical metrics of the obtained SOS:",
|
info_strs = ["Numerical metrics of the obtained SOS:",
|
||||||
"ɛ(elt - λu - ∑ξᵢ*ξᵢ) ≈ $(aug(residual))",
|
"ɛ(elt - λu - ∑ξᵢ*ξᵢ) ≈ $(aug(residual))",
|
||||||
"‖elt - λu - ∑ξᵢ*ξᵢ‖₁ ≈ $(L1_norm)",
|
"‖elt - λu - ∑ξᵢ*ξᵢ‖₁ ≈ $(L1_norm)",
|
||||||
"Floating point (NOT certified) λ ≈"]
|
"Floating point (NOT certified) λ ≈"]
|
||||||
@info join(info_strs, "\n") certified_λ
|
@info join(info_strs, "\n") floatingpoint_λ
|
||||||
|
|
||||||
if certified_λ ≤ 0
|
if floatingpoint_λ ≤ 0
|
||||||
return certified_λ
|
return floatingpoint_λ
|
||||||
end
|
end
|
||||||
|
|
||||||
λ = @interval(λ)
|
λ = @interval(λ)
|
||||||
@ -190,18 +194,18 @@ function certify_SOS_decomposition(elt::GroupRingElem, orderunit::GroupRingElem,
|
|||||||
"λ ∈ $λ"]
|
"λ ∈ $λ"]
|
||||||
@info(join(info_strs, "\n"))
|
@info(join(info_strs, "\n"))
|
||||||
eoi = elt - λ*orderunit
|
eoi = elt - λ*orderunit
|
||||||
|
|
||||||
@info("Projecting columns of Q to the augmentation ideal...")
|
@info("Projecting columns of Q to the augmentation ideal...")
|
||||||
@time Q, check = augIdproj(Interval, Q)
|
@time Q, check = augIdproj(Interval, Q)
|
||||||
@info "Checking that sum of every column contains 0.0..." check_augmented=check
|
@info "Checking that sum of every column contains 0.0..." check_augmented=check
|
||||||
check || @warn("The following numbers are meaningless!")
|
check || @warn("The following numbers are meaningless!")
|
||||||
|
|
||||||
@info("Computing sum of squares decomposition...")
|
@info("Computing sum of squares decomposition...")
|
||||||
@time residual = eoi - compute_SOS(parent(eoi), Q)
|
@time residual = eoi - compute_SOS(parent(eoi), Q)
|
||||||
|
|
||||||
L1_norm = norm(residual,1)
|
L1_norm = norm(residual,1)
|
||||||
certified_λ = λ - 2.0^(2ceil(log2(R)))*L1_norm
|
certified_λ = λ - 2.0^(2ceil(log2(R)))*L1_norm
|
||||||
|
|
||||||
info_strs = ["Numerical metrics of the obtained SOS:",
|
info_strs = ["Numerical metrics of the obtained SOS:",
|
||||||
"ɛ(elt - λu - ∑ξᵢ*ξᵢ) ∈ $(aug(residual))",
|
"ɛ(elt - λu - ∑ξᵢ*ξᵢ) ∈ $(aug(residual))",
|
||||||
"‖elt - λu - ∑ξᵢ*ξᵢ‖₁ ∈ $(L1_norm)",
|
"‖elt - λu - ∑ξᵢ*ξᵢ‖₁ ∈ $(L1_norm)",
|
||||||
@ -262,7 +266,7 @@ end
|
|||||||
function spectral_gap(sett::Settings)
|
function spectral_gap(sett::Settings)
|
||||||
fp = PropertyT.fullpath(sett)
|
fp = PropertyT.fullpath(sett)
|
||||||
isdir(fp) || mkpath(fp)
|
isdir(fp) || mkpath(fp)
|
||||||
|
|
||||||
if isfile(filename(sett,:Δ))
|
if isfile(filename(sett,:Δ))
|
||||||
# cached
|
# cached
|
||||||
@info "Loading precomputed Δ..."
|
@info "Loading precomputed Δ..."
|
||||||
@ -283,7 +287,7 @@ function spectral_gap(sett::Settings)
|
|||||||
|
|
||||||
λ < 0 && @warn "Solver did not produce a valid solution!"
|
λ < 0 && @warn "Solver did not produce a valid solution!"
|
||||||
end
|
end
|
||||||
|
|
||||||
info_strs = ["Numerical metrics of matrix solution:",
|
info_strs = ["Numerical metrics of matrix solution:",
|
||||||
"sum(P) = $(sum(P))",
|
"sum(P) = $(sum(P))",
|
||||||
"maximum(P) = $(maximum(P))",
|
"maximum(P) = $(maximum(P))",
|
||||||
@ -295,6 +299,6 @@ function spectral_gap(sett::Settings)
|
|||||||
|
|
||||||
@time Q = real(sqrt(Symmetric( (P.+ P')./2 )))
|
@time Q = real(sqrt(Symmetric( (P.+ P')./2 )))
|
||||||
certified_sgap = spectral_gap(Δ, λ, Q, R=sett.radius)
|
certified_sgap = spectral_gap(Δ, λ, Q, R=sett.radius)
|
||||||
|
|
||||||
return certified_sgap
|
return certified_sgap
|
||||||
end
|
end
|
||||||
|
@ -39,11 +39,11 @@ end
|
|||||||
|
|
||||||
function compute_SOS_square(RG::GroupRing, Q::AbstractMatrix{<:Real})
|
function compute_SOS_square(RG::GroupRing, Q::AbstractMatrix{<:Real})
|
||||||
result = zeros(eltype(Q), maximum(RG.pm));
|
result = zeros(eltype(Q), maximum(RG.pm));
|
||||||
|
|
||||||
for i in 1:size(Q,2)
|
for i in 1:size(Q,2)
|
||||||
GroupRings.fmac!(result, view(Q,:,i), view(Q,:,i), RG.pm)
|
GroupRings.fmac!(result, view(Q,:,i), view(Q,:,i), RG.pm)
|
||||||
end
|
end
|
||||||
|
|
||||||
return GroupRingElem(result, RG)
|
return GroupRingElem(result, RG)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -59,7 +59,7 @@ end
|
|||||||
function loadGRElem(fname::String, G::Group)
|
function loadGRElem(fname::String, G::Group)
|
||||||
pm = load(fname, "pm")
|
pm = load(fname, "pm")
|
||||||
RG = GroupRing(G, pm)
|
RG = GroupRing(G, pm)
|
||||||
return loadGRElem(fname, RG)
|
return loadGRElem(fname, RG)
|
||||||
end
|
end
|
||||||
|
|
||||||
function loadGRElem(fname::String)
|
function loadGRElem(fname::String)
|
||||||
|
@ -181,7 +181,7 @@ end
|
|||||||
function (p::perm)(A::GroupRingElem)
|
function (p::perm)(A::GroupRingElem)
|
||||||
RG = parent(A)
|
RG = parent(A)
|
||||||
result = zero(RG, eltype(A.coeffs))
|
result = zero(RG, eltype(A.coeffs))
|
||||||
|
|
||||||
for (idx, c) in enumerate(A.coeffs)
|
for (idx, c) in enumerate(A.coeffs)
|
||||||
if c!= zero(eltype(A.coeffs))
|
if c!= zero(eltype(A.coeffs))
|
||||||
result[p(RG.basis[idx])] = c
|
result[p(RG.basis[idx])] = c
|
||||||
@ -218,8 +218,8 @@ import Base.*
|
|||||||
"""
|
"""
|
||||||
function *(x::AbstractAlgebra.MatElem, P::Generic.perm)
|
function *(x::AbstractAlgebra.MatElem, P::Generic.perm)
|
||||||
z = similar(x)
|
z = similar(x)
|
||||||
m = rows(x)
|
m = nrows(x)
|
||||||
n = cols(x)
|
n = ncols(x)
|
||||||
for i = 1:m
|
for i = 1:m
|
||||||
for j = 1:n
|
for j = 1:n
|
||||||
z[i, j] = x[i,P[j]]
|
z[i, j] = x[i,P[j]]
|
||||||
|
@ -55,14 +55,14 @@ function SOS_problem(X::GroupRingElem, orderunit::GroupRingElem; upper_bound::Fl
|
|||||||
else
|
else
|
||||||
λ = JuMP.@variable(m, λ)
|
λ = JuMP.@variable(m, λ)
|
||||||
end
|
end
|
||||||
|
|
||||||
cnstrs = constraints(parent(X).pm)
|
cnstrs = constraints(parent(X).pm)
|
||||||
for (constraint_indices, x, u) in zip(cnstrs, X.coeffs, orderunit.coeffs)
|
for (constraint_indices, x, u) in zip(cnstrs, X.coeffs, orderunit.coeffs)
|
||||||
JuMP.@constraint(m, x - λ*u == sum(P[constraint_indices]))
|
JuMP.@constraint(m, x - λ*u == sum(P[constraint_indices]))
|
||||||
end
|
end
|
||||||
|
|
||||||
JuMP.@objective(m, Max, λ)
|
JuMP.@objective(m, Max, λ)
|
||||||
|
|
||||||
return m
|
return m
|
||||||
end
|
end
|
||||||
|
|
||||||
@ -88,12 +88,12 @@ function SOS_problem(X::GroupRingElem, orderunit::GroupRingElem, data::OrbitData
|
|||||||
else
|
else
|
||||||
λ = JuMP.@variable(m, λ)
|
λ = JuMP.@variable(m, λ)
|
||||||
end
|
end
|
||||||
|
|
||||||
@info "Adding $(length(data.orbits)) constraints..."
|
@info "Adding $(length(data.orbits)) constraints..."
|
||||||
@time addconstraints!(m, Ps, X, orderunit, data)
|
@time addconstraints!(m, Ps, X, orderunit, data)
|
||||||
|
|
||||||
JuMP.@objective(m, Max, λ)
|
JuMP.@objective(m, Max, λ)
|
||||||
|
|
||||||
return m, Ps
|
return m, Ps
|
||||||
end
|
end
|
||||||
|
|
||||||
@ -121,9 +121,9 @@ function addconstraints!(m::JuMP.Model,
|
|||||||
for (t, orbit) in enumerate(data.orbits)
|
for (t, orbit) in enumerate(data.orbits)
|
||||||
orbit_constraint!(orb_cnstr, cnstrs, orbit)
|
orbit_constraint!(orb_cnstr, cnstrs, orbit)
|
||||||
constraintLHS!(M, orb_cnstr, data.Uπs, UπsT, data.dims)
|
constraintLHS!(M, orb_cnstr, data.Uπs, UπsT, data.dims)
|
||||||
|
|
||||||
x, u = X_orb[t], orderunit_orb[t]
|
x, u = X_orb[t], orderunit_orb[t]
|
||||||
|
|
||||||
JuMP.@constraints m begin
|
JuMP.@constraints m begin
|
||||||
x - λ*u == sum(dot(M[π], P[π]) for π in eachindex(data.Uπs))
|
x - λ*u == sum(dot(M[π], P[π]) for π in eachindex(data.Uπs))
|
||||||
end
|
end
|
||||||
@ -142,7 +142,7 @@ function reconstruct(Ps::Vector{M},
|
|||||||
lU = length(Uπs)
|
lU = length(Uπs)
|
||||||
transfP = [dims[π].*Uπs[π]*Ps[π]*Uπs[π]' for π in 1:lU]
|
transfP = [dims[π].*Uπs[π]*Ps[π]*Uπs[π]' for π in 1:lU]
|
||||||
tmp = [zeros(Float64, size(first(transfP))) for _ in 1:lU]
|
tmp = [zeros(Float64, size(first(transfP))) for _ in 1:lU]
|
||||||
|
|
||||||
Threads.@threads for π in 1:lU
|
Threads.@threads for π in 1:lU
|
||||||
tmp[π] = perm_avg(tmp[π], transfP[π], values(preps))
|
tmp[π] = perm_avg(tmp[π], transfP[π], values(preps))
|
||||||
end
|
end
|
||||||
@ -172,7 +172,7 @@ end
|
|||||||
#
|
#
|
||||||
###############################################################################
|
###############################################################################
|
||||||
|
|
||||||
function warmstart_scs!(m::JuMP.Model, warmstart)
|
function setwarmstart_scs!(m::JuMP.Model, warmstart)
|
||||||
solver_name(m) == "SCS" || throw("warmstarting defined only for SCS!")
|
solver_name(m) == "SCS" || throw("warmstarting defined only for SCS!")
|
||||||
primal, dual, slack = warmstart
|
primal, dual, slack = warmstart
|
||||||
m.moi_backend.optimizer.model.optimizer.sol.primal = primal
|
m.moi_backend.optimizer.model.optimizer.sol.primal = primal
|
||||||
@ -190,14 +190,14 @@ function getwarmstart_scs(m::JuMP.Model)
|
|||||||
)
|
)
|
||||||
return warmstart
|
return warmstart
|
||||||
end
|
end
|
||||||
|
|
||||||
function solve(m::JuMP.Model, with_optimizer::JuMP.OptimizerFactory, warmstart=nothing)
|
function solve(m::JuMP.Model, with_optimizer::JuMP.OptimizerFactory, warmstart=nothing)
|
||||||
|
|
||||||
set_optimizer(m, with_optimizer)
|
set_optimizer(m, with_optimizer)
|
||||||
MOIU.attach_optimizer(m)
|
MOIU.attach_optimizer(m)
|
||||||
|
|
||||||
if warmstart != nothing
|
if warmstart != nothing
|
||||||
warmstart_scs!(m, warmstart)
|
setwarmstart_scs!(m, warmstart)
|
||||||
end
|
end
|
||||||
|
|
||||||
optimize!(m)
|
optimize!(m)
|
||||||
|
Loading…
Reference in New Issue
Block a user