# The optimized numbers of variables and clauses to encode a graph coloring problem in CNF

## Problem Statement

Given a finite graph $$G = \langle V, E\rangle$$, consisting of vertice set $$V$$ and edge set $$E$$, and a finite set of colors $$C$$, a problem instance of graph coloring is to assign each vertex $$v \in V$$ a $$\text{color} (v) \in C$$ such that $$\forall \langle v, w\rangle \in E, \text{color}(v) \not= \text{color}(w)$$. Now we encode an instance of graph coloring problem into a CNF (conjunctive normal formula) $$F$$.

Note: The word "encode" means that we'll know a graph coloring problem if a CNF is given, and also will know a CNF if a graph coloring problem is given.

• What is the minimal number of propositional variables in $$F$$?
• What is the minimal number of clauses in $$F$$?

## Original Version

A solution to a graph coloring problem is an assignment of colors to vertices such that no two adjacent vertices have the same color. Formally, a finite graph $$G = \langle V, E\rangle$$ consists of vertices $$V = \{v_1, \cdots, v_n\}$$ and edges $$E = \{ \langle v_{i_1} , w_{i_1} \rangle , \cdots , \langle v_{i_k} , w_{i_k} \rangle \}$$. The finite set of colors is given by $$C = \{c_1, \cdots , c_m \}$$. A problem instance is given by a graph and a set of colors: the problem is to assign each vertex $$v \in V$$ a $$\text{color}(v) \in C$$ such that for every edge $$\langle v, w\rangle \in E$$, $$\text{color}(v) \not= \text{color}(w)$$. Clearly, not all instances have solutions.

Show how to encode an instance of a graph coloring problem into a PL formula $$F$$. $$F$$ should be satisfiable iff a graph coloring exists.

1. Describe a set of constraints in PL asserting that every vertex is colored. Since the sets of vertices, edges, and colors are all finite, use notation such as “$$\text{color}(v) = c$$” to indicate that vertex $$v$$ has color $$c$$. Realize that such an assertion is encodeable as a single propositional variable $$P^c_v$$.
2. Describe a set of constraints in PL asserting that every vertex has at most one color.
3. Describe a set of constraints in PL asserting that no two connected vertices have the same color.
4. Identify a significant optimization in this encoding. Hint: Can any constraints be dropped? Why?
5. If the constraints are not already in CNF, specify them in CNF now. For $$N$$ vertices, $$K$$ edges, and $$M$$ colors, how many variables does the optimized encoding require? How many clauses?

As suggested by @D.W.♦, I copy the original problem here (above is the version simplified by me). This original version is Exercise 1.6 from:

Bradley, A. and Manna, Z. (2007). The Calculus of Computation. Dordrecht: Springer, p.34.

## My Analysis

The optimized CNF within my ability is to use propositional variable $$P_v^c$$ to indicate that $$\text{color}(v) = c$$. Here we can only use at most $$|V|$$ colors of all colors, i.e., the number of colors in our design of propositional variables is $$|V|\min (|V|, |C|)$$. Then we can build a CNF: $$F_0 = \bigwedge_{v \in V} (\bigvee_{c \in C} P_v^c) \wedge \bigwedge_{v \in V} (\bigvee_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \vee \neg P_v^{c_2})) \land \bigwedge_{c \in C \\ \langle v, w\rangle \in E} (\neg P_v^c \vee \neg P_w^c)$$

In this variable, there're $$|V| \min (|V|, |C|)$$ propositional variables and $$2|V| + |C||E|$$ clauses.

I failed to prove $$F_0$$ is the CNF with neither the least propositional variables nor the least clauses. Is there an another CNF $$F'$$ with less propostional variables or less clauses? How to find the minimal number of propositional variables and clauses of legal CNFs?

• If the 2nd group of terms in $F_0$ is supposed to rule out that a vertex has 2 or more colors, shouldn't the term be $(\bigwedge_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \vee \neg P_v^{c_2}))$ ( instead of $(\bigvee_{c_1 \not= c_2 \in C} (\neg P_v^{c_1} \wedge \neg P_v^{c_2}))$ ) ? As it stands the duplicity check passes iff for a given vertex there exist 2 [amongst all] colors that are not assigned to that vertex. What you want is that for each triple of vertex and 2 different colors, [at least] one color is not assigned to the vertex. Sep 27, 2019 at 15:40

The problem statement needs to be specified more precisely to be meaningful.

If I'm being pedantic, I would say that the minimum number of propositional variables is zero: you can solve the graph coloring problem (taking exponential time if necessary), then either use the formula $$\text{True}$$ or $$\text{False}$$ according to whether the graph is $$C$$-colorable or not. I suspect this isn't what you're looking for, so you probably need to define the problem statement more carefully to be able to answer the question in a useful way. For instance, perhaps you need to specify exactly what properties you want $$F$$ to have.

• Thanks for your answer. I've edited my problem. In the language of set theory, what I want to ask is to find a set of CNFs so that there's a bijection between the set of CNFs and the set of graph coloring problems. Is that clear enough? Sep 28, 2019 at 2:40
• And, appologize for my typo of the number propositional variables. In fact, I use $|V| \min (|V|, |C|)$ propositional variables in designed CNF. Sep 28, 2019 at 2:56
• @namasikanam, That doesn't seem sufficient. I suspect you want some additional properties, such as satisfiability of the CNF is related to colorability of the graph, or that any satisfying assignment somehow can be used to construct a coloring of the graph (but in polynomial time? or is exponential time ok?), or something.
– D.W.
Sep 28, 2019 at 4:46
• Thanks for comment. In fact I'm not sure whether additional properties are necessary. It's just an exercise of my textbook! Can you give some answer with any additional properties needed? I'll try to email the author, Prof. Bradley in Stanford University, for clarification. Sep 28, 2019 at 8:15
• @namasikanam, good idea. One can encode a graph coloring problem using $2 |E| \lg |V| + \lg |C|$ bits, so if we don't need the CNF to have any properties (e.g., its satisfiability must be related to the colorability of the graph), then you could encode from there to any family of at least $2^{2 |E| \lg |V| + \lg |C|}$ formulas. For instance, there are $\ge 2^{2^n}$ CNF formulas on $n$ variables, so $\lg (2 |E| \lg |V| + \lg |C|)$ variables should suffice. I question whether this is useful or what is intended, though.
– D.W.
Sep 29, 2019 at 4:05

I think optimization is we can drop the second constraint in PL formula. If a node is assigned with multiple colors, we can just have to pick one color, as they will all satisfy the edge constraints. So F is satisfiable iff a graph coloring exists.