Boolean Satisfiability Problem

Overview

The Boolean Satisfiability Problem (SAT) determines whether there exists an assignment of truth values to variables that makes a given Boolean formula evaluate to true.

This example demonstrates:

Formulating a SAT problem in Conjunctive Normal Form (CNF)
Converting it to a tensor network
Finding satisfying assignments
Counting satisfiable solutions

We'll work with a CNF formula consisting of multiple clauses.

using GenericTensorNetworks, GenericTensorNetworks.ProblemReductions

Define boolean variables

@bools a b c d e f g

Create a CNF formula: (a ∨ b ∨ ¬d ∨ ¬e) ∧ (¬a ∨ d ∨ e ∨ ¬f) ∧ (f ∨ g) ∧ (¬b ∨ c)

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)

Manual Verification

For small problems, we can manually find and verify a satisfying assignment:

assignment = Dict([:a=>true, :b=>false, :c=>false, :d=>true, :e=>false, :f=>false, :g=>true])

Dict{Symbol, Bool} with 7 entries:
  :a => 1
  :b => 0
  :f => 0
  :d => 1
  :e => 0
  :c => 0
  :g => 1

Check if this assignment satisfies the formula:

satisfiable(cnf, assignment)

true

Tensor Network Formulation

Define the satisfiability problem:

sat = Satisfiability(cnf)

Satisfiability{Symbol, Int64, UnitWeight, ProblemReductions.EXTREMA}([:a, :b, :d, :e, :f, :g, :c], [1, 1, 1, 1], (a ∨ b ∨ ¬d ∨ ¬e) ∧ (¬a ∨ d ∨ e ∨ ¬f) ∧ (f ∨ g) ∧ (¬b ∨ c))

The objective is to maximize the number of satisfied clauses:

objectives(sat)

4-element Vector{ProblemReductions.LocalSolutionSize{Int64}}:
 LocalSolutionSize{Int64} on [1, 2, 3, 4]
┌───────────────┬──────┐
│ Configuration │ Size │
├───────────────┼──────┤
│ [0, 0, 0, 0]  │  1   │
│ [1, 0, 0, 0]  │  1   │
│ [0, 1, 0, 0]  │  1   │
│ [1, 1, 0, 0]  │  1   │
│ [0, 0, 1, 0]  │  1   │
│ [1, 0, 1, 0]  │  1   │
│ [0, 1, 1, 0]  │  1   │
│ [1, 1, 1, 0]  │  1   │
│ [0, 0, 0, 1]  │  1   │
│ [1, 0, 0, 1]  │  1   │
│ [0, 1, 0, 1]  │  1   │
│ [1, 1, 0, 1]  │  1   │
│ [0, 0, 1, 1]  │  0   │
│ [1, 0, 1, 1]  │  1   │
│ [0, 1, 1, 1]  │  1   │
│ [1, 1, 1, 1]  │  1   │
└───────────────┴──────┘

 LocalSolutionSize{Int64} on [1, 3, 4, 5]
┌───────────────┬──────┐
│ Configuration │ Size │
├───────────────┼──────┤
│ [0, 0, 0, 0]  │  1   │
│ [1, 0, 0, 0]  │  1   │
│ [0, 1, 0, 0]  │  1   │
│ [1, 1, 0, 0]  │  1   │
│ [0, 0, 1, 0]  │  1   │
│ [1, 0, 1, 0]  │  1   │
│ [0, 1, 1, 0]  │  1   │
│ [1, 1, 1, 0]  │  1   │
│ [0, 0, 0, 1]  │  1   │
│ [1, 0, 0, 1]  │  0   │
│ [0, 1, 0, 1]  │  1   │
│ [1, 1, 0, 1]  │  1   │
│ [0, 0, 1, 1]  │  1   │
│ [1, 0, 1, 1]  │  1   │
│ [0, 1, 1, 1]  │  1   │
│ [1, 1, 1, 1]  │  1   │
└───────────────┴──────┘

 LocalSolutionSize{Int64} on [5, 6]
┌───────────────┬──────┐
│ Configuration │ Size │
├───────────────┼──────┤
│    [0, 0]     │  0   │
│    [1, 0]     │  1   │
│    [0, 1]     │  1   │
│    [1, 1]     │  1   │
└───────────────┴──────┘

 LocalSolutionSize{Int64} on [2, 7]
┌───────────────┬──────┐
│ Configuration │ Size │
├───────────────┼──────┤
│    [0, 0]     │  1   │
│    [1, 0]     │  0   │
│    [0, 1]     │  1   │
│    [1, 1]     │  1   │
└───────────────┴──────┘

Convert to tensor network representation:

problem = GenericTensorNetwork(sat)

GenericTensorNetwork{Satisfiability{Symbol, Int64, UnitWeight, ProblemReductions.EXTREMA}, OMEinsum.DynamicNestedEinsum{Int64}, Int64}
- open vertices: Int64[]
- fixed vertices: Dict{Int64, Int64}()
- contraction time = 2^5.248, space = 2^2.0, read-write = 2^5.728

Mathematical Background

For each boolean variable x, we assign a degree of freedom $s_x ∈ \{0,1\}$, where:

0 represents the value 'false'
1 represents the value 'true'

Each clause is mapped to a tensor. For example, the clause ¬x ∨ y ∨ ¬z becomes a tensor labeled by $(s_x, s_y, s_z)$:

\[C_{s_x,s_y,s_z} = \begin{cases} 0 & \text{if } s_x = 1, s_y = 0, s_z = 1 \\ 1 & \text{otherwise} \end{cases}\]

Only the configuration $(s_x, s_y, s_z) = (1, 0, 1)$ makes this clause unsatisfied.

Solution Analysis

1. Satisfiability Check

Find the maximum number of clauses that can be satisfied:

num_satisfiable = solve(problem, SizeMax())[]

4.0ₜ

2. Counting Solutions

The graph polynomial counts assignments by number of satisfied clauses:

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

3. Finding a Satisfying Assignment

Find one satisfying assignment:

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

Convert the bit vector to a variable assignment and verify:

solution_assignment = Dict(zip(ProblemReductions.symbols(problem.problem), single_config))
satisfiable(cnf, solution_assignment)

true

More APIs

The Independent Set Problem chapter has more examples on how to use the APIs.

This page was generated using Literate.jl.