update sat docs

Author: GiggleLiu

docs/src/ref.md

@@ -9,6 +9,7 @@ Matching
 Coloring
 MaxCut
 PaintShop
+Satisfiability
 ```
 
 ```@docs

examples/Coloring.jl

@@ -29,17 +29,17 @@ show_graph(graph; locs=locations)
 # For a vertex ``v``, we define the degree of freedoms ``c_v\in\{1,2,3\}`` and a vertex tensor labelled by it as
 # ```math
 # W(v) = \left(\begin{matrix}
-#     r_v\\
-#     g_v\\
-#     b_v
+#     1\\
+#     1\\
+#     1
 # \end{matrix}\right).
 # ```
 # For an edge ``(u, v)``, we define an edge tensor as a matrix labelled by ``(c_u, c_v)`` to specify the constraint
 # ```math
 # B = \left(\begin{matrix}
-#     0 & 1 & 1\\
-#     1 & 0 & 1\\
-#     1 & 1 & 0
+#     1 & x & x\\
+#     x & 1 & x\\
+#     x & x & 1
 # \end{matrix}\right).
 # ```
 # The number of possible colouring can be obtained by contracting this tensor network by setting vertex tensor elements ``r_v, g_v`` and ``b_v`` to 1.

examples/Satisfiability.jl

@@ -24,18 +24,37 @@ assignment = Dict([:a=>true, :b=>false, :c=>false, :d=>true, :e=>false, :f=>fals
 
 satisfiable(cnf, assignment)
 
-# We can contruct a [`Satisfiability`](@ref) problem to solve the above problem more cleverly.
+# ## Tensor network representation
+# We can contruct a [`Satisfiability`](@ref) problem to solve the above problem.
+# To generate a tensor network, we map a boolean variable ``x`` and its negation ``\neg x`` to a degree of freedom (label) ``s_x \in \{0, 1\}``,
+# where 0 stands for variable ``x`` having value `false` while 1 stands for having value `true`.
+# Then we map a clause to a tensor. For example, a clause ``¬x ∨ y ∨ ¬z`` can be mapped to a tensor labeled by ``(s_x, s_y, s_z)``.
+# ```math
+# C = \left(\begin{matrix}
+# \left(\begin{matrix}
+# x & x \\
+# x & x
+# \end{matrix}\right) \\
+# \left(\begin{matrix}
+# x & x \\
+# 1 & x
+# \end{matrix}\right)
+# \end{matrix}\right).
+# ```
+# There is only one entry ``(s_x, s_y, s_z) = (1, 0, 1)`` that makes this clause unsatisfied.
+# If we contract this tensor network, we will get a multiplicative factor ``x`` whenever there is a clause satisfied.
 
 problem = Satisfiability(cnf);
 
-# ## Satisfiability and its counting
+# ## Solving properties
+# #### 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
+# #### Find one of the solutions
 single_config = solve(problem, SingleConfigMax())[].c.data
 
 # One will see a bit vector printed.