Stochastic Learning for SAT- Encoded Graph Coloring Problems

Stochastic Learning for SAT- Encoded Graph Coloring Problems

Noureddine Bouhmala (Vestfold University College, Norway) and Ole-Christoffer Granmo (University of Agder, Norway)
Copyright: © 2010 |Pages: 19
DOI: 10.4018/jamc.2010070101


The graph coloring problem (GCP) is a widely studied combinatorial optimization problem due to its numerous applications in many areas, including time tabling, frequency assignment, and register allocation. The need for more efficient algorithms has led to the development of several GC solvers. In this paper, the authors introduce a team of Finite Learning Automata, combined with the random walk algorithm, using Boolean satisfiability encoding for the GCP. The authors present an experimental analysis of the new algorithm’s performance compared to the random walk technique, using a benchmark set containing SAT-encoding graph coloring test sets.
Article Preview

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.

Complete Article List

Search this Journal:
Open Access Articles: Forthcoming
Volume 10: 4 Issues (2019): 1 Released, 3 Forthcoming
Volume 9: 4 Issues (2018)
Volume 8: 4 Issues (2017)
Volume 7: 4 Issues (2016)
Volume 6: 4 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing