# SAT for arithmetic

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$$?

• What did you try? Where did you get stuck? – David Richerby Feb 18 '15 at 15:15
• You encode that constraint the same way you encode $\; \left|\hspace{.02 in}X\hspace{-0.05 in}-\hspace{-0.05 in}Y\hspace{.02 in}\right| = n \:\:$. $\;\;\;\;\;\;$ – user12859 Feb 18 '15 at 15:35
• @RickyDemer Presumably this is a two-part question. In the first part you have to encode $|X-Y| \geq n$, and in the second $|X-Y|=n$. – Yuval Filmus Feb 18 '15 at 15:45

1. 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.