Function fourier_motzkin_unsat 

pub fn fourier_motzkin_unsat(constraints: &[Constraint]) -> bool

Check if a constraint set is unsatisfiable using Fourier-Motzkin elimination.

This is the core decision procedure. It eliminates variables one by one until only constant constraints remain, then checks for contradictions.

Algorithm

For each variable x in the system:

1. Partition constraints into lower bounds on x, upper bounds on x, and independent
2. For each pair (lower, upper), derive a new constraint without x
3. Check for immediate contradictions (e.g., 5 <= 0)

Returns

• true if the constraints are unsatisfiable (contradiction found)
• false if the constraints may be satisfiable

Usage for Validity

To prove a goal G is valid, we check if NOT(G) is unsatisfiable. If fourier_motzkin_unsat(negation_constraints) returns true, the goal is valid.