GCP Constraint Based SAT Clause Generation in Polynomial Time

Main Article Content

Nidhi Dahale
N.S. Chaudhari, Maya Ingle


Graph Colorability Problem (GCP) belongs to a subset of the large family of NP–Hard combinatorial problems. Till now there exist very less deterministic methods to find the solutions to k- Color problem. Constraint analysis of the k-Color problem and formulating the constraints to the SAT clauses provides another way to find the solution to this typical problem. The recent advancement in the development of SAT solvers has really provided an easy approach to find the truth values for a SAT formula. Thus, we have performed the formulations of the constraints of GCP into ALOC, AMOC and DCOL clauses. With our formulations, we are able to generate the SAT clauses in polynomial time. The total SAT clauses that are being generated with our formulations are | V | + | V |* k*(k-1) / 2 + (m*E).


Keywords: SAT, Graph Coloring, Encodings, Clauses, Polynomial Time


Download data is not yet available.

Article Details