More Efficient Handling of Conjunctions in DNF

Although we can replace equalities with two inequalities, this is typically inefficient way to handle them.

If the coefficient next to a variable is one, then we can just solve for this variable and use one-point rule.

What if the coefficient is not one? In that case we use techniques for solving linear Diophantine equations (=linear equations over integers).

Here is an example illustrating the key ideas.

$\begin{equation*} \exists a,b,d.\ a + b = s \land a + 5d = 2b \land a \ge 0 \land b \ge 0 \land d \ge 1 \end{equation*}$

See more in e.g. in Hermite normal form.

Question: what if instead of $d \ge 1$ we had $d \neq 0$