diff --git a/src/main/java/fr/univamu/solver/Interval.java b/src/main/java/fr/univamu/solver/Interval.java
new file mode 100644
index 0000000000000000000000000000000000000000..976e9b741a87c6f598594ff93b5a2c0f2f0e5d22
--- /dev/null
+++ b/src/main/java/fr/univamu/solver/Interval.java
@@ -0,0 +1,203 @@
+package fr.univamu.solver;
+
+public class Interval {
+	public static int MIN_VALUE = -1000000000;
+	public static int MAX_VALUE = +1000000000;
+
+	private int min = MIN_VALUE;
+	private int max = MAX_VALUE;
+
+	public Interval() {
+	}
+
+	public Interval(int min, int max) {
+		if (min <= max) {
+			this.min = min;
+			this.max = max;
+		} else {
+			this.min = +1;
+			this.max = -1;
+		}
+	}
+
+	public String toString() {
+		return isEmpty() ? "[]" : String.format("[%d,%d]", min, max);
+	}
+
+	public boolean reduce(Interval i) {
+		return reduce(i.min, i.max);
+	}
+
+	/*
+	 * Réduire l'intervalle et renvoyer TRUE si une modification a été faite.
+	 */
+	public boolean reduce(int newMin, int newMax) {
+		var oldMin = min;
+		var oldMax = max;
+		if (newMin > newMax) {
+			min = +1;
+			max = -1;
+		} else {
+			min = (newMin > min) ? newMin : min;
+			max = (newMax < max) ? newMax : max;
+			if (min > max) {
+				min = +1;
+				max = -1;
+			}
+		}
+		return (min != oldMin || max != oldMax);
+	}
+
+	public int getSize() {
+		return (min <= max) ? (1 + max - min) : 0;
+	}
+
+	public boolean isFixed() {
+		return (min == max);
+	}
+
+	public boolean isEmpty() {
+		return (min > max);
+	}
+
+	public int getSign() {
+		if (max < 0)
+			return -1;
+		if (min > 0)
+			return +1;
+		return 0;
+	}
+
+	public boolean isNotEmpty() {
+		return (min <= max);
+	}
+
+	public boolean isInside(Interval i) {
+		return (i.min <= this.min && this.min <= this.max && this.max <= i.max);
+	}
+
+	public boolean contains(int v) {
+		return (min <= v && v <= max);
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof Interval i) {
+			return (this.min == i.min && this.max == i.max);
+		}
+		return false;
+	}
+
+	static public Interval empty() {
+		return new Interval(+1, -1);
+	}
+
+	public Interval add(Interval i) {
+		if (isEmpty() || i.isEmpty()) {
+			return empty();
+		}
+		return new Interval(this.min + i.min, this.max + i.max);
+	}
+
+	public Interval sub(Interval i) {
+		if (isEmpty() || i.isEmpty()) {
+			return empty();
+		}
+		return new Interval(this.min - i.max, this.max - i.min);
+	}
+
+	public Interval mul(Interval i) {
+		if (isEmpty() || i.isEmpty()) {
+			return empty();
+		}
+		var minMin = this.min * i.min;
+		var minMax = this.min * i.max;
+		var maxMin = this.max * i.min;
+		var maxMax = this.max * i.max;
+		int min = Math.min(Math.min(Math.min(minMin, minMax), maxMin), maxMax);
+		int max = Math.max(Math.max(Math.max(minMin, minMax), maxMin), maxMax);
+		return new Interval(min, max);
+	}
+
+	public Interval div(Interval i) {
+		if (isEmpty() || i.isEmpty()) {
+			return empty();
+		}
+		int min = Integer.MAX_VALUE;
+		int max = Integer.MIN_VALUE;
+		int divisors[] = { i.min, -1, 1, i.max };
+		for (int divisor : divisors) {
+			if (divisor == 0)
+				continue;
+			if (!i.contains(divisor))
+				continue;
+			// min
+			min = Math.min(min, (this.min / divisor));
+			min = Math.min(min, (this.max / divisor));
+			// max
+			max = Math.max(max, (this.min / divisor));
+			max = Math.max(max, (this.max / divisor));
+		}
+		return new Interval(min, max);
+	}
+
+	// XXXX
+	public Interval div2(Interval i) {
+		if (isEmpty() || i.isEmpty()) {
+			return empty();
+		}
+		if (i.contains(0)) {
+			return new Interval();
+		}
+		int min = Integer.MAX_VALUE;
+		int max = Integer.MIN_VALUE;
+		int divisors[] = { i.min, -1, 1, i.max };
+		for (int divisor : divisors) {
+			if (!i.contains(divisor))
+				continue;
+			// min
+			min = Math.min(min, (this.min / divisor));
+			min = Math.min(min, (this.max / divisor));
+			// max
+			max = Math.max(max, (this.min / divisor));
+			max = Math.max(max, (this.max / divisor));
+		}
+
+		if (getSign() * i.getSign() == 1) {
+			// same sign, result is > 0
+			if (min <= 0)
+				min = 1;
+		}
+
+		if (getSign() * i.getSign() == -1) {
+			// different sign, result is < 0
+			if (max >= 0)
+				max = -1;
+		}
+
+		return new Interval(min, max);
+	}
+
+	public Interval inter(Interval i) {
+		var min = Integer.max(this.min, i.min);
+		var max = Integer.min(this.max, i.max);
+		return new Interval(min, max);
+	}
+
+	public int getMin() {
+		return min;
+	}
+
+	public int getMax() {
+		return max;
+	}
+
+	public void setMin(int min) {
+		this.min = min;
+	}
+
+	public void setMax(int max) {
+		this.max = max;
+	}
+
+}
diff --git a/src/main/java/fr/univamu/solver/Solver.java b/src/main/java/fr/univamu/solver/Solver.java
new file mode 100644
index 0000000000000000000000000000000000000000..21a9fec8480f9ac3f443549c7741df8e66b1b5ae
--- /dev/null
+++ b/src/main/java/fr/univamu/solver/Solver.java
@@ -0,0 +1,418 @@
+package fr.univamu.solver;
+
+import java.util.LinkedList;
+import java.util.List;
+
+class Constraint {
+	private char type;
+	private Variable result;
+	private Variable var1;
+	private Variable var2;
+
+	public String toString() {
+		return String.format("%s(%s,%s,%s)", type, result, var1, var2);
+	}
+
+	public Constraint(char type, Variable result, Variable var1, Variable var2) {
+		this.type = type;
+		this.result = result;
+		this.var1 = var1;
+		this.var2 = var2;
+	}
+
+	public char getType() {
+		return type;
+	}
+
+	public Variable getResult() {
+		return result;
+	}
+
+	public Variable getVar1() {
+		return var1;
+	}
+
+	public Variable getVar2() {
+		return var2;
+	}
+}
+
+public class Solver {
+
+	private static final int CHECK_INTERVALS_STRATEGY = 1;
+	private static final int REDUCE_AND_CHECK_INTERVALS_STRATEGY = 2;
+
+	private List<Constraint> constraints = new LinkedList<>();
+	private List<Variable> variables = new LinkedList<>();
+	private int strategy = CHECK_INTERVALS_STRATEGY;
+
+	private long solutionsCounter = 0;
+	private long nodesCounter = 0;
+	private long maxNodes = 1000_000_000L;
+	private boolean verbose = true;
+
+	public void reduceAndCheckIntervalsStrategy() {
+		strategy = REDUCE_AND_CHECK_INTERVALS_STRATEGY;
+	}
+
+	private boolean checkAddConstraintIntervalsStrategy(Constraint c) {
+		return c.getVar1().add(c.getVar2()).inter(c.getResult()).isNotEmpty();
+	}
+
+	private boolean checkMulConstraintIntervalsStrategy(Constraint c) {
+		return c.getVar1().mul(c.getVar2()).inter(c.getResult()).isNotEmpty();
+	}
+
+	private boolean checkDivConstraintIntervalsStrategy(Constraint c) {
+		return c.getVar1().div(c.getVar2()).inter(c.getResult()).isNotEmpty();
+	}
+
+	private boolean checkDiffConstraintIntervalsStrategy(Constraint c) {
+		var result = c.getResult();
+		var ko = result.equals(c.getVar1()) && result.isFixed();
+		return (!ko);
+	}
+
+	private boolean reduceAddConstraint(Constraint c) {
+		var change = c.getResult().reduce(c.getVar1().add(c.getVar2()));
+		change = c.getVar1().reduce(c.getResult().sub(c.getVar2())) || change;
+		change = c.getVar2().reduce(c.getResult().sub(c.getVar1())) || change;
+		return change;
+	}
+
+	private boolean reduceMulConstraint(Constraint c) {
+		var change = false;
+		for (int i = 0; i < 3; i++) {
+			change = c.getResult().reduce(c.getVar1().mul(c.getVar2())) || change;
+			change = c.getVar2().reduce(c.getResult().div2(c.getVar1())) || change;
+			change = c.getVar1().reduce(c.getResult().div2(c.getVar2())) || change;
+		}
+		return change;
+	}
+
+	private boolean checkConstraintIntervalsStrategy(Constraint c) {
+		switch (c.getType()) {
+		case '+':
+			return checkAddConstraintIntervalsStrategy(c);
+		case '#':
+			return checkDiffConstraintIntervalsStrategy(c);
+		case '*':
+			return checkMulConstraintIntervalsStrategy(c);
+		case '/':
+			return checkDivConstraintIntervalsStrategy(c);
+		default:
+			break;
+		}
+		throw new IllegalArgumentException("bad constraint: " + c);
+	}
+
+	private boolean reduce(Constraint c) {
+		switch (c.getType()) {
+		case '+':
+			return reduceAddConstraint(c);
+		case '*':
+			return reduceMulConstraint(c);
+//		case '#':
+//		case '/':
+		}
+		return false;
+	}
+
+	private boolean checkConstraint(Constraint c) {
+		switch (strategy) {
+		case CHECK_INTERVALS_STRATEGY:
+		case REDUCE_AND_CHECK_INTERVALS_STRATEGY:
+			return checkConstraintIntervalsStrategy(c);
+		}
+		throw new IllegalStateException("bad strategy: " + strategy);
+	}
+
+	private boolean checkConstraints() {
+		for (Constraint c : constraints) {
+			if (!checkConstraint(c)) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+	public Variable findVariable() {
+		Variable best = null;
+		for (Variable v : variables) {
+			if (v.isFixed()) {
+				// ne pas choisir
+			} else if (best == null) {
+				best = v;
+			} else if (v.getSize() < best.getSize()) {
+				best = v;
+			}
+		}
+		return best;
+	}
+
+	public boolean findSolutions() {
+		if (++nodesCounter > maxNodes) {
+			throw new IllegalStateException("too many nodes");
+		}
+		if (checkConstraints() == false) {
+			return false;
+		}
+		var v = findVariable();
+		if (v == null) {
+			solutionsCounter++;
+			if (verbose) {
+				variables.stream().filter(Variable::isNamed).forEach(System.out::println);
+				System.out.println();
+			}
+			return true;
+		}
+
+		boolean result = false;
+		int min = v.getMin();
+		int max = v.getMax();
+
+		// Comment découper le domaine ?
+		int step = 1;
+		if (v.getSize() > 1000) {
+			if (min < 0 && max >= 0) {
+				step = -min;
+			} else {
+				int mid = (min + max) / 2;
+				step = (1 + mid - min);
+			}
+		}
+
+		// explorer le domaine
+		for (int value = min; value <= max; value += step) {
+			v.setMin(value);
+			v.setMax(Math.min(value + step - 1, max));
+			if (findSolutions()) {
+				result = true;
+			}
+		}
+		v.setMin(min);
+		v.setMax(max);
+		return result;
+	}
+
+	public Variable newVar() {
+		var v = new Variable(variables.size());
+		variables.add(v);
+		return v;
+	}
+
+	public Variable newVar(String name) {
+		var v = new Variable(name);
+		variables.add(v);
+		return v;
+	}
+
+	public Variable newConstant(int value) {
+		return newVar().domain(value);
+	}
+
+	public void eq(Variable a, Variable b) {
+		sub(newConstant(0), a, b); // 0 = A - B
+	}
+
+	public void gt(Variable a, Variable b) {
+		sub(newVar().domain(1, Variable.MAX_VALUE), a, b); // Z=A-B,Z>0
+	}
+
+	public void get(Variable a, Variable b) {
+		sub(newVar().domain(0, Variable.MAX_VALUE), a, b); // Z=A-B, Z>=0
+	}
+
+	public void lt(Variable a, Variable b) {
+		gt(b, a);
+	}
+
+	public void let(Variable a, Variable b) {
+		get(b, a);
+	}
+
+	public void diff(Variable a, Variable b) {
+		constraints.add(new Constraint('#', a, b, null));
+	}
+
+	public void allDiff(Variable... variables) {
+		for (int i = 0; i < variables.length; i++)
+			for (int j = i + 1; j < variables.length; j++) {
+				diff(variables[i], variables[j]);
+			}
+	}
+
+	private void add(Variable result, Variable a, Variable b) {
+		constraints.add(new Constraint('+', result, a, b));
+	}
+
+	private void sub(Variable result, Variable a, Variable b) {
+		add(a, result, b);
+	}
+
+	private void mul(Variable result, Variable a, Variable b) {
+		constraints.add(new Constraint('*', result, a, b));
+	}
+
+	private void div(Variable result, Variable a, Variable b) {
+		constraints.add(new Constraint('/', result, a, b));
+	}
+
+	private Variable parseSimpleTerm(List<Object> terms) {
+		var first = terms.removeFirst();
+		if (first instanceof Variable var) {
+			return var;
+		}
+		if (first instanceof Integer cst) {
+			return this.newConstant(cst);
+		}
+		throw new IllegalArgumentException("bad expression: " + first);
+	}
+
+	private boolean parseToken(String token, List<Object> terms) {
+		if (!terms.isEmpty()) {
+			if (token.equals(terms.getFirst())) {
+				terms.removeFirst();
+				return true;
+			}
+		}
+		return false;
+	}
+
+	private Variable parseMultiplicationTerm(List<Object> terms) {
+		var first = parseSimpleTerm(terms);
+		if (parseToken("*", terms)) {
+			var second = parseMultiplicationTerm(terms);
+			var result = newVar();
+			mul(result, first, second);
+			return result;
+		}
+		if (parseToken("/", terms)) {
+			var second = parseMultiplicationTerm(terms);
+			var result = newVar();
+			div(result, first, second);
+			return result;
+		}
+		return first;
+	}
+
+	private Variable parseAdditionTerm(List<Object> terms) {
+		var first = parseMultiplicationTerm(terms);
+		if (parseToken("+", terms)) {
+			var second = parseAdditionTerm(terms);
+			var result = newVar();
+			add(result, first, second);
+			return result;
+		}
+		if (parseToken("-", terms)) {
+			var second = parseAdditionTerm(terms);
+			var result = newVar();
+			add(first, result, second);
+			return result;
+		}
+		return first;
+	}
+
+	public void addConstraint(Object... terms) {
+		var termsList = new LinkedList<>();
+		termsList.addAll(List.of(terms));
+		var var1 = parseAdditionTerm(termsList);
+		var relation = termsList.removeFirst();
+		var var2 = parseAdditionTerm(termsList);
+		if (!termsList.isEmpty()) {
+			throw new IllegalArgumentException("bad expression: " + termsList);
+		}
+		if (relation instanceof String carRelation) {
+			switch (carRelation) {
+			case "=":
+				eq(var1, var2);
+				return;
+			case ">":
+				gt(var1, var2);
+				return;
+			case ">=":
+				get(var1, var2);
+				return;
+			case "<":
+				lt(var1, var2);
+				return;
+			case "<=":
+				let(var1, var2);
+				return;
+			case "<>":
+				diff(var1, var2);
+				return;
+			}
+		}
+		throw new IllegalArgumentException("bad relation: " + relation);
+	}
+
+	public Variable expression2(Object... terms) {
+		var termsList = new LinkedList<>(List.of(terms));
+		var result = parseAdditionTerm(termsList);
+		if (!termsList.isEmpty()) {
+			throw new IllegalArgumentException("bad expression: " + termsList);
+		}
+		return result;
+	}
+
+	private void reduce() {
+		if (verbose) {
+			System.out.println("Variables before reduction:");
+			variables.forEach(System.out::println);
+		}
+
+		for (boolean change = true; change;) {
+			change = false;
+			for (Constraint c : constraints) {
+				if (reduce(c)) {
+					change = true;
+				}
+			}
+		}
+
+		if (verbose) {
+			System.out.println("Variables after reduction:");
+			variables.forEach(System.out::println);
+		}
+	}
+
+	public long solve() {
+		this.solutionsCounter = 0;
+		this.nodesCounter = 0;
+		if (strategy == REDUCE_AND_CHECK_INTERVALS_STRATEGY) {
+			reduce();
+		}
+		findSolutions();
+		return solutionsCounter;
+	}
+
+	public int getStrategy() {
+		return strategy;
+	}
+
+	public long getNodesCounter() {
+		return nodesCounter;
+	}
+
+	public long getMaxNodes() {
+		return maxNodes;
+	}
+
+	public void setStrategy(int strategy) {
+		this.strategy = strategy;
+	}
+
+	public void setMaxNodes(long maxNodes) {
+		this.maxNodes = maxNodes;
+	}
+
+	public boolean isVerbose() {
+		return verbose;
+	}
+
+	public void setVerbose(boolean verbose) {
+		this.verbose = verbose;
+	}
+
+}
diff --git a/src/main/java/fr/univamu/solver/Variable.java b/src/main/java/fr/univamu/solver/Variable.java
new file mode 100644
index 0000000000000000000000000000000000000000..8e5905608118a94ac657a1828a65b4389b178af2
--- /dev/null
+++ b/src/main/java/fr/univamu/solver/Variable.java
@@ -0,0 +1,51 @@
+package fr.univamu.solver;
+
+public class Variable extends Interval {
+
+	final private String name;
+	final private boolean named;
+
+	public Variable(int _number) {
+		named = false;
+		name = "_" + _number;
+	}
+
+	public Variable(String _name) {
+		named = true;
+		name = _name;
+	}
+
+	public Variable domain(int min, int max) {
+		reduce(min, max);
+		return this;
+	}
+
+	public Variable domain(int value) {
+		return domain(value, value);
+	}
+
+	public int getFixedValue() {
+		if (isFixed()) {
+			return (getMin());
+		}
+		throw new IllegalStateException("variable not fixed: " + this);
+	}
+
+	public String toString() {
+		return (String.format("%s%s", this.name, super.toString()));
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		return super.equals(obj);
+	}
+
+	public String getName() {
+		return name;
+	}
+
+	public boolean isNamed() {
+		return named;
+	}
+
+}