Skip to content

Instantly share code, notes, and snippets.

@micromaomao
Created December 10, 2020 00:15
Show Gist options
  • Save micromaomao/24b45ed36c64d22f4079afac3614fd59 to your computer and use it in GitHub Desktop.
Save micromaomao/24b45ed36c64d22f4079afac3614fd59 to your computer and use it in GitHub Desktop.
### A Pluto.jl notebook ###
# v0.12.16
using Markdown
using InteractiveUtils
# This Pluto notebook uses @bind for interactivity. When running this notebook outside of Pluto, the following 'mock version' of @bind gives bound variables a default value (instead of an error).
macro bind(def, element)
quote
local el = $(esc(element))
global $(esc(def)) = Core.applicable(Base.get, el) ? Base.get(el) : missing
el
end
end
# ╔═╡ 4488cec8-3a6f-11eb-2408-ffdbbe77174e
begin
using GraphPlot
using LightGraphs
using Random
struct Graph
size::Int
edges::Set{Tuple{Int,Int}}
end
function carteisan(a::Vector{T}, b::Vector{T}) where {T}
res = Vector{Tuple{T,T}}()
for x in a
for y in b
push!(res, (x, y))
end
end
res
end
function carteisan(a::AbstractVector{T}, b::AbstractVector{T}) where {T}
a_a = collect(a)
b_a = collect(b)
carteisan(a_a, b_a)
end
md"""
# A notebook that finds instances to #4(b)
"""
end
# ╔═╡ 70b22786-3a67-11eb-0f32-2d56e507c545
begin
local gs_ctrl, edge_ctrl
gs_ctrl = @bind graph_size html"""<input type="number" min="1" max="20" step="1">"""
edge_ctrl = @bind nb_edges html"""<input type="number" min="0" max="4000">"""
md"""
## Parameters
Graph size: $gs_ctrl \
Number of edges: $edge_ctrl
"""
end
# ╔═╡ a8e1fde4-3a75-11eb-2442-1fc311bbeec1
if !@isdefined(graph_size) || ismissing(graph_size) || graph_size == 0 || isnan(graph_size)
html"""<span style="color: red">Please enter parameters above!</span>"""
elseif graph_size^2 < nb_edges
"""
<div style="color: white; background-color: red; font-weight: bold; padding: 10px;">
The number of edges (""" * "$nb_edges" * """) is too large for a graph of size """ * "$graph_size" * """!
</div>
""" |> HTML
else
nothing
end
# ╔═╡ 4cdc1938-3a77-11eb-039b-7912ca4c14e7
function rand_graph()
size = graph_size
edge_vec = carteisan(1:size,1:size)
shuffle!(edge_vec)
graph = SimpleDiGraph{Int}(size)
for i in 1:nb_edges
if !add_edge!(graph, edge_vec[i])
throw("add edge failed.")
end
end
graph
end
# ╔═╡ fa6144a0-3a72-11eb-0a71-018f50186e73
begin
local b
b = @bind btn html"""<input type="button" value="Regenerate">"""
md"Press me to regenerate graph: $b"
end
# ╔═╡ 54108498-3a70-11eb-192d-7b2f5d535135
btn; g = rand_graph()
# ╔═╡ 9889b41e-3a70-11eb-0321-dd32b90c542f
gplot(g,nodelabel=collect(1:nv(g)),arrowlengthfrac=0.1,layout=stressmajorize_layout)
# ╔═╡ 75e73fdc-3a78-11eb-2456-bd336b501dfe
function box(inner, vert)
nexts = neighbors(g, vert)
for n in nexts
if !inner(n)
return false
end
end
return true
end
# ╔═╡ e5450594-3a78-11eb-1d7b-e55a8bfff409
function diamond(inner, vert)
nexts = neighbors(g, vert)
for n in nexts
if inner(n)
return true
end
end
return false
end
# ╔═╡ 13fc1260-3a79-11eb-0bcc-e96fed3d7fc3
implies(a, b) = !a || b
# ╔═╡ 26f220c6-3a79-11eb-39db-b53e700fc0d0
formula(p, vert) = implies(diamond(v -> box(p, v), vert), box(v -> diamond(p, v), vert))
# ╔═╡ 867b04e8-3a79-11eb-1f0d-b3e8437f97ac
function formula(p)
for v in vertices(g)
if !formula(p, v)
return false
end
end
true
end
# ╔═╡ b0600344-3a79-11eb-3c2f-3d00f3a6d705
function formula()
for i in 0:(2^nv(g)-1)
p(v) = (i & (1<<(v-1))) != 0
if !formula(p)
return false
end
end
return true
end
# ╔═╡ 41e0cf1c-3a7a-11eb-1b6c-519ac78d7bd5
begin
local ans
if formula()
ans = html"""<span style="color: green">valid</span>"""
else
ans = html"""<span style="color: red">not valid</span>"""
end
md"### The formula is $ans in this graph!"
end
# ╔═╡ Cell order:
# ╟─4488cec8-3a6f-11eb-2408-ffdbbe77174e
# ╟─70b22786-3a67-11eb-0f32-2d56e507c545
# ╟─a8e1fde4-3a75-11eb-2442-1fc311bbeec1
# ╟─4cdc1938-3a77-11eb-039b-7912ca4c14e7
# ╟─fa6144a0-3a72-11eb-0a71-018f50186e73
# ╟─54108498-3a70-11eb-192d-7b2f5d535135
# ╟─9889b41e-3a70-11eb-0321-dd32b90c542f
# ╟─41e0cf1c-3a7a-11eb-1b6c-519ac78d7bd5
# ╟─75e73fdc-3a78-11eb-2456-bd336b501dfe
# ╟─e5450594-3a78-11eb-1d7b-e55a8bfff409
# ╟─13fc1260-3a79-11eb-0bcc-e96fed3d7fc3
# ╟─26f220c6-3a79-11eb-39db-b53e700fc0d0
# ╟─867b04e8-3a79-11eb-1f0d-b3e8437f97ac
# ╟─b0600344-3a79-11eb-3c2f-3d00f3a6d705
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment