Stochastic Learning for SAT- Encoded Graph Coloring Problems

1. Introduction

In the graph coloring problem (GCP) an undirected graph G(V, E) is given, where V is a set of vertices, and E is a set of pairs of vertices called edges. We call a k-coloring of G, a mapping such that if C(p) = C(q) then . The set is the set of colors. There exist two variants of this problem. In the optimization variant, the goal is to find the chromatic number , which is the minimal k for which there exists a k-coloring of G. In the decision variant, the question is to decide whether for a particular number of colors, a coloring of G exists. All these problems are known to be NP-complete, so it is unlikely that a polynomial-time algorithm exists that solves any of these problems.

In this paper the focus is on the decision variant of the GCP. Encoding the GCP as a Boolean satisfiability problem (SAT) and solving it using efficient SAT algorithms has caused considerable interest. The SAT problem, which is known to be NP-complete (Cook, 1971), can be defined as follows. A propositional formulawith m clauses and n Boolean variables is given. A Boolean variable is a variable that can take one of the two values, True or False. Each clause , in turn, has the form:,where and denotes the negation of . The task is to determine whether the propositional formula evaluates to True. Such an assignment, if it exists, is called a satisfying assignment for , and is called satisfiable. Otherwise, is said to be unsatisfiable. Most SAT solvers use a Conjunctive Normal Form (CNF) representation of the propositional formula. In CNF, the formula is represented as a conjunction of clauses, where each clause is a disjunction of literals, and a literal is a Boolean variable or its negation. For example, is a clause containing the two literals and . This clause is satisfied if either is True or is True. When each clause in contains exactly literals, the resulting SAT problem is called k-SAT.