diff --git a/src/PropertyT.jl b/src/PropertyT.jl index a60015f..ba9dc02 100644 --- a/src/PropertyT.jl +++ b/src/PropertyT.jl @@ -4,6 +4,7 @@ using JLD using GroupRings using Memento +using Groups import Nemo: Group, GroupElem const logger = Memento.config("info", fmt="{msg}") @@ -45,23 +46,21 @@ function ΔandSDPconstraints(name::String, G::Group) return Δ, sdp_constraints end -function ΔandSDPconstraints{T<:GroupElem}(name::String, S::Vector{T}, radius::Int) - S, Id = generating_set() +function ΔandSDPconstraints{T<:GroupElem}(name::String, S::Vector{T}, Id::T; radius::Int=2) info(logger, "Computing pm, Δ, sdp_constraints...") - t = @timed Δ, sdp_constraints = ΔandSDPconstraints(S, radius) - info(logger, timed_msg(t)) + Δ, 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}, r::Int=2) - Id = parent(S[1])() - B, sizes = Groups.generate_balls(S, Id, radius=2*r) +function ΔandSDPconstraints{T<:GroupElem}(S::Vector{T}, Id::T; radius::Int=2) + B, sizes = Groups.generate_balls(S, Id, radius=2*radius) info(logger, "Generated balls of sizes $sizes") info(logger, "Creating product matrix...") - t = @timed pm = GroupRings.create_pm(B, GroupRings.reverse_dict(B), sizes[r]; twisted=true) + t = @timed pm = GroupRings.create_pm(B, GroupRings.reverse_dict(B), sizes[radius]; twisted=true) info(logger, timed_msg(t)) info(logger, "Creating sdp_constratints...") @@ -70,7 +69,7 @@ function ΔandSDPconstraints{T<:GroupElem}(S::Vector{T}, r::Int=2) RG = GroupRing(parent(Id), B, pm) - Δ = splaplacian(RG, S, B[1:sizes[r]], sizes[2*r]) + Δ = splaplacian(RG, S, Id, sizes[2*radius]) return Δ, sdp_constraints end @@ -143,6 +142,7 @@ end Kazhdan_from_sgap(λ,N) = sqrt(2*λ/N) function setup_logging(name::String) + isdir(name) || mkdir(name) Memento.add_handler(logger, Memento.DefaultHandler(joinpath(name,"full_$(string((now()))).log"), @@ -155,20 +155,16 @@ function setup_logging(name::String) end -function check_property_T(name::String, S, solver, upper_bound, tol, radius) +function check_property_T(name::String, S, Id, solver, upper_bound, tol, radius) - if !isdir(name) - mkdir(name) - end - - setup_logging(name) + isdir(name) || mkdir(name) if all(isfile.(pmΔfilenames(name))) # cached Δ, sdp_constraints = ΔandSDPconstraints(name, parent(S[1])) else # compute - Δ, sdp_constraints = ΔandSDPconstraints(name, S, radius) + Δ, sdp_constraints = ΔandSDPconstraints(name, S, Id, radius=radius) end info(logger, "|S| = $(length(S))") @@ -202,7 +198,7 @@ function check_property_T(name::String, S, solver, upper_bound, tol, radius) end if sgap > 0 info(logger, "λ ≥ $(Float64(trunc(sgap,12)))") - Kazhdan_κ = Kazhdan_from_sgap(sgap, S) + Kazhdan_κ = Kazhdan_from_sgap(sgap, length(S)) Kazhdan_κ = Float64(trunc(Kazhdan_κ, 12)) info(logger, "κ($name, S) ≥ $Kazhdan_κ: Group HAS property (T)!") return true diff --git a/src/checksolution.jl b/src/checksolution.jl index 4e04c92..2db075e 100644 --- a/src/checksolution.jl +++ b/src/checksolution.jl @@ -81,7 +81,7 @@ function distance_to_cone{T<:Rational, S<:Interval}(λ::T, sqrt_matrix::Array{S, SOS = compute_SOS(sqrt_matrix, Δ) info(logger, "ɛ(∑ξᵢ*ξᵢ) ∈ $(GroupRings.augmentation(SOS))") λ_int = @interval(λ) - Δ_int = GroupRingElem([@interval(c) for c in Δ.coeffs], parent(Δ).pm) + Δ_int = GroupRingElem([@interval(c) for c in Δ.coeffs], parent(Δ)) SOS_diff = EOI(Δ_int, λ_int) - SOS eoi_SOS_L1_dist = norm(SOS_diff,1) @@ -91,7 +91,7 @@ function distance_to_cone{T<:Rational, S<:Interval}(λ::T, sqrt_matrix::Array{S, info(logger, "ɛ(Δ² - λΔ - ∑ξᵢ*ξᵢ) ∈ $(ɛ_dist)") info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ∈ $(eoi_SOS_L1_dist)") - distance_to_cone = λ - 2^(len-1)*eoi_SOS_L₁_dist + distance_to_cone = λ - 2^(len-1)*eoi_SOS_L1_dist return distance_to_cone end @@ -99,14 +99,14 @@ function distance_to_cone{T<:AbstractFloat}(λ::T, sqrt_matrix::Array{T,2}, Δ:: SOS = compute_SOS(sqrt_matrix, Δ) SOS_diff = EOI(Δ, λ) - SOS - eoi_SOS_L₁_dist = norm(SOS_diff,1) + eoi_SOS_L1_dist = norm(SOS_diff,1) info(logger, "λ = $λ") ɛ_dist = GroupRings.augmentation(SOS_diff) info(logger, "ɛ(Δ² - λΔ - ∑ξᵢ*ξᵢ) ≈ $(@sprintf("%.10f", ɛ_dist))") - info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ≈ $(@sprintf("%.10f", eoi_SOS_L₁_dist))") + info(logger, "‖Δ² - λΔ - ∑ξᵢ*ξᵢ‖₁ ≈ $(@sprintf("%.10f", eoi_SOS_L1_dist))") - distance_to_cone = λ - 2^(len-1)*eoi_SOS_L₁_dist + distance_to_cone = λ - 2^(len-1)*eoi_SOS_L1_dist return distance_to_cone end @@ -115,7 +115,7 @@ function check_distance_to_positive_cone(Δ::GroupRingElem, λ, P; isapprox(eigvals(P), abs(eigvals(P)), atol=tol) || warn("The solution matrix doesn't seem to be positive definite!") - @assert P == Symmetric(P) + # @assert P == Symmetric(P) Q = real(sqrtm(P)) info(logger, "------------------------------------------------------------") @@ -130,6 +130,7 @@ function check_distance_to_positive_cone(Δ::GroupRingElem, λ, P; return fp_distance end + info(logger, "") info(logger, "Projecting columns of rationalized Q to the augmentation ideal...") δ = eps(λ) Q_ℚ = ℚ(Q, δ) @@ -140,20 +141,20 @@ function check_distance_to_positive_cone(Δ::GroupRingElem, λ, P; info(logger, "Checking in interval arithmetic") Q_ℚω_int = Float64.(Q_ℚω) ± δ - t = @timed Interval_dist_to_Σ² = distance_to_cone(λ_ℚ, Q_ℚω_int, Δ_ℚ, len=len) + t = @timed Interval_dist_to_ΣSq = distance_to_cone(λ_ℚ, Q_ℚω_int, Δ_ℚ, len=len) info(logger, timed_msg(t)) - info(logger, "The Augmentation-projected actual distance (to positive cone) ∈ $(Interval_dist_to_Σ²)") + info(logger, "The Augmentation-projected actual distance (to positive cone) ∈ $(Interval_dist_to_ΣSq)") info(logger, "------------------------------------------------------------") - if Interval_dist_to_Σ².lo ≤ 0 || !rational - return Interval_dist_to_Σ² + if Interval_dist_to_ΣSq.lo ≤ 0 || !rational + return Interval_dist_to_ΣSq else info(logger, "Checking Projected SOS decomposition in exact rational arithmetic...") - t = @timed ℚ_dist_to_Σ² = distance_to_cone(λ_ℚ, Q_ℚω, Δ_ℚ, len=len) + t = @timed ℚ_dist_to_ΣSq = distance_to_cone(λ_ℚ, Q_ℚω, Δ_ℚ, len=len) info(logger, timed_msg(t)) - @assert isa(ℚ_dist_to_Σ², Rational) - info(logger, "Augmentation-projected rational distance (to positive cone) ≥ $(Float64(trunc(ℚ_dist_to_Σ²,8)))") + @assert isa(ℚ_dist_to_ΣSq, Rational) + info(logger, "Augmentation-projected rational distance (to positive cone) ≥ $(Float64(trunc(ℚ_dist_to_ΣSq,8)))") info(logger, "------------------------------------------------------------") - return ℚ_dist_to_Σ² + return ℚ_dist_to_ΣSq end end diff --git a/src/sdps.jl b/src/sdps.jl index 365b960..20489a1 100644 --- a/src/sdps.jl +++ b/src/sdps.jl @@ -13,9 +13,9 @@ function constraints_from_pm(pm, total_length=maximum(pm)) return constraints end -function splaplacian(RG::GroupRing, S, basis, n=length(basis), T::Type=Int) +function splaplacian(RG::GroupRing, S, Id=RG.group(), n=length(basis),T::Type=Int) result = RG(spzeros(T, n)) - result[RG.group()] = T(length(S)) + result[Id] = T(length(S)) for s in S result[s] -= one(T) end @@ -27,7 +27,7 @@ function create_SDP_problem(Δ::GroupRingElem, matrix_constraints; upper_bound=I Δ² = Δ*Δ @assert length(Δ.coeffs) == length(matrix_constraints) m = JuMP.Model(); - JuMP.@variable(m, P[1:N, 1:N], SDP) + JuMP.@variable(m, P[1:N, 1:N]) JuMP.@SDconstraint(m, P >= 0) JuMP.@constraint(m, sum(P[i] for i in eachindex(P)) == 0)