Evolution in Networks and Computer Communications |
Foundation of Computer Science USA |
ENCC - Number 1 |
None 2011 |
Authors: Prakash C. Sharma, Narendra S. Chaudhari |
927fb9b3-4f6e-4092-b462-3d4a4627ef5e |
Prakash C. Sharma, Narendra S. Chaudhari . Polynomial 3-SAT Encoding for K-Colorability of Graph. Evolution in Networks and Computer Communications. ENCC, 1 (None 2011), 19-24.
Graph k-Colorability (for k ≥ 3) Problem (GCP) is an well known NP-Complete problem; till now there are not any known deterministic methods that can solve a GCP in a polynomial time. To solve this efficiently, we go through Propositional Satisfiability, which is the first known NP-Complete problem [3]. However, to use the SAT solvers, there is a need to convert or encode an k-colorable graph to 3-SAT first. In this paper, we are presenting a polynomial 3-SAT encoding technique for k-colorability of graph. Alexander Tsiatas [1] gave a reduction approach from 3-Colorable graph to 3-SAT encoding. According to [1], total number of clauses generated in 3-CNF-SAT formula for 3-colorable graph G = (V, E) is ((27*|V|) + (256*|E|)). In our earlier formulation of reduction of k-colorable graph to 3-SAT [2], we generalized [1] for k-colorable graph and generated ((kk*(k-2)*|V|) + (22k+2 *|E|)) clauses in 3-CNF. Here, we present our approach to encode a k-colorable graph to 3-CNF-Satisfiability (SAT) formula in polynomial time with mathematical proof. Our formulation generates total (((k-2)*|V| ) + (k*|E|) ) clauses in 3-CNF for k-colorable graph. Thus, our formulation is better than approach [1] and [2]. Also, we tested our encoding formulation approach on different graph coloring instances of DIMACS[8][9].