Satisfiability problem

Problem definition

In logic and computer science, the boolean satisfiability problem is the problem of determining if there exists an interpretation that satisfies a given boolean formula. One can specify a satisfiable problem in the 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 GenericTensorNetworks

@bools a b c d e f g

cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c))

(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)

true

Generic tensor network representation

We can use Satisfiability to construct the tensor network for solving the satisfiability problem as

sat = Satisfiability(cnf)

Satisfiability{Symbol, UnitWeight}((a ∨ b ∨ ¬d ∨ ¬e) ∧ (¬a ∨ d ∨ e ∨ ¬f) ∧ (f ∨ g) ∧ (¬b ∨ c), UnitWeight())

The tensor network representation of the satisfiability problem can be obtained by

problem = GenericTensorNetwork(sat)

GenericTensorNetwork{Satisfiability{Symbol, UnitWeight}, OMEinsum.DynamicNestedEinsum{Symbol}, Symbol}(Satisfiability{Symbol, UnitWeight}((a ∨ b ∨ ¬d ∨ ¬e) ∧ (¬a ∨ d ∨ e ∨ ¬f) ∧ (f ∨ g) ∧ (¬b ∨ c), UnitWeight()), f, f-g -> 
├─ b-f, b-c -> f
│  ├─ a-b-d-e, a-d-e-f -> b-f
│  │  ├─ a-b-d-e
│  │  └─ a-d-e-f
│  └─ b-c
└─ f-g
, Dict{Symbol, Int64}())

Theory (can skip)

We can construct a Satisfiability 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)$.

\[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.

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())[]

4.0ₜ

The GraphPolynomial of a satisfiability problem counts the number of solutions that k clauses satisfied.

num_satisfiable_count = read_size_count(solve(problem, GraphPolynomial())[])

5-element Vector{Pair{Int64, BigInt}}:
 0 => 0
 1 => 0
 2 => 12
 3 => 56
 4 => 60

Find one of the solutions

single_config = read_config(solve(problem, SingleConfigMax())[])

1111111

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

true

This page was generated using Literate.jl.