From f6282cd95ae9470836952ffe7db4c3cda626276e Mon Sep 17 00:00:00 2001 From: massat <jean-luc.massat@univ-amu.fr> Date: Thu, 3 Oct 2024 17:05:31 +0200 Subject: [PATCH] Create --- src/main/java/fr/univamu/solver/Interval.java | 203 +++++++++ src/main/java/fr/univamu/solver/Solver.java | 418 ++++++++++++++++++ src/main/java/fr/univamu/solver/Variable.java | 51 +++ 3 files changed, 672 insertions(+) create mode 100644 src/main/java/fr/univamu/solver/Interval.java create mode 100644 src/main/java/fr/univamu/solver/Solver.java create mode 100644 src/main/java/fr/univamu/solver/Variable.java 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 0000000..976e9b7 --- /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 0000000..21a9fec --- /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 0000000..8e59056 --- /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; + } + +} -- GitLab