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

Abstract

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
Top

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 jamc.2010070101.m01 such that if C(p) = C(q) then jamc.2010070101.m02. The set jamc.2010070101.m03 is the set of colors. There exist two variants of this problem. In the optimization variant, the goal is to find the chromatic number jamc.2010070101.m04, 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 formulajamc.2010070101.m05with 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 jamc.2010070101.m06, in turn, has the form:jamc.2010070101.m07,where jamc.2010070101.m08 and jamc.2010070101.m09 denotes the negation of jamc.2010070101.m10. The task is to determine whether the propositional formula jamc.2010070101.m11 evaluates to True. Such an assignment, if it exists, is called a satisfying assignment for jamc.2010070101.m12, and jamc.2010070101.m13 is called satisfiable. Otherwise, jamc.2010070101.m14 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, jamc.2010070101.m15 is a clause containing the two literals jamc.2010070101.m16 and jamc.2010070101.m17. This clause is satisfied if either jamc.2010070101.m18 is True or jamc.2010070101.m19 is True. When each clause in jamc.2010070101.m20 contains exactly jamc.2010070101.m21 literals, the resulting SAT problem is called k-SAT.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 11: 4 Issues (2020): 2 Released, 2 Forthcoming
Volume 10: 4 Issues (2019)
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