Basic example: Mantel's theorem
The maximum edge density in triangle free graphs is well known to be $\frac{1}{2}$, as was first proven by Mantel in 1907. Here we give an automatic proof.
using FlagSOS
Setting up the model
We define the relevant graphs using their adjacency matrices.
edge = Graph(Bool[0 1; 1 0]);
triangle = Graph(Bool[0 1 1; 1 0 1; 1 1 0]);
We start with an empty FlagModel
of type Graph
, where we forbid the triangle graph (and all graphs containing it):
m = FlagModel{Graph}()
addForbiddenFlag!(m, triangle)
Set{Graph} with 1 element:
Graph(Bool[0 1 1; 1 0 1; 1 1 0])
Choosing a relaxation
Now we need to choose a hierarchy. One option is the Lasserre hierarchy, which we can attach to the model using addLasserreBlock!
.
addLasserreBlock!(m, 4);
This results in a semidefinite programming problem with block sizes
modelSize(m)
5₁4₂2₂1₃
We want to maximize the edge
density, which we do by minimizing its negative
m.objective = -1 * edge
-1 Graph(Bool[0 1; 1 0])
Finally, we compute the coefficients of the SDP.
computeSDP!(m)
1-element Vector{Nothing}:
nothing
Solving the SDP
We solve the relaxation using Hypatia.
using Hypatia, JuMP
jm = buildJuMPModel(m)
set_optimizer(jm.model, Hypatia.Optimizer)
optimize!(jm.model)
termination_status(jm.model)
OPTIMAL::TerminationStatusCode = 1
objective_value(jm.model)
0.5000000041677629
This page was generated using Literate.jl.