This paper will study the solution of graph coloring problems
by encoding into propositional satisfiability problems.
The study will cover three kinds of satisfiability solvers,
based on postorder reasoning (e.g., grasp, chaff), preorder
reasoning (e.g., 2cl, 2clsEq), and back-chaining (modoc).
The study will evaluate at least three encodings, one of them
believed to be new.
The study will also consider some simple symmetry-breaking methods,
specific to coloring.
Preliminary results are given.
If time permits, variations of graph coloring will be considered.