new sat doc

Author: GiggleLiu

docs/make.jl

@@ -36,6 +36,7 @@ makedocs(;
             "Matching problem" => "tutorials/Matching.md",
             "Binary paint shop problem" => "tutorials/PaintShop.md",
             "Coloring problem" => "tutorials/Coloring.md",
+            "Satisfiability problem" => "tutorials/Satisfiability.md",
             "Other problems" => "tutorials/Others.md",
         ],
         "Performance Tips" => "performancetips.md",

examples/Coloring.jl

@@ -49,7 +49,7 @@ problem = Coloring{3}(graph);
 
 # ## Solving properties
 # ##### counting all possible coloring
-num_of_coloring = solve(problem, CountingAll())[]
+num_of_coloring = solve(problem, CountingMax())[]
 
 # ##### finding one best coloring
 single_solution = solve(problem, SingleConfigMax())[]
@@ -70,6 +70,7 @@ show_graph(linegraph; locs=[0.5 .* (locations[e.src] .+ locations[e.dst])
 # Let us construct the tensor network and see if there are solutions.
 lineproblem = Coloring{3}(linegraph);
 
-num_of_coloring = solve(lineproblem, CountingAll())[]
+num_of_coloring = solve(lineproblem, CountingMax())[]
 
-# You will see a zero printed, meaning no solution for the 3-coloring on edges of a Petersen graph.
+# You will see the maximum size 28 is smaller than the number of edges in the `linegraph`,
+# meaning no solution for the 3-coloring on edges of a Petersen graph.

examples/Satisfiability.jl

@@ -9,3 +9,35 @@
 #     * how to compute weighted graphs and handle open vertices.
 
 # ## Problem definition
+# One can specify a satisfiable problem in the [conjuctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form).
+# In boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction (∧) of one or more clauses,
+# where a clause is a disjunction (∨) of literals.
+using GraphTensorNetworks
+
+@bools a b c d e f g
+
+cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c))
+
+# To goal is to find an assignment to satisfy the above CNF.
+# For a satisfiability problem at this size, we can find the following assignment to satisfy this assignment manually.
+assignment = Dict([:a=>true, :b=>false, :c=>false, :d=>true, :e=>false, :f=>false, :g=>true])
+
+satisfiable(cnf, assignment)
+
+# We can contruct a [`Satisfiability`](@ref) problem to solve the above problem more cleverly.
+
+problem = Satisfiability(cnf);
+
+# ## Satisfiability and its counting
+# The size of a satisfiability problem is defined by the number of satisfiable clauses.
+num_satisfiable = solve(problem, SizeMax())[]
+
+# The [`GraphPolynomial`](@ref) of a satisfiability problem counts the number of solutions that `k` clauses satisfied.
+num_satisfiable_count = solve(problem, GraphPolynomial())[]
+
+# ## Find one of the solutions
+single_config = solve(problem, SingleConfigMax())[].c.data
+
+# One will see a bit vector printed.
+# One can create an assignment and check the validity with the following statement:
+satisfiable(cnf, Dict(zip(labels(problem), single_config)))

src/arithematics.jl

@@ -282,6 +282,7 @@ Base.zero(::ConfigSampler{N,S,C}) where {N,S,C} = zero(ConfigSampler{N,S,C})
 Base.one(::ConfigSampler{N,S,C}) where {N,S,C} = one(ConfigSampler{N,S,C})
 
 # tree config enumerator
+# it must be mutable, otherwise the `IdDict` trick for computing the length does not work.
 """
     TreeConfigEnumerator{N,S,C} <: AbstractSetNumber
 
@@ -339,7 +340,6 @@ julia> one(s)
 
 ```
 """
-# it must be mutable, otherwise the `IdDict` trick for computing the length does not work.
 mutable struct TreeConfigEnumerator{N,S,C} <: AbstractSetNumber
     tag::TreeTag
     data::StaticElementVector{N,S,C}

src/interfaces.jl

@@ -286,18 +286,15 @@ post_invert_exponent(t::TropicalNumbers.TropicalTypes) = inv(t)
 Returns the maximum size of the graph problem. 
 A shorthand of `solve(problem, SizeMax(); usecuda=false)`.
 """
-function max_size end
+max_size(m::GraphProblem; usecuda=false) = Int(sum(solve(m, SizeMax(); usecuda=usecuda)).n)  # floating point number is faster (BLAS)
+
 """
     max_size_count(problem; usecuda=false)
 
 Returns the maximum size and the counting of the graph problem.
 It is a shorthand of `solve(problem, CountingMax(); usecuda=false)`.
 """
-function max_size_count end
-for TP in [:MaximalIS, :IndependentSet, :Matching, :MaxCut, :PaintShop]
-    @eval max_size(m::$TP; usecuda=false) = Int(sum(solve(m, SizeMax(); usecuda=usecuda)).n)  # floating point number is faster (BLAS)
-    @eval max_size_count(m::$TP; usecuda=false) = (r = sum(solve(m, CountingMax(); usecuda=usecuda)); (Int(r.n), Int(r.c)))
-end
+max_size_count(m::GraphProblem; usecuda=false) = (r = sum(solve(m, CountingMax(); usecuda=usecuda)); (Int(r.n), Int(r.c)))
 
 using DelimitedFiles
 

src/networks/Coloring.jl

@@ -26,20 +26,20 @@ labels(gp::Coloring) = [1:gp.nv...]
 function generate_tensors(x::T, c::Coloring{K}) where {K,T}
     ixs = getixsv(c.code)
     return add_labels!(map(1:length(ixs)) do i
-        i <= c.nv ? coloringv(x, K) .^ get_weights(c, i) : coloringb(T, K)
+        i <= c.nv ? coloringv(T, K) .^ get_weights(c, i) : coloringb(x, K)
     end, ixs, labels(c))
 end
 
 # coloring bond tensor
-function coloringb(::Type{T}, k::Int) where T
-    x = ones(T, k, k)
+function coloringb(x::T, k::Int) where T
+    x = fill(x, k, k)
     for i=1:k
-        x[i,i] = zero(T)
+        x[i,i] = one(T)
     end
     return x
 end
 # coloring vertex tensor
-coloringv(x::T, k::Int) where T = fill(x, k)
+coloringv(::Type{T}, k::Int) where T = fill(one(T), k)
 
 # utilities
 """

src/networks/Satisfiability.jl

@@ -1,3 +1,9 @@
+"""
+    BoolVar{T}
+    BoolVar(name, neg)
+
+Boolean variable for constructing CNF clauses.
+"""
 struct BoolVar{T}
     name::T
     neg::Bool

test/networks/Coloring.jl

@@ -6,11 +6,11 @@ using Test, GraphTensorNetworks, Graphs
         add_edge!(g, i, j)
     end
     code = Coloring{3}(g; optimizer=GreedyMethod())
-    res = solutions(code, CountingTropical{Float64,Float64}; all=true)[]
+    res = best_solutions(code; all=true)[]
     @test length(res.c.data) == 12
     g = smallgraph(:petersen)
     code = Coloring{3}(g; optimizer=GreedyMethod())
-    res = solutions(code, CountingTropicalF64; all=true)[]
+    res = best_solutions(code; all=true)[]
     @test length(res.c.data) == 120
 
     c = solve(code, SingleConfigMax())[]