mirror of
https://github.com/kalmarek/PropertyT.jl.git
synced 2024-11-29 17:50:27 +01:00
Merge branch 'enh/rework-logging' of https://git.wmi.amu.edu.pl/kalmar/PropertyT.jl into enh/rework-logging
This commit is contained in:
commit
8413254917
@ -36,9 +36,8 @@ function compute_SOS(Q::AbstractArray, pm::Array{Int,2}, l::Int)
|
||||
groupring_square(Q[:,i], l, pm)
|
||||
end
|
||||
|
||||
println("")
|
||||
|
||||
return result
|
||||
|
||||
end
|
||||
|
||||
function compute_SOS(Q::AbstractArray, RG::GroupRing, l::Int)
|
||||
@ -46,32 +45,13 @@ function compute_SOS(Q::AbstractArray, RG::GroupRing, l::Int)
|
||||
return GroupRingElem(result, RG)
|
||||
end
|
||||
|
||||
function distance_to_cone{T<:Interval}(elt::GroupRingElem, Q::AbstractArray{T,2}, wlen::Int)
|
||||
SOS = compute_SOS(Q, parent(elt), length(elt.coeffs))
|
||||
SOS_diff = elt - SOS
|
||||
function distances_to_cone(elt::GroupRingElem, wlen::Int)
|
||||
ɛ_dist = GroupRings.augmentation(elt)
|
||||
|
||||
ɛ_dist = GroupRings.augmentation(SOS_diff)
|
||||
info(logger, "ɛ(∑ξᵢ*ξᵢ) ∈ $(ɛ_dist)")
|
||||
|
||||
eoi_SOS_L1_dist = norm(SOS_diff,1)
|
||||
info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ∈ $(eoi_SOS_L1_dist)")
|
||||
eoi_SOS_L1_dist = norm(elt,1)
|
||||
|
||||
dist = 2^(wlen-1)*eoi_SOS_L1_dist
|
||||
return dist
|
||||
end
|
||||
|
||||
function distance_to_cone{T}(elt::GroupRingElem, Q::AbstractArray{T,2}, wlen::Int)
|
||||
SOS = compute_SOS(Q, parent(elt), length(elt.coeffs))
|
||||
SOS_diff = elt - SOS
|
||||
|
||||
ɛ_dist = GroupRings.augmentation(SOS_diff)
|
||||
info(logger, "ɛ(Δ² - λΔ - ∑ξᵢ*ξᵢ) ≈ $(@sprintf("%.10f", ɛ_dist))")
|
||||
|
||||
eoi_SOS_L1_dist = norm(SOS_diff,1)
|
||||
info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ≈ $(@sprintf("%.10f", eoi_SOS_L1_dist))")
|
||||
|
||||
dist = 2^(wlen-1)*eoi_SOS_L1_dist
|
||||
return dist
|
||||
return dist, ɛ_dist, eoi_SOS_L1_dist
|
||||
end
|
||||
|
||||
function augIdproj{T, I<:AbstractInterval}(S::Type{I}, Q::AbstractArray{T,2})
|
||||
@ -99,30 +79,56 @@ function augIdproj{T}(Q::AbstractArray{T,2}, logger)
|
||||
return Q
|
||||
end
|
||||
|
||||
function distance_to_positive_cone(Δ::GroupRingElem, λ, Q, wlen::Int)
|
||||
function distance_to_cone(elt::GroupRingElem, λ::T, Q::AbstractArray{T,2}, wlen::Int, logger) where {T<:AbstractFloat}
|
||||
|
||||
info(logger, "------------------------------------------------------------")
|
||||
info(logger, "λ = $λ")
|
||||
info(logger, "Checking in floating-point arithmetic...")
|
||||
Δ²_λΔ = EOI(Δ, λ)
|
||||
@logtime logger fp_distance = λ - distance_to_cone(Δ²_λΔ, Q, wlen)
|
||||
info(logger, "Floating point distance (to positive cone) ≈ $(@sprintf("%.10f", fp_distance))")
|
||||
@logtime logger SOS_diff = elt - compute_SOS(Q, parent(elt), length(elt.coeffs))
|
||||
dist, ɛ_dist, eoi_SOS_L1_dist = distances_to_cone(SOS_diff, wlen)
|
||||
info(logger, "ɛ(Δ² - λΔ - ∑ξᵢ*ξᵢ) ≈ $(@sprintf("%.10f", ɛ_dist))")
|
||||
info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ≈ $(@sprintf("%.10f", eoi_SOS_L1_dist))")
|
||||
|
||||
fp_distance = λ - dist
|
||||
|
||||
info(logger, "Floating point distance (to positive cone) ≈")
|
||||
info(logger, "$(@sprintf("%.10f", fp_distance))")
|
||||
info(logger, "")
|
||||
|
||||
return fp_distance
|
||||
end
|
||||
|
||||
function distance_to_cone(elt::GroupRingElem, λ::T, Q::AbstractArray{T,2}, wlen::Int, logger) where {T<:AbstractInterval}
|
||||
info(logger, "------------------------------------------------------------")
|
||||
info(logger, "λ = $λ")
|
||||
info(logger, "Checking in interval arithmetic...")
|
||||
@logtime logger SOS_diff = elt - compute_SOS(Q, parent(elt), length(elt.coeffs))
|
||||
dist, ɛ_dist, eoi_SOS_L1_dist = distances_to_cone(SOS_diff, wlen)
|
||||
info(logger, "ɛ(∑ξᵢ*ξᵢ) ∈ $(ɛ_dist)")
|
||||
info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ∈ $(eoi_SOS_L1_dist)")
|
||||
|
||||
int_distance = λ - dist
|
||||
|
||||
info(logger, "The Augmentation-projected actual distance (to positive cone) ∈")
|
||||
info(logger, "$(int_distance)")
|
||||
info(logger, "")
|
||||
|
||||
return int_distance
|
||||
end
|
||||
|
||||
function check_distance_to_cone(Δ::GroupRingElem, λ, Q, wlen::Int, logger)
|
||||
|
||||
fp_distance = distance_to_cone(EOI(Δ, λ), λ, Q, wlen, logger)
|
||||
|
||||
if fp_distance ≤ 0
|
||||
return fp_distance
|
||||
end
|
||||
|
||||
info(logger, "")
|
||||
Q = augIdproj(Q, logger)
|
||||
|
||||
info(logger, "Checking in interval arithmetic")
|
||||
λ = @interval(λ)
|
||||
Δ = GroupRingElem([@interval(c) for c in Δ.coeffs], parent(Δ))
|
||||
Δ²_λΔ = EOI(Δ, λ)
|
||||
Q = augIdproj(Q, logger)
|
||||
|
||||
@logtime logger Interval_dist_to_ΣSq = λ - distance_to_cone(Δ²_λΔ, Q, wlen)
|
||||
info(logger, "The Augmentation-projected actual distance (to positive cone) ∈ $(Interval_dist_to_ΣSq)")
|
||||
info(logger, "------------------------------------------------------------")
|
||||
int_distance = distance_to_cone(EOI(Δ, λ), λ, Q, wlen, logger)
|
||||
|
||||
return Interval_dist_to_ΣSq
|
||||
return int_distance.lo
|
||||
end
|
||||
|
||||
@ -14,6 +14,7 @@ immutable Settings{T<:AbstractMathProgSolver}
|
||||
upper_bound::Float64
|
||||
tol::Float64
|
||||
warmstart::Bool
|
||||
logger
|
||||
end
|
||||
|
||||
prefix(s::Settings) = s.name
|
||||
@ -32,23 +33,23 @@ immutable OrbitData{T<:AbstractArray{Float64, 2}, LapType <:AbstractVector{Float
|
||||
end
|
||||
|
||||
function OrbitData(sett::Settings)
|
||||
splap = load(joinpath(prepath(sett), "delta.jld"), "Δ");
|
||||
pm = load(joinpath(prepath(sett), "pm.jld"), "pm");
|
||||
splap = load(filename(prepath(sett), :Δ), "Δ");
|
||||
pm = load(filename(prepath(sett), :pm), "pm");
|
||||
cnstr = PropertyT.constraints(pm);
|
||||
splap² = similar(splap)
|
||||
splap² = GroupRings.mul!(splap², splap, splap, pm);
|
||||
|
||||
Uπs = load(joinpath(prepath(sett), "U_pis.jld"), "Uπs")
|
||||
Uπs = load(filename(prepath(sett), :Uπs), "Uπs")
|
||||
nzros = [i for i in 1:length(Uπs) if size(Uπs[i],2) !=0]
|
||||
Uπs = Uπs[nzros]
|
||||
Uπs = sparsify!.(Uπs, sett.tol, check=true, verbose=true)
|
||||
|
||||
#dimensions of the corresponding πs:
|
||||
dims = load(joinpath(prepath(sett), "U_pis.jld"), "dims")[nzros]
|
||||
dims = load(filename(prepath(sett), :Uπs), "dims")[nzros]
|
||||
|
||||
m, P = init_model(size(Uπs,1), [size(U,2) for U in Uπs]);
|
||||
|
||||
orbits = load(joinpath(prepath(sett), "orbits.jld"), "orbits");
|
||||
orbits = load(filename(prepath(sett), :orb), "orbits");
|
||||
n = size(Uπs[1],1)
|
||||
orb_spcnstrm = [orbit_constraint(cnstr[collect(orb)], n) for orb in orbits]
|
||||
orb_splap = orbit_spvector(splap, orbits)
|
||||
@ -79,7 +80,7 @@ function sparsify!{Tv,Ti}(M::SparseMatrixCSC{Tv,Ti}, eps=eps(Tv); verbose=false)
|
||||
m = nnz(M)
|
||||
|
||||
if verbose
|
||||
info(logger, "Sparsified density:", rpad(densM, 20), " → ", rpad(dens(M), 20))
|
||||
info("Sparsified density:", rpad(densM, 20), " → ", rpad(dens(M), 20))
|
||||
end
|
||||
|
||||
return M
|
||||
@ -91,11 +92,11 @@ function sparsify!{T}(M::AbstractArray{T}, eps=eps(T); check=false, verbose=fals
|
||||
M[abs.(M) .< eps] .= zero(T)
|
||||
|
||||
if check && rankM != rank(M)
|
||||
warn(logger, "Sparsification decreased the rank!")
|
||||
warn("Sparsification decreased the rank!")
|
||||
end
|
||||
|
||||
if verbose
|
||||
info(logger, "Sparsified density:", rpad(densM, 20), " → ", rpad(dens(M),20))
|
||||
info("Sparsified density:", rpad(densM, 20), " → ", rpad(dens(M),20))
|
||||
end
|
||||
|
||||
return sparse(M)
|
||||
@ -103,19 +104,6 @@ end
|
||||
|
||||
sparsify{T}(U::AbstractArray{T}, tol=eps(T); check=true, verbose=false) = sparsify!(deepcopy(U), tol, check=check, verbose=verbose)
|
||||
|
||||
function init_orbit_data(logger, sett::Settings; radius=2)
|
||||
|
||||
ex(fname) = isfile(joinpath(prepath(sett), fname))
|
||||
|
||||
files_exists = ex.(["delta.jld", "pm.jld", "U_pis.jld", "orbits.jld", "preps.jld"])
|
||||
|
||||
if !all(files_exists)
|
||||
compute_orbit_data(logger, prepath(sett), sett.G, sett.S, sett.autS, radius=radius)
|
||||
end
|
||||
|
||||
return 0
|
||||
end
|
||||
|
||||
function transform(U::AbstractArray, V::AbstractArray; sparse=true)
|
||||
if sparse
|
||||
return sparsify!(U'*V*U)
|
||||
@ -178,8 +166,8 @@ function init_model(n, sizes)
|
||||
end
|
||||
|
||||
function create_SDP_problem(sett::Settings)
|
||||
info(logger, "Loading orbit data....")
|
||||
@logtime logger SDP_problem, orb_data = OrbitData(sett);
|
||||
info(sett.logger, "Loading orbit data....")
|
||||
@logtime sett.logger SDP_problem, orb_data = OrbitData(sett);
|
||||
|
||||
if sett.upper_bound < Inf
|
||||
λ = JuMP.getvariable(SDP_problem, :λ)
|
||||
@ -187,8 +175,8 @@ function create_SDP_problem(sett::Settings)
|
||||
end
|
||||
|
||||
t = length(orb_data.laplacian)
|
||||
info(logger, "Adding $t constraints ... ")
|
||||
@logtime logger addconstraints!(SDP_problem, orb_data)
|
||||
info(sett.logger, "Adding $t constraints ... ")
|
||||
@logtime sett.logger addconstraints!(SDP_problem, orb_data)
|
||||
|
||||
return SDP_problem, orb_data
|
||||
end
|
||||
@ -201,16 +189,16 @@ function λandP(m::JuMP.Model, data::OrbitData, warmstart=true)
|
||||
end
|
||||
|
||||
function λandP(m::JuMP.Model, data::OrbitData, sett::Settings)
|
||||
info(logger, "Solving SDP problem...")
|
||||
λ, Ps = λandP(m, data, sett.warmstart)
|
||||
info(sett.logger, "Solving SDP problem...")
|
||||
@logtime sett.logger λ, Ps = λandP(m, data, sett.warmstart)
|
||||
|
||||
info(logger, "Reconstructing P...")
|
||||
info(sett.logger, "Reconstructing P...")
|
||||
|
||||
preps = load_preps(joinpath(prepath(sett), "preps.jld"), sett.autS)
|
||||
preps = load_preps(filename(prepath(sett), :preps), sett.autS)
|
||||
|
||||
@logtime logger recP = reconstruct_sol(preps, data.Us, Ps, data.dims)
|
||||
@logtime sett.logger recP = reconstruct_sol(preps, data.Us, Ps, data.dims)
|
||||
|
||||
fname = PropertyT.λSDPfilenames(fullpath(sett))[2]
|
||||
fname = filename(fullpath(sett), :P)
|
||||
save(fname, "origP", Ps, "P", recP)
|
||||
return λ, recP
|
||||
end
|
||||
@ -229,49 +217,39 @@ end
|
||||
|
||||
function check_property_T(sett::Settings)
|
||||
|
||||
init_orbit_data(logger, sett, radius=sett.radius)
|
||||
ex(s) = exists(filename(prepath(sett), s))
|
||||
|
||||
if !sett.warmstart && all(isfile.(λSDPfilenames(fullpath(sett))))
|
||||
files_exists = ex.([:pm, :Δ, :Uπs, :orb, :preps])
|
||||
|
||||
if !all(files_exists)
|
||||
compute_orbit_data(sett.logger, prepath(sett), sett.S, sett.autS, radius=sett.radius)
|
||||
end
|
||||
|
||||
cond1 = exists(filename(fullpath(sett), :λ))
|
||||
cond2 = exists(filename(fullpath(sett), :P))
|
||||
|
||||
if !sett.warmstart && cond1 && cond2
|
||||
λ, P = PropertyT.λandP(fullpath(sett))
|
||||
else
|
||||
info(logger, "Creating SDP problem...")
|
||||
info(sett.logger, "Creating SDP problem...")
|
||||
SDP_problem, orb_data = create_SDP_problem(sett)
|
||||
JuMP.setsolver(SDP_problem, sett.solver)
|
||||
info(sett.logger, Base.repr(SDP_problem))
|
||||
|
||||
λ, P = λandP(SDP_problem, orb_data, sett)
|
||||
end
|
||||
|
||||
info(logger, "λ = $λ")
|
||||
info(logger, "sum(P) = $(sum(P))")
|
||||
info(logger, "maximum(P) = $(maximum(P))")
|
||||
info(logger, "minimum(P) = $(minimum(P))")
|
||||
|
||||
if λ > 0
|
||||
pm_fname, Δ_fname = pmΔfilenames(prepath(sett))
|
||||
RG = GroupRing(sett.G, load(pm_fname, "pm"))
|
||||
Δ = GroupRingElem(load(Δ_fname, "Δ")[:, 1], RG)
|
||||
info(sett.logger, "λ = $λ")
|
||||
info(sett.logger, "sum(P) = $(sum(P))")
|
||||
info(sett.logger, "maximum(P) = $(maximum(P))")
|
||||
info(sett.logger, "minimum(P) = $(minimum(P))")
|
||||
|
||||
isapprox(eigvals(P), abs.(eigvals(P)), atol=sett.tol) ||
|
||||
warn("The solution matrix doesn't seem to be positive definite!")
|
||||
# @assert P == Symmetric(P)
|
||||
@logtime logger Q = real(sqrtm(Symmetric(P)))
|
||||
|
||||
sgap = distance_to_positive_cone(Δ, λ, Q, 2*sett.radius)
|
||||
if isa(sgap, Interval)
|
||||
sgap = sgap.lo
|
||||
if λ > 0
|
||||
return check_λ(sett.name, sett.S, λ, P, sett.radius, sett.logger)
|
||||
end
|
||||
if sgap > 0
|
||||
info(logger, "λ ≥ $(Float64(trunc(sgap,12)))")
|
||||
Kazhdan_κ = PropertyT.Kazhdan_from_sgap(sgap, length(sett.S))
|
||||
Kazhdan_κ = Float64(trunc(Kazhdan_κ, 12))
|
||||
info(logger, "κ($(sett.name), S) ≥ $Kazhdan_κ: Group HAS property (T)!")
|
||||
return true
|
||||
else
|
||||
sgap = Float64(trunc(sgap, 12))
|
||||
info(logger, "λ($(sett.name), S) ≥ $sgap: Group may NOT HAVE property (T)!")
|
||||
return false
|
||||
end
|
||||
end
|
||||
info(logger, "κ($(sett.name), S) ≥ $λ < 0: Tells us nothing about property (T)")
|
||||
info(sett.logger, "κ($(sett.name), S) ≥ $λ < 0: Tells us nothing about property (T)")
|
||||
return false
|
||||
end
|
||||
|
||||
@ -166,12 +166,13 @@ function orthSVD{T}(M::AbstractMatrix{T})
|
||||
return fact[:U][:,1:M_rank]
|
||||
end
|
||||
|
||||
function compute_orbit_data{T<:GroupElem}(logger, name::String, G::Nemo.Group, S::Vector{T}, autS::Nemo.Group; radius=2)
|
||||
function compute_orbit_data{T<:GroupElem}(logger, name::String, S::Vector{T}, autS::Nemo.Group; radius=2)
|
||||
isdir(name) || mkdir(name)
|
||||
|
||||
info(logger, "Generating ball of radius $(2*radius)")
|
||||
|
||||
# TODO: Fix that by multiple dispatch?
|
||||
G = parent(first(S))
|
||||
Id = (isa(G, Nemo.Ring) ? one(G) : G())
|
||||
|
||||
@logtime logger E_2R, sizes = Groups.generate_balls(S, Id, radius=2*radius);
|
||||
@ -182,10 +183,10 @@ function compute_orbit_data{T<:GroupElem}(logger, name::String, G::Nemo.Group, S
|
||||
info(logger, "Product matrix")
|
||||
@logtime logger pm = GroupRings.create_pm(E_2R, E_rdict, sizes[radius], twisted=true)
|
||||
RG = GroupRing(G, E_2R, E_rdict, pm)
|
||||
Δ = PropertyT.splaplacian(RG, S)
|
||||
Δ = PropertyT.spLaplacian(RG, S)
|
||||
@assert GroupRings.augmentation(Δ) == 0
|
||||
save(joinpath(name, "delta.jld"), "Δ", Δ.coeffs)
|
||||
save(joinpath(name, "pm.jld"), "pm", pm)
|
||||
save(filename(name, :Δ), "Δ", Δ.coeffs)
|
||||
save(filename(name, :pm), "pm", pm)
|
||||
|
||||
info(logger, "Decomposing E into orbits of $(autS)")
|
||||
@logtime logger orbs = orbit_decomposition(autS, E_2R, E_rdict)
|
||||
@ -195,7 +196,7 @@ function compute_orbit_data{T<:GroupElem}(logger, name::String, G::Nemo.Group, S
|
||||
|
||||
info(logger, "Action matrices")
|
||||
@logtime logger reps = perm_reps(autS, E_2R[1:sizes[radius]], E_rdict)
|
||||
save_preps(joinpath(name, "preps.jld"), reps)
|
||||
save_preps(filename(name, :preps), reps)
|
||||
reps = matrix_reps(reps)
|
||||
|
||||
info(logger, "Projections")
|
||||
|
||||
364
src/PropertyT.jl
364
src/PropertyT.jl
@ -12,18 +12,28 @@ using MathProgBase
|
||||
|
||||
using Memento
|
||||
|
||||
const logger = Memento.config("info", fmt="{msg}")
|
||||
const solver_logger = Memento.config("info", fmt="{msg}")
|
||||
|
||||
function setup_logging(name::String)
|
||||
isdir(name) || mkdir(name)
|
||||
L = Memento.config("info", fmt="{date}| {msg}")
|
||||
|
||||
Memento.add_handler(logger,
|
||||
Memento.DefaultHandler(joinpath(name,"full_$(string((now()))).log"),
|
||||
Memento.DefaultFormatter("{date}| {msg}")), "full_log")
|
||||
handler = Memento.DefaultHandler(
|
||||
filename(name, :logall), Memento.DefaultFormatter("{date}| {msg}"))
|
||||
|
||||
e = redirect_stderr(logger.handlers["full_log"].io)
|
||||
handler.levels.x = L.levels
|
||||
L.handlers["all"] = handler
|
||||
|
||||
# e = redirect_stderr(L.handlers["all"].io)
|
||||
|
||||
return L
|
||||
end
|
||||
|
||||
function solverlogger(name)
|
||||
logger = Memento.config("info", fmt="{msg}")
|
||||
|
||||
handler = DefaultHandler(
|
||||
filename(name, :logsolver), DefaultFormatter("{date}| {msg}"))
|
||||
handler.levels.x = logger.levels
|
||||
logger.handlers["solver_log"] = handler
|
||||
return logger
|
||||
end
|
||||
|
||||
@ -36,7 +46,7 @@ macro logtime(logger, ex)
|
||||
local diff = Base.GC_Diff(Base.gc_num(), stats)
|
||||
local ts = time_string(elapsedtime, diff.allocd, diff.total_time,
|
||||
Base.gc_alloc_count(diff))
|
||||
esc(info(logger, ts))
|
||||
$(esc(info))($(esc(logger)), ts)
|
||||
val
|
||||
end
|
||||
end
|
||||
@ -66,277 +76,112 @@ function time_string(elapsedtime, bytes, gctime, allocs)
|
||||
return str
|
||||
end
|
||||
|
||||
function exists(fname::String)
|
||||
return isfile(fname) || islink(fname)
|
||||
exists(fname::String) = isfile(fname) || islink(fname)
|
||||
|
||||
filename(prefix, s::Symbol) = filename(prefix, Val{s})
|
||||
|
||||
@eval begin
|
||||
for (s,n) in [
|
||||
[:pm, "pm.jld"],
|
||||
[:Δ, "delta.jld"],
|
||||
[:λ, "lambda.jld"],
|
||||
[:P, "SDPmatrix.jld"],
|
||||
[:warm, "warmstart.jld"],
|
||||
[:Uπs, "U_pis.jld"],
|
||||
[:orb, "orbits.jld"],
|
||||
[:preps,"preps.jld"],
|
||||
|
||||
[:logall, "full_$(string(now())).log"],
|
||||
[:logsolver,"solver_$(string(now())).log"]
|
||||
]
|
||||
|
||||
filename(prefix::String, ::Type{Val{$:(s)}}) = joinpath(prefix, :($n))
|
||||
end
|
||||
end
|
||||
|
||||
function pmΔfilenames(prefix::String)
|
||||
isdir(prefix) || mkdir(prefix)
|
||||
pm_filename = joinpath(prefix, "pm.jld")
|
||||
Δ_coeff_filename = joinpath(prefix, "delta.jld")
|
||||
return pm_filename, Δ_coeff_filename
|
||||
function Laplacian(name::String, G::Group)
|
||||
if exists(filename(name, :Δ)) && exists(filename(name, :pm))
|
||||
RG = GroupRing(G, load(filename(name, :pm), "pm"))
|
||||
Δ = GroupRingElem(load(filename(name, :Δ), "Δ")[:, 1], RG)
|
||||
else
|
||||
throw("You need to precompute $(filename(name, :pm)) and $(filename(name, :Δ)) to load it!")
|
||||
end
|
||||
return Δ
|
||||
end
|
||||
|
||||
function λSDPfilenames(prefix::String)
|
||||
isdir(prefix) || mkdir(prefix)
|
||||
λ_filename = joinpath(prefix, "lambda.jld")
|
||||
SDP_filename = joinpath(prefix, "SDPmatrix.jld")
|
||||
return λ_filename, SDP_filename
|
||||
end
|
||||
function Laplacian{T<:GroupElem}(S::Vector{T}, Id::T,
|
||||
logger=getlogger(); radius::Int=2)
|
||||
|
||||
function ΔandSDPconstraints(prefix::String, G::Group)
|
||||
info(logger, "Loading precomputed pm, Δ, sdp_constraints...")
|
||||
pm_fname, Δ_fname = pmΔfilenames(prefix)
|
||||
|
||||
product_matrix = load(pm_fname, "pm")
|
||||
sdp_constraints = constraints(product_matrix)
|
||||
|
||||
RG = GroupRing(G, product_matrix)
|
||||
Δ = GroupRingElem(load(Δ_fname, "Δ")[:, 1], RG)
|
||||
|
||||
return Δ, sdp_constraints
|
||||
end
|
||||
|
||||
function ΔandSDPconstraints{T<:GroupElem}(name::String, S::Vector{T}, Id::T; radius::Int=2)
|
||||
info(logger, "Computing pm, Δ, sdp_constraints...")
|
||||
Δ, sdp_constraints = ΔandSDPconstraints(S, Id, radius=radius)
|
||||
pm_fname, Δ_fname = pmΔfilenames(name)
|
||||
save(pm_fname, "pm", parent(Δ).pm)
|
||||
save(Δ_fname, "Δ", Δ.coeffs)
|
||||
return Δ, sdp_constraints
|
||||
end
|
||||
|
||||
function ΔandSDPconstraints{T<:GroupElem}(S::Vector{T}, Id::T; radius::Int=2)
|
||||
info(logger, "Generating balls of sizes $sizes")
|
||||
info(logger, "Generating metric ball of radius $radius...")
|
||||
@logtime logger E_R, sizes = Groups.generate_balls(S, Id, radius=2*radius)
|
||||
info(logger, "Generated balls of sizes $sizes.")
|
||||
|
||||
info(logger, "Creating product matrix...")
|
||||
@logtime logger pm = GroupRings.create_pm(E_R, GroupRings.reverse_dict(E_R), sizes[radius]; twisted=true)
|
||||
|
||||
info(logger, "Creating sdp_constratints...")
|
||||
@logtime logger sdp_constraints = PropertyT.constraints(pm)
|
||||
|
||||
RG = GroupRing(parent(Id), E_R, pm)
|
||||
|
||||
Δ = splaplacian(RG, S)
|
||||
return Δ, sdp_constraints
|
||||
Δ = spLaplacian(RG, S)
|
||||
return Δ
|
||||
end
|
||||
|
||||
function λandP(name::String)
|
||||
λ_fname, SDP_fname = λSDPfilenames(name)
|
||||
f₁ = exists(λ_fname)
|
||||
f₂ = exists(SDP_fname)
|
||||
λ_fname = filename(name, :λ)
|
||||
P_fname = filename(name, :P)
|
||||
|
||||
if f₁ && f₂
|
||||
info(logger, "Loading precomputed λ, P...")
|
||||
if exists(λ_fname) && exists(P_fname)
|
||||
λ = load(λ_fname, "λ")
|
||||
P = load(SDP_fname, "P")
|
||||
P = load(P_fname, "P")
|
||||
else
|
||||
throw(ArgumentError("You need to precompute λ and SDP matrix P to load it!"))
|
||||
throw("You need to precompute $λ_fname and $P_fname to load it!")
|
||||
end
|
||||
return λ, P
|
||||
end
|
||||
|
||||
function λandP(name::String, SDP_problem::JuMP.Model, varλ, varP, warmstart=false)
|
||||
add_handler(solver_logger,
|
||||
DefaultHandler(joinpath(name, "solver_$(string(now())).log"),
|
||||
DefaultFormatter("{date}| {msg}")),
|
||||
"solver_log")
|
||||
if warmstart && isfile(joinpath(name, "warmstart.jld"))
|
||||
ws = load(joinpath(name, "warmstart.jld"), "warmstart")
|
||||
function λandP(name::String, SDP::JuMP.Model, varλ, varP, warmstart=true)
|
||||
|
||||
if warmstart && isfile(filename(name, :warm))
|
||||
ws = load(filename(name, :warm), "warmstart")
|
||||
else
|
||||
ws = nothing
|
||||
end
|
||||
|
||||
λ, P, warmstart = compute_λandP(SDP_problem, varλ, varP, warmstart=ws)
|
||||
solver_log = solverlogger(name)
|
||||
|
||||
remove_handler(solver_logger, "solver_log")
|
||||
Base.Libc.flush_cstdio()
|
||||
o = redirect_stdout(solver_log.handlers["solver_log"].io)
|
||||
Base.Libc.flush_cstdio()
|
||||
|
||||
λ_fname, P_fname = λSDPfilenames(name)
|
||||
λ, P, warmstart = solve_SDP(SDP, varλ, varP, warmstart=ws)
|
||||
|
||||
Base.Libc.flush_cstdio()
|
||||
redirect_stdout(o)
|
||||
|
||||
delete!(solver_log.handlers, "solver_log")
|
||||
|
||||
if λ > 0
|
||||
save(λ_fname, "λ", λ)
|
||||
save(P_fname, "P", P)
|
||||
save(joinpath(name, "warmstart.jld"), "warmstart", warmstart)
|
||||
save(filename(name, :λ), "λ", λ)
|
||||
save(filename(name, :P), "P", P)
|
||||
save(filename(name, :warm), "warmstart", warmstart)
|
||||
else
|
||||
throw(ErrorException("Solver did not produce a valid solution!: λ = $λ"))
|
||||
throw(ErrorException("Solver did not produce a valid solution: λ = $λ"))
|
||||
end
|
||||
return λ, P
|
||||
|
||||
end
|
||||
|
||||
function fillfrominternal!(m::JuMP.Model, traits)
|
||||
# Copied from JuMP/src/solvers.jl:178
|
||||
|
||||
stat::Symbol = MathProgBase.status(m.internalModel)
|
||||
|
||||
numRows, numCols = length(m.linconstr), m.numCols
|
||||
m.objBound = NaN
|
||||
m.objVal = NaN
|
||||
m.colVal = fill(NaN, numCols)
|
||||
m.linconstrDuals = Array{Float64}(0)
|
||||
|
||||
discrete = (traits.int || traits.sos)
|
||||
|
||||
if stat == :Optimal
|
||||
# If we think dual information might be available, try to get it
|
||||
# If not, return an array of the correct length
|
||||
if discrete
|
||||
m.redCosts = fill(NaN, numCols)
|
||||
m.linconstrDuals = fill(NaN, numRows)
|
||||
else
|
||||
if !traits.conic
|
||||
m.redCosts = try
|
||||
MathProgBase.getreducedcosts(m.internalModel)[1:numCols]
|
||||
catch
|
||||
fill(NaN, numCols)
|
||||
end
|
||||
|
||||
m.linconstrDuals = try
|
||||
MathProgBase.getconstrduals(m.internalModel)[1:numRows]
|
||||
catch
|
||||
fill(NaN, numRows)
|
||||
end
|
||||
elseif !traits.qp && !traits.qc
|
||||
JuMP.fillConicDuals(m)
|
||||
end
|
||||
end
|
||||
else
|
||||
# Problem was not solved to optimality, attempt to extract useful
|
||||
# information anyway
|
||||
|
||||
if traits.lin
|
||||
if stat == :Infeasible
|
||||
m.linconstrDuals = try
|
||||
infray = MathProgBase.getinfeasibilityray(m.internalModel)
|
||||
@assert length(infray) == numRows
|
||||
infray
|
||||
catch
|
||||
suppress_warnings || warn("Infeasibility ray (Farkas proof) not available")
|
||||
fill(NaN, numRows)
|
||||
end
|
||||
elseif stat == :Unbounded
|
||||
m.colVal = try
|
||||
unbdray = MathProgBase.getunboundedray(m.internalModel)
|
||||
@assert length(unbdray) == numCols
|
||||
unbdray
|
||||
catch
|
||||
suppress_warnings || warn("Unbounded ray not available")
|
||||
fill(NaN, numCols)
|
||||
end
|
||||
end
|
||||
end
|
||||
# conic duals (currently, SOC and SDP only)
|
||||
if !discrete && traits.conic && !traits.qp && !traits.qc
|
||||
if stat == :Infeasible
|
||||
JuMP.fillConicDuals(m)
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
# If the problem was solved, or if it terminated prematurely, try
|
||||
# to extract a solution anyway. This commonly occurs when a time
|
||||
# limit or tolerance is set (:UserLimit)
|
||||
if !(stat == :Infeasible || stat == :Unbounded)
|
||||
try
|
||||
# Do a separate try since getobjval could work while getobjbound does not and vice versa
|
||||
objBound = MathProgBase.getobjbound(m.internalModel) + m.obj.aff.constant
|
||||
m.objBound = objBound
|
||||
end
|
||||
try
|
||||
objVal = MathProgBase.getobjval(m.internalModel) + m.obj.aff.constant
|
||||
colVal = MathProgBase.getsolution(m.internalModel)[1:numCols]
|
||||
# Rescale off-diagonal terms of SDP variables
|
||||
if traits.sdp
|
||||
offdiagvars = JuMP.offdiagsdpvars(m)
|
||||
colVal[offdiagvars] /= sqrt(2)
|
||||
end
|
||||
# Don't corrupt the answers if one of the above two calls fails
|
||||
m.objVal = objVal
|
||||
m.colVal = colVal
|
||||
end
|
||||
end
|
||||
|
||||
return stat
|
||||
end
|
||||
|
||||
function compute_λandP(m, varλ, varP; warmstart=nothing)
|
||||
λ = 0.0
|
||||
P = nothing
|
||||
|
||||
traits = JuMP.ProblemTraits(m, relaxation=false)
|
||||
|
||||
while λ == 0.0
|
||||
try
|
||||
JuMP.build(m, traits=traits)
|
||||
if warmstart != nothing
|
||||
p_sol, d_sol, s = warmstart
|
||||
MathProgBase.SolverInterface.setwarmstart!(m.internalModel, p_sol; dual_sol = d_sol, slack=s);
|
||||
end
|
||||
solve_SDP(m)
|
||||
λ = MathProgBase.getobjval(m.internalModel)
|
||||
catch y
|
||||
warn(solver_logger, y)
|
||||
end
|
||||
end
|
||||
|
||||
warmstart = (m.internalModel.primal_sol, m.internalModel.dual_sol,
|
||||
m.internalModel.slack)
|
||||
|
||||
fillfrominternal!(m, traits)
|
||||
|
||||
P = JuMP.getvalue(varP)
|
||||
λ = JuMP.getvalue(varλ)
|
||||
|
||||
return λ, P, warmstart
|
||||
end
|
||||
|
||||
Kazhdan_from_sgap(λ,N) = sqrt(2*λ/N)
|
||||
|
||||
function check_property_T(name::String, S, Id, solver, upper_bound, tol, radius)
|
||||
function check_λ(name, S, λ, P, radius, logger)
|
||||
|
||||
isdir(name) || mkdir(name)
|
||||
RG = GroupRing(parent(first(S)), load(filename(name, :pm), "pm"))
|
||||
Δ = GroupRingElem(load(filename(name, :Δ), "Δ")[:, 1], RG)
|
||||
|
||||
if all(exists.(pmΔfilenames(name)))
|
||||
# cached
|
||||
Δ, sdp_constraints = ΔandSDPconstraints(name, parent(S[1]))
|
||||
else
|
||||
# compute
|
||||
Δ, sdp_constraints = ΔandSDPconstraints(name, S, Id, radius=radius)
|
||||
end
|
||||
|
||||
if all(exists.(λSDPfilenames(name)))
|
||||
λ, P = λandP(name)
|
||||
else
|
||||
info(logger, "Creating SDP problem...")
|
||||
SDP_problem, λ, P = create_SDP_problem(Δ, sdp_constraints, upper_bound=upper_bound)
|
||||
JuMP.setsolver(SDP_problem, solver)
|
||||
|
||||
|
||||
λ, P = λandP(name, SDP_problem, λ, P)
|
||||
end
|
||||
|
||||
info(logger, "λ = $λ")
|
||||
info(logger, "sum(P) = $(sum(P))")
|
||||
info(logger, "maximum(P) = $(maximum(P))")
|
||||
info(logger, "minimum(P) = $(minimum(P))")
|
||||
|
||||
if λ > 0
|
||||
pm_fname, Δ_fname = pmΔfilenames(name)
|
||||
RG = GroupRing(parent(first(S)), load(pm_fname, "pm"))
|
||||
Δ = GroupRingElem(load(Δ_fname, "Δ")[:, 1], RG)
|
||||
|
||||
isapprox(eigvals(P), abs(eigvals(P)), atol=tol) ||
|
||||
warn("The solution matrix doesn't seem to be positive definite!")
|
||||
# @assert P == Symmetric(P)
|
||||
@logtime logger Q = real(sqrtm(Symmetric(P)))
|
||||
|
||||
sgap = distance_to_positive_cone(Δ, λ, Q, 2*radius)
|
||||
if isa(sgap, Interval)
|
||||
sgap = sgap.lo
|
||||
end
|
||||
sgap = check_distance_to_cone(Δ, λ, Q, 2*radius, logger)
|
||||
|
||||
if sgap > 0
|
||||
info(logger, "λ ≥ $(Float64(trunc(sgap,12)))")
|
||||
info(logger, "λ($name, S) ≥ $(Float64(trunc(sgap,12)))")
|
||||
Kazhdan_κ = Kazhdan_from_sgap(sgap, length(S))
|
||||
Kazhdan_κ = Float64(trunc(Kazhdan_κ, 12))
|
||||
info(logger, "κ($name, S) ≥ $Kazhdan_κ: Group HAS property (T)!")
|
||||
@ -347,7 +192,50 @@ function check_property_T(name::String, S, Id, solver, upper_bound, tol, radius)
|
||||
return false
|
||||
end
|
||||
end
|
||||
info(logger, "κ($name, S) ≥ $λ < 0: Tells us nothing about property (T)")
|
||||
|
||||
function check_property_T(name::String, S, Id, solver, upper_bound, tol, radius)
|
||||
|
||||
isdir(name) || mkdir(name)
|
||||
LOGGER = Memento.getlogger()
|
||||
|
||||
if exists(filename(name, :pm)) && exists(filename(name, :Δ))
|
||||
# cached
|
||||
info(LOGGER, "Loading precomputed Δ...")
|
||||
Δ = Laplacian(name, parent(S[1]))
|
||||
else
|
||||
# compute
|
||||
Δ = Laplacian(S, Id, LOGGER, radius=radius)
|
||||
save(filename(name, :pm), "pm", parent(Δ).pm)
|
||||
save(filename(name, :Δ), "Δ", Δ.coeffs)
|
||||
end
|
||||
|
||||
fullpath = joinpath(name, string(upper_bound))
|
||||
isdir(fullpath) || mkdir(fullpath)
|
||||
|
||||
if exists(filename(fullpath, :λ)) && exists(filename(fullpath, :P))
|
||||
info(LOGGER, "Loading precomputed λ, P...")
|
||||
λ, P = λandP(fullpath)
|
||||
else
|
||||
info(LOGGER, "Creating SDP problem...")
|
||||
SDP_problem, varλ, varP = create_SDP_problem(Δ, constraints(parent(Δ).pm), upper_bound=upper_bound)
|
||||
JuMP.setsolver(SDP_problem, solver)
|
||||
info(LOGGER, Base.repr(SDP_problem))
|
||||
|
||||
@logtime LOGGER λ, P = λandP(fullpath, SDP_problem, varλ, varP)
|
||||
end
|
||||
|
||||
info(LOGGER, "λ = $λ")
|
||||
info(LOGGER, "sum(P) = $(sum(P))")
|
||||
info(LOGGER, "maximum(P) = $(maximum(P))")
|
||||
info(LOGGER, "minimum(P) = $(minimum(P))")
|
||||
|
||||
isapprox(eigvals(P), abs.(eigvals(P)), atol=tol) ||
|
||||
warn("The solution matrix doesn't seem to be positive definite!")
|
||||
|
||||
if λ > 0
|
||||
return check_λ(name, S, λ, P, radius, LOGGER)
|
||||
end
|
||||
info(LOGGER, "κ($name, S) ≥ $λ < 0: Tells us nothing about property (T)")
|
||||
return false
|
||||
end
|
||||
|
||||
|
||||
131
src/SDPs.jl
131
src/SDPs.jl
@ -13,7 +13,7 @@ function constraints(pm, total_length=maximum(pm))
|
||||
return constraints
|
||||
end
|
||||
|
||||
function splaplacian(RG::GroupRing, S, T::Type=Float64)
|
||||
function spLaplacian(RG::GroupRing, S, T::Type=Float64)
|
||||
result = RG(T)
|
||||
result[RG.group()] = T(length(S))
|
||||
for s in S
|
||||
@ -22,7 +22,7 @@ function splaplacian(RG::GroupRing, S, T::Type=Float64)
|
||||
return result
|
||||
end
|
||||
|
||||
function splaplacian{TT<:Ring}(RG::GroupRing{TT}, S, T::Type=Float64)
|
||||
function spLaplacian{TT<:Ring}(RG::GroupRing{TT}, S, T::Type=Float64)
|
||||
result = RG(T)
|
||||
result[one(RG.group)] = T(length(S))
|
||||
for s in S
|
||||
@ -55,21 +55,122 @@ function create_SDP_problem(Δ::GroupRingElem, matrix_constraints; upper_bound=I
|
||||
return m, λ, P
|
||||
end
|
||||
|
||||
function solve_SDP(SDP_problem)
|
||||
info(logger, Base.repr(SDP_problem))
|
||||
function solve_SDP(m, varλ, varP; warmstart=nothing)
|
||||
|
||||
o = redirect_stdout(solver_logger.handlers["solver_log"].io)
|
||||
Base.Libc.flush_cstdio()
|
||||
traits = JuMP.ProblemTraits(m, relaxation=false)
|
||||
|
||||
@logtime logger solution_status = MathProgBase.optimize!(SDP_problem.internalModel)
|
||||
Base.Libc.flush_cstdio()
|
||||
|
||||
redirect_stdout(o)
|
||||
|
||||
if solution_status != :Optimal
|
||||
warn(logger, "The solver did not solve the problem successfully!")
|
||||
JuMP.build(m, traits=traits)
|
||||
if warmstart != nothing
|
||||
p_sol, d_sol, s = warmstart
|
||||
MathProgBase.SolverInterface.setwarmstart!(m.internalModel, p_sol; dual_sol = d_sol, slack=s);
|
||||
end
|
||||
info(logger, solution_status)
|
||||
|
||||
return 0
|
||||
MathProgBase.optimize!(m.internalModel)
|
||||
|
||||
λ = MathProgBase.getobjval(m.internalModel)
|
||||
|
||||
warmstart = (m.internalModel.primal_sol, m.internalModel.dual_sol,
|
||||
m.internalModel.slack)
|
||||
|
||||
fillfrominternal!(m, traits)
|
||||
|
||||
P = JuMP.getvalue(varP)
|
||||
λ = JuMP.getvalue(varλ)
|
||||
|
||||
return λ, P, warmstart
|
||||
end
|
||||
|
||||
function fillfrominternal!(m::JuMP.Model, traits)
|
||||
# Copied from JuMP/src/solvers.jl:178
|
||||
|
||||
stat::Symbol = MathProgBase.status(m.internalModel)
|
||||
|
||||
numRows, numCols = length(m.linconstr), m.numCols
|
||||
m.objBound = NaN
|
||||
m.objVal = NaN
|
||||
m.colVal = fill(NaN, numCols)
|
||||
m.linconstrDuals = Array{Float64}(0)
|
||||
|
||||
discrete = (traits.int || traits.sos)
|
||||
|
||||
if stat == :Optimal
|
||||
# If we think dual information might be available, try to get it
|
||||
# If not, return an array of the correct length
|
||||
if discrete
|
||||
m.redCosts = fill(NaN, numCols)
|
||||
m.linconstrDuals = fill(NaN, numRows)
|
||||
else
|
||||
if !traits.conic
|
||||
m.redCosts = try
|
||||
MathProgBase.getreducedcosts(m.internalModel)[1:numCols]
|
||||
catch
|
||||
fill(NaN, numCols)
|
||||
end
|
||||
|
||||
m.linconstrDuals = try
|
||||
MathProgBase.getconstrduals(m.internalModel)[1:numRows]
|
||||
catch
|
||||
fill(NaN, numRows)
|
||||
end
|
||||
elseif !traits.qp && !traits.qc
|
||||
JuMP.fillConicDuals(m)
|
||||
end
|
||||
end
|
||||
else
|
||||
# Problem was not solved to optimality, attempt to extract useful
|
||||
# information anyway
|
||||
|
||||
if traits.lin
|
||||
if stat == :Infeasible
|
||||
m.linconstrDuals = try
|
||||
infray = MathProgBase.getinfeasibilityray(m.internalModel)
|
||||
@assert length(infray) == numRows
|
||||
infray
|
||||
catch
|
||||
suppress_warnings || warn("Infeasibility ray (Farkas proof) not available")
|
||||
fill(NaN, numRows)
|
||||
end
|
||||
elseif stat == :Unbounded
|
||||
m.colVal = try
|
||||
unbdray = MathProgBase.getunboundedray(m.internalModel)
|
||||
@assert length(unbdray) == numCols
|
||||
unbdray
|
||||
catch
|
||||
suppress_warnings || warn("Unbounded ray not available")
|
||||
fill(NaN, numCols)
|
||||
end
|
||||
end
|
||||
end
|
||||
# conic duals (currently, SOC and SDP only)
|
||||
if !discrete && traits.conic && !traits.qp && !traits.qc
|
||||
if stat == :Infeasible
|
||||
JuMP.fillConicDuals(m)
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
# If the problem was solved, or if it terminated prematurely, try
|
||||
# to extract a solution anyway. This commonly occurs when a time
|
||||
# limit or tolerance is set (:UserLimit)
|
||||
if !(stat == :Infeasible || stat == :Unbounded)
|
||||
try
|
||||
# Do a separate try since getobjval could work while getobjbound does not and vice versa
|
||||
objBound = MathProgBase.getobjbound(m.internalModel) + m.obj.aff.constant
|
||||
m.objBound = objBound
|
||||
end
|
||||
try
|
||||
objVal = MathProgBase.getobjval(m.internalModel) + m.obj.aff.constant
|
||||
colVal = MathProgBase.getsolution(m.internalModel)[1:numCols]
|
||||
# Rescale off-diagonal terms of SDP variables
|
||||
if traits.sdp
|
||||
offdiagvars = JuMP.offdiagsdpvars(m)
|
||||
colVal[offdiagvars] /= sqrt(2)
|
||||
end
|
||||
# Don't corrupt the answers if one of the above two calls fails
|
||||
m.objVal = objVal
|
||||
m.colVal = colVal
|
||||
end
|
||||
end
|
||||
|
||||
return stat
|
||||
end
|
||||
|
||||
Loading…
Reference in New Issue
Block a user