The problem of Satisfiability Modulo Theories (SMT) is to decide satisfiability of the given formula over the given first-order theory. One of the practically interesting theories, used for example for describing parallel programs with weak memory models, is the theory of ordering constraints. This theory was investigated theoretically and some algorithms for it were proposed during the last years. As an unrelated topic, it has also been recently proposed to use a technique of vertex elimination to encode graph problems such as acyclicity and reachability using propositional formulas. For this purpose, the technique was shown to be efficient in practice. The goal of this thesis is to design a translation of SMT formulas over the theory of ordering constraints to propositional formulas using the technique of vertex elimination, so that an efficient propositional satisfiability solver (SAT) can be used to solve it. The student will prove the correctness of the designed translation, implement it, and experimentally evaluate it on a suitable set of benchmarks.