# How does Mathematica compute 'Reduce'?

I submit a Reduce command and get results like this:

Reduce[t0 >= 0 && -9 + t0 - 5 t1 + 154 >= 0 && -5 + t0 - 3 t1 + 77 >= 0, {t0, t1}, integers]

With output:

Reduce::bdomv: Warning: integers is not a valid domain specification. Assuming it is a variable to eliminate. (0 <= t0 <= 75/2 && t1 <= (72 + t0)/3) || (t0 > 75/2 && t1 <= (145 + t0)/5)

Put simply, what algorithm is being used to obtain these results?

Preamble: "integers" -> Integers in your problem statement, Mathematica uses CamelType.

The method depends on your problem, naturally. In your case it appears to be the Contejean–Devie method. A [buried] excerpt from the Mathematica documentation:

For polynomial systems, Reduce uses cylindrical algebraic decomposition for real domains and Gröbner basis methods for complex domains.

With algebraic functions, Reduce constructs equivalent purely polynomial systems.

With transcendental functions, Reduce generates polynomial systems composed with transcendental conditions, then reduces these using functional relations and a database of inverse image information. With piecewise functions, Reduce does symbolic expansion to construct a collection of continuous systems.

For univariate transcendental equations, Reduce represents solutions as transcendental Root objects. For exp-log function equations over the reals, Reduce uses an exact exp-log root isolation algorithm. For analytic function equations over bounded real or complex domains, Reduce finds roots using validated numerical methods. For elementary functions, both the number and the location of roots are fully validated using interval arithmetic methods. For non-elementary functions, validation of the number of roots depends on correctness of numeric integration and validation of the location of roots depends on correctness of accuracy estimates provided by the Wolfram Language's significance arithmetic.

For Diophantine systems, Reduce solves linear equations using Hermite normal form, and linear inequalities using Contejean–Devie methods. For univariate polynomial equations, it uses an improved Cucker–Koiran–Smale method, while for bivariate quadratic equations, it uses Hardy–Muskat–Williams methods for ellipses and classical techniques for Pell and other cases. Reduce includes specialized methods for about 25 classes of Diophantine equations, including the Tzanakis–de Weger algorithm for Thue equations.

It's also worth mentioning that the original problem is rather straightforward to reduce by hand:

$$t_0 \ge 0 \quad \text{and} \quad t_1 \le \cases{ \frac{t_0}{3} + 24 \quad \text{if } \, t_0 \le 32, \\ \frac{t_0}{5} + 29 \quad \text{otherwise}}$$