Chromatic Polynomials 11 – Boolean Satisfiability

I keep touting CPs as a language of logic. Let’s see how well that claim holds up by comparing it to a well-established language of logic, Boolean Satisfiability (or “SAT”).

SAT Introduction

A SAT expression is an expression containing multiple Boolean variables, e.g. x₁, x₂, x₃, etc., where each variable can be true or false (often “0” and “1” are used in place of false and true). An expression is satisfiable if there are values for its variables which result in the expression evaluating to true. The simplest possible expression consists of a single variable, e.g. x, and is satisfiable if and only if x is true. The expression can also contain the following operators:

NOT, ¬: The expression ¬x₁ is satisfiable if x₁ is false.

AND, ˄: The expression x₁ ˄ x₂ is satisfiable if and only if x₁ and x₂ are both true.

OR,˅: The expression x₁ ˅ x₂ is satisfiable if either x₁ or x₂ are true.

These operations are combined to form more complex logical expressions:

(x₁ ˅ ¬x₃) ˄ ¬(x₁ ˅ x₂)

This expression is only satisfiable if x₁, x₂, and x₃ are all false.

As with all good languages of logic, DeMorgan’s laws apply:

¬(x₁ ˅ x₃) = ¬x₁ ˄ ¬x₂

¬(x₁ ˄ x₂) = ¬x₁ ˅ ¬x₂

This is only the briefest possible introduction to SAT problems. There are many variants to SAT problems and an entire field of mathematics dedicated to their study. SAT is a true language of logic.

Translating SAT expressions to CPs

Every SAT expression can be converted to a Chromatic Polynomial, with a few simple transformations:

A single variable must be converted to a Kronecker Delta comparing a vertex to true. For brevity, I’ll use 0 and 1 for false and true:

x₁  =>  δ_σ1{1}

The B-SAT NOT operation is converted to the CP NOT expression, (1 - …):

¬x₁  =>  (1 - δ_σ1{1})

Note that if the expression being negated is a single variable, then it can be converted to comparing the vertex to 0 instead of 1:

¬x₁  =>  δ_σ1{0}

The SAT AND operation is converted to the product of the AND operands:

x₁ ˄ x₂  =>  δ_σ1{1} δ_σ2{1}

Note that the rules for multiplying EKDs allow us to reduce this example to:

x₁ ˄ x₂  =>  δ_σ1σ2{1}

The B-SAT OR operation is converted to the CP OR expression:

x₁ ˅ x₂  =>  1 - δ_σ1{0}δ_σ2{0}

which can be reduced to:

x₁ ˅ x₂  =>  1 - δ_σ1σ2{0}

Note that this makes use of DeMorgan’s laws, since a direct translation to addition, δ_σ1{1} + δ_σ2{1}, is only correct if the two terms are mutually exclusive.

Here is a sample SAT expression:

(x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁

The solution requires us to find values for x₁, x₂, and x₃ such that the expression is true. By visual inspection, we can see that the final term, ¬x₁, requires that x₁ is false. If x₁ is false, then x₂ must be false for (x₁ ∨ ¬x₂) to be true. The middle term, (¬x₁ ∨ x₂ ∨ x₃), is true because ¬x₁ is true, leaving no constraints on x₃. Thus, we have two solutions:

x₁ = false, x₂ = false, x₃ = false

and

x₁ = false, x₂ = false, x₃ = true

We can translate this expression directly to CPs with the following operators:

x₁ becomes δσ₁{1}

¬x₁ becomes δσ₁{0}. Note that we could also use (1 - δσ₁{1}), but this creates extra terms and slows down processing.

(A ∧ B) becomes AB

(A ∨ B) becomes either (1 – (1 – A)(1 – B)) or (A + B - AB). The first form is more preferred, since it is easier to expand to more terms.

Translating the sample SAT expression to CPs gives us:

(1 - (1 - δσ₁{1}) (1 - δσ₂{0})) (1 - (1 - δσ₁{0}) (1 - δσ₂{1}) (1 - δσ₃{1})) * δσ₁{0}

Summing the CP’s vertices from 0 to 1 will show us that there are 2 solutions.

Solving Satisfiability CPs

To find solutions, we use the same Solution method we used to solve logic puzzles – try a value for a vertex. If the sum is 0, then no solutions have that vertex set to that value. If the sum is 1 or more, we can save that value for that vertex and continue to find solution values for the other vertices.

Simplifying before Summing

Since the previous article showed how we can save work by simplifying before summing, let’s try that with this SAT-to-CP example. We can reduce the CP by replacing (1 - δσ_n{0}) with δσ_n{1} and (1 - δσ_n{1}) with δσ₂{0}.

(1 - δσ₁{0}*δσ₂{1}) (1 - δσ₁{1} δσ₂{0} δσ₃{0}) δσ₁{0}

We can combine EKDs that share a single constant, replacing δσ₂{0} * δσ₃{0} with δσ₂σ₃{0}:

(1 - δσ₁{0}*δσ₂{1}) (1 - δσ₁{1} δσ₂σ₃{0}) * δσ₁{0}

We can combine EKDs that share a single constant, replacing δσ₂{0} * δσ₃{0} with δσ₂σ₃{0}:

(1 - δσ₁{0}*δσ₂{1}) (1 - δσ₁{1} δσ₂σ₃{0}) * δσ₁{0}

We can find even more simplifications by expanding the terms. Let us expand the last two expressions, (1 - δσ₁{1} δσ₂σ₃{0}) δσ₁{0}, to:

δσ₁{0} - δσ₁{0} δσ₁{1} δσ₂σ₃{0}

We know that δσ₁{0} * δσ₁{1} yields 0, leaving us with:

δσ₁{0} - 0 * δσ₂σ₃{0}

δσ₁{0}

Plugging this back into the original CP gives us:

(1 - δσ₁{0}*δσ₂{1}) * δσ₁{0}

Expanding that produces:

δσ₁{0} - δσ₁{0}*δσ₂{1}

δσ₁{0} * (1 - δσ₂{1})

δσ₁{0} * δσ₂{0}

δσ₁σ₂{0}

This expression is so simple that we do not need to sum it. We can see that σ₁ and σ₂ must be 0. Since there is no restriction placed on σ₃, it can be either 0 or 1. This gives us two solutions.

There is a lot more to SAT problems than I have shown here – it’s a field of study that someone could dedicate their entire career to. My goal isn’t to provide an exhaustive tour of SAT, but to show that SAT problems can be translated to CPs and solved through CP evaluation.

Previous Post:

www.solutionslookingforproblems.com

Chromatic Polynomials 10 – Simplifying Before Summing

There are a few ways to simplify a CP before summing it.Replacing a Vertex with a ConstantIf the entire CP is multiplied by a term that constrains a svertex to a single constant, e.g. δσ5{2}, we can remove that term and instead replace all instances of σ5 with the constant 2. Examples:δσ5{2}(1 - δσ4σ5)       becomes        (1 - δσ4{2})δσ5{2}δσ4σ5σ6            becomes        δσ4σ6{2}δσ5{2}δσ4σ5{2-5}        becomes        δσ4{2}δσ5σ6{2}δσ4σ5σ6{2-5} becomes        δσ4{2}δσ5{2}δσ5{2-5}            be

Next Post:

Chromatic Polynomials 12 - coming soon.