Call for Paper - August 2022 Edition
IJCA solicits original research papers for the August 2022 Edition. Last date of manuscript submission is July 20, 2022. Read More

Polynomial 3-SAT Encoding for K-Colorability of Graph

Evolution in Networks and Computer Communications
© 2011 by IJCA Journal
Number 1 - Article 4
Year of Publication: 2011
Prakash C. Sharma
Narendra S. Chaudhari

Prakash C Sharma and Narendra S Chaudhari. Polynomial 3-SAT Encoding for K-Colorability of Graph. IJCA Special Issue on Evolution in Networks and Computer Communications (1):19-24, 2011. Full text available. BibTeX

	author = {Prakash C. Sharma and Narendra S. Chaudhari},
	title = {Polynomial 3-SAT Encoding for K-Colorability of Graph},
	journal = {IJCA Special Issue on Evolution in Networks and Computer Communications},
	year = {2011},
	number = {1},
	pages = {19-24},
	note = {Full text available}


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].


  1. Alexander Tsiatas, “Phase Transitions in Boolean Satisfiability and Graph Coloring”, May 2008, Department of Computer Science, Cornell University, (
  2. Prakash C. Sharma and Narendra S. Chaudhari, “A Graph Coloring Approach for Channel Assignment in Cellular Network via Propositional Satisfiability” International Conference on Emerging Trends in Networks and Computer Communications (ETNCC) at Udaipur , 22-24 April 2011, pp 23-26
  3. Garey, M. R. and Johnson, D. S., Computers and Interactability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979.
  4. Daniel Marx, “Graph Colouring Problems and their applications in Scheduling”, Periodica Polytechnica Ser El. Eng Vol.48, No.1, pp. 11-16 (2004)
  5. Maaly A. Hassan and Andrew Chickadel, “A Review Of Interference Reduction In Wireless Networks Using Graph Coloring Methods” , International journal on applications of graph theory in wireless ad hoc networks and sensor networks (GRAPH-HOC) Vol.3, No.1, March 2011, pp 58-67.
  6. Mohammad Malkawi, Mohammad Al-Haj Hassan and Osama Al-Haj Hassan, “New Exam Scheduling Algorithm using Graph Coloring”, The International Arab Journal of Information Technology, Vol. 5, No. 1, January 2008, pp 80-87
  7. Koen Claessen, Niklas Een, Mary Sheeran and Niklas Sorensson, “SAT-solving in practice”, Proceedings of the 9th International Workshop on Discrete Event Systems Goteborg, Sweden, pp 61-67,May 28-30, 2008.
  8. Graph Coloring Instances, available at
  9. DIMACS Implementation Challenges, available at http://dimacs.rutgers .edu/Challenges/