logic.jl

### 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