We present three different encodings (SAT, PBC, SMT) to prove termination
of rewrite systems with the Knuth-Bendix order automatically. The constraints
for the weight function and for the precedence are encoded in a formula
which is tested for satisfiability. Any satisfying assignment represents a weight
function and a precedence such that the induced Knuth-Bendix order orients
the rules of the encoded rewrite system from left to right. Comprehensive
experimental results will be presented.

This is joint work with Harald Zankl.