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.
- 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$.
- Describe a set of constraints in PL asserting that every vertex has at most one color.
- Describe a set of constraints in PL asserting that no two connected vertices have the same color.
- Identify a significant optimization in this encoding. Hint: Can any constraints be dropped? Why?
- 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?
