Given two integers $X$ and $Y$, each can be encoded in binary $X=(x_4 x_3 x_2 x_1)$ and $Y=(y_4 y_3 y_2 y_1)$, how do I encode each one of the constraints
$$|X-Y|\geq n \quad\text{and}\quad|X-Y|= n$$ when $n$ is a given natural number (say, 10) as a boolean formula over $x_1,\dots, x_4, y_1, \dots, y_4$?
Here is the general approach to this type of question.
You write a boolean combinatorial circuit to express the constraint. In other words, you write a circuit $C$ that takes as input the values of your variables (e.g., $X$, $Y$) and outputs true or false. Your circuit $C$ should be designed to output true if the inputs satisfy all of your constraints, or false if they don't. Your circuit can use standard boolean gates, e.g., AND, OR, NOT, XOR, and so on.
You use the Tseitin transform to convert this to an instance of SAT. (Basically, this is using the standard reduction from CircuitSAT to SAT that's implicit in Cook's theorem.)
You feed the SAT formula to a SAT solver, and ask it to find for you a set of inputs that satisfies the formula you got in step 2 (i.e., that satisfies all your constraints).
Alternatively, some SAT front-ends and SMT solvers will help do these steps for you, which saves some effort. For instance, STP lets you express your constraints directly as arbitrary expressions containing AND, OR, NOT, XOR, etc. (so it does steps 2 and 3 for you). It also has some convenient syntactic support for constraints that use integer arithmetic, so it will make step 1 easier for you as well. Another example of such a solver is Z3.
