added ad hoc solver

integraal/integraal-explanation/src/main/java/fr/boreal/explanation/MicroMUSSolver.java

+package fr.boreal.explanation;
+
+import java.util.*;
+import java.util.stream.Collectors;
+
+public class MicroMUSSolver {
+
+    // Factory for unique integer representation of variables
+    private static class VariableFactory {
+        private final Map<String, PropositionalVariable> nameToVar = new HashMap<>();
+        private final Map<Integer, PropositionalVariable> idToVar = new HashMap<>();
+        private int counter = 1;
+
+        public PropositionalVariable getOrCreate(String name) {
+            return nameToVar.computeIfAbsent(name, k -> {
+                PropositionalVariable var = new PropositionalVariable(name, counter);
+                idToVar.put(counter, var);
+                counter++;
+                return var;
+            });
+        }
+
+        public String getName(int id) {
+            return idToVar.getOrDefault(id, new PropositionalVariable("?", id)).name;
+        }
+    }
+
+    private static final VariableFactory factory = new VariableFactory();
+
+    // Propositional variable wrapper
+    private static class PropositionalVariable {
+        private final int variable;
+        private final String name;
+
+        public PropositionalVariable(String name, int var) {
+            this.name = name;
+            this.variable = var;
+        }
+
+        public String toString() {
+            return this.name;
+        }
+    }
+
+    // Horn clause record
+    private static class HornClause {
+        private final PropositionalVariable[] body;
+        private final PropositionalVariable head;
+        private final int group;
+
+        public HornClause(PropositionalVariable[] body, PropositionalVariable head, int group) {
+            Arrays.sort(body, Comparator.comparingInt(v -> v.variable)); // Ensure body is sorted by variable integer
+            this.body = body;
+            this.head = head;
+            this.group = group;
+        }
+
+        public PropositionalVariable[] getBody() {
+            return body;
+        }
+
+        public PropositionalVariable getHead() {
+            return head;
+        }
+
+        public int getGroup() {
+            return group;
+        }
+
+        @Override
+        public String toString() {
+            StringBuilder sb = new StringBuilder();
+            sb.append("(");
+            for (int i = 0; i < body.length; i++) {
+                sb.append(body[i].name);
+                if (i < body.length - 1) sb.append(" ∧ ");
+            }
+            sb.append(") -> ").append(head.name);
+            return sb.toString();
+        }
+    }
+
+    // Index structure for Horn Clauses
+    private static class ClauseIndex {
+        private final Map<PropositionalVariable, Set<HornClause>> index = new HashMap<>();
+
+        public void addClause(HornClause clause) {
+            index.computeIfAbsent(clause.getHead(), k -> new HashSet<>()).add(clause);
+        }
+
+        public Set<HornClause> getClausesProving(PropositionalVariable variable, Set<Integer> groups) {
+            return index.getOrDefault(variable, Collections.emptySet()).stream()
+                    .filter(clause -> groups.isEmpty() || groups.contains(clause.getGroup()))
+                    .collect(Collectors.toSet());
+        }
+    }
+
+    private final ClauseIndex IDX = new ClauseIndex();
+
+    public void addClause(HornClause clause) {
+        IDX.addClause(clause);
+    }
+
+    // MUS proving method
+    public boolean prove(PropositionalVariable propositionalVar, Set<Integer> groups, boolean stopAtFirst) {
+        int level = -1;
+        Deque<PropositionalVariable> toProve = new ArrayDeque<>();
+        Set<PropositionalVariable> seen = new HashSet<>();
+        toProve.add(propositionalVar);
+
+        List<List<HornClause>> sequence = new ArrayList<>();
+        List<Integer> pointer = new ArrayList<>(Collections.nCopies(100, 0)); // Arbitrary large limit
+        boolean found = false;
+
+        while (true) {
+            PropositionalVariable current = toProve.poll();
+            if (current == null) break;
+            level++;
+
+            if (pointer.get(level) == 0) {
+                //load clauses
+                sequence.add(IDX.getClausesProving(current, groups).stream().toList());
+            }
+
+            if (sequence.get(level).isEmpty()) {
+                pointer.set(level, 0);
+                sequence.set(level, new ArrayList<>()); // Empty the sequence at this level
+                level--;
+                continue;
+            }
+
+            HornClause candidate = sequence.get(level).get(pointer.get(level));
+            seen.add(current);
+
+            for (PropositionalVariable bodyVar : candidate.getBody()) {
+                if (!seen.contains(bodyVar)) {
+                    toProve.add(bodyVar);
+                }
+            }
+
+            if (toProve.isEmpty()) {
+                if (checkSolutionOK(candidate)) {
+                    for (int i = 0; i < sequence.size(); i++)
+                        System.out.println(sequence.get(i).get(pointer.get(i)));
+                    found = true;
+                    toProve.add(propositionalVar);
+                    pointer.set(level, pointer.get(level) + 1);
+                    level--;
+                }
+
+                if (stopAtFirst) {
+                    break;
+                }
+            }
+            if (pointer.get(level) == sequence.get(level).size()) {
+                pointer.set(level, 0);
+                sequence.set(level, new ArrayList<>()); // Empty the sequence at this level
+                level--;
+
+            }
+
+        }
+        return found;
+    }
+
+    private boolean checkSolutionOK(HornClause candidate) {
+        return true;
+    }
+
+    public static void main(String[] args) {
+        MicroMUSSolver solver = new MicroMUSSolver();
+        PropositionalVariable D = factory.getOrCreate("D");
+        PropositionalVariable B = factory.getOrCreate("B");
+        PropositionalVariable A = factory.getOrCreate("A");
+        PropositionalVariable C = factory.getOrCreate("C");
+
+        solver.addClause(new HornClause(new PropositionalVariable[]{}, D, 1));
+        solver.addClause(new HornClause(new PropositionalVariable[]{}, B, 1));
+        solver.addClause(new HornClause(new PropositionalVariable[]{D}, B, 2));
+        solver.addClause(new HornClause(new PropositionalVariable[]{B, A}, C, 3));
+        solver.addClause(new HornClause(new PropositionalVariable[]{C}, A, 4));
+        solver.addClause(new HornClause(new PropositionalVariable[]{}, C, 5));
+
+        boolean result = solver.prove(C, Set.of(1, 2, 3, 4, 5), false);
+        System.out.println("Proof found: " + result);
+    }
+}
\ No newline at end of file