diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/GMUSStatistics.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/GMUSStatistics.java
index 7d358b7696f9f6718ec2805cf81737d7a383ce5c..2af93276bc6a646e3fdffe5e949852c4432071c5 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/GMUSStatistics.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/GMUSStatistics.java
@@ -9,9 +9,8 @@ public class GMUSStatistics {
public long inteGraalToSat4JClauseConversion = -1;
public long sat4jToInteGraalMUSDecoding = -1;
public int heuristicsDetectedNonMinimalityFromSameGroupClauseConflict = 0;
- public int heuristicsDetectedNonMinimalityFromIdenticalClauseConflictInDifferentGroup = 0;
- public int heuristicsDetectedNoAlternatives = 0;
public int heuristicsDetectedSameClauseInDifferentGroup = 0;
public int usedHeavyChaseBasedCheckToDiscoverNonMinimality = 0;
- public int theConflictingClauseCannotBeInferredAsItHasNoSupportAtomClause=0;
+ public int theConflictingClauseCannotBeInferredAsItHasNoSupportAtomClause = 0;
+ public int heuristicDetectedAPreviousGroupMUSWithLessGroupsThanTheCandidateGMUS = 0;
}
diff --git a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/Sat4JSolver.java b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/Sat4JSolver.java
index cf53260fff17e67e3742e306f7bd1237c9819625..41254e1984cbc83db31b8211c5de46b358dda18d 100644
--- a/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/Sat4JSolver.java
+++ b/integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/Sat4JSolver.java
@@ -30,7 +30,7 @@ import java.util.stream.Collectors;
public class Sat4JSolver implements Solver {
private static List<List<Integer>> lists;
- private static boolean debug = false;
+ private static boolean debug = true;
/**
* enumerates MUSes via Sat4J
@@ -153,13 +153,23 @@ public class Sat4JSolver implements Solver {
try {
List<List<List<Integer>>> MUSes = new ArrayList();
+ List<Set<Integer>> MUsesGroups = new ArrayList();
var sat4JMUSes = enumerateMUSesViaSat4J(instance);
+ // we sort the muses by size
+ sat4JMUSes.sort(Comparator.comparingInt(List::size));
+
for (List<List<Integer>> mus : sat4JMUSes) {
- if (isGMUS(mus, instance)) {
+ if (isGMUS(mus, instance, MUsesGroups)) {
+
+ /* we record the mus solution */
MUSes.add(mus);
+ /* we record the groups of the solution */
+ Set<Integer> groups = mus.stream().map(m -> m.getFirst()).collect(Collectors.toSet());
+ MUsesGroups.add(groups);
+
debugPrint("Solution found #" + MUSes.size());
mus.forEach(Sat4JSolver::debugPrintClause);
debugPrint("==========\n");
@@ -167,11 +177,11 @@ public class Sat4JSolver implements Solver {
}
return MUSes;
+
} catch (ContradictionException e) {
System.out.println("Contradiction found\n +" + e.getMessage());
return new ArrayList<>();
}
-
}
@@ -247,7 +257,7 @@ public class Sat4JSolver implements Solver {
}
- public static boolean isGMUS(List<List<Integer>> candidateGMUS, Instance instance) {
+ public static boolean isGMUS(List<List<Integer>> candidateGMUS, Instance instance, List<Set<Integer>> MUsesGroups) {
debugPrint("Checking candidate solution");
candidateGMUS.forEach(Sat4JSolver::debugPrintClause);
@@ -259,6 +269,11 @@ public class Sat4JSolver implements Solver {
.map(clause -> clause.get(0))
.collect(Collectors.toSet());
+ if (checkIfASmallerGroupMUSExists(MUsesGroups, candidateMUSGroups, instance)) {
+ instance.statistics.heuristicDetectedAPreviousGroupMUSWithLessGroupsThanTheCandidateGMUS++;
+ return false;
+ }
+
// For every clause in the candidate, look up its conflict set in the theory,
// restricted to those clauses whose group is among the candidate's groups.
for (List<Integer> gMUSClause : candidateGMUS) {
@@ -273,33 +288,49 @@ public class Sat4JSolver implements Solver {
}
// Restrict conflicts to those clauses that belong to one of the candidate groups.
- List<List<Integer>> allConflictsWithTheClauseInTheGroups = instance.clausesGroupedByHead.get(head).stream()
+ List<List<Integer>> allConflictsWithTheClauseInDifferentMUSGroups = instance.clausesGroupedByHead.get(head).stream()
+ .filter(conflictClause -> conflictClause != gMUSClause)
+ .filter(conflictClause -> candidateMUSGroups.contains(conflictClause.getFirst()) && conflictClause.getFirst() != gMUSClause.getFirst())
+ .collect(Collectors.toList());
+
+
+ // Restrict conflicts to those clauses that belong to one of the candidate groups.
+ List<List<Integer>> allConflictsWithTheClauseInSameMUSGroup = instance.clausesGroupedByHead.get(head).stream()
.filter(conflictClause -> conflictClause != gMUSClause)
- .filter(conflictClause -> candidateMUSGroups.contains(conflictClause.get(0)))
+ .filter(conflictClause -> conflictClause.getFirst() == gMUSClause.getFirst())
.collect(Collectors.toList());
- if (allConflictsWithTheClauseInTheGroups.isEmpty()) {
+
+ if (allConflictsWithTheClauseInDifferentMUSGroups.isEmpty() && allConflictsWithTheClauseInSameMUSGroup.isEmpty()) {
// the clause has no conflicting clauses (in the groups of the candidate mus), so it is not a source of non-minilality
instance.statistics.heuristicsDetectedNoConflictingClauseExistsWithinTheGroups++;
continue;
}
// Compute the set of groups in these restricted conflicts.
- Set<Integer> conflictGroups = allConflictsWithTheClauseInTheGroups.stream()
+ Set<Integer> conflictGroups = allConflictsWithTheClauseInDifferentMUSGroups.stream()
.map(conflictClause -> conflictClause.get(0))
.collect(Collectors.toSet());
- if (conflictGroups.contains(gMUSClause.get(0))) {
+ if (!allConflictsWithTheClauseInSameMUSGroup.isEmpty()) {
// Case 1: there is a conflicting clause in the same groupe
- if (hasNonMinimalityHeuristicCase1(candidateGMUS, gMUSClause, allConflictsWithTheClauseInTheGroups, instance)) {
+ if (hasNonMinimalityHeuristicCase1(candidateGMUS, gMUSClause, allConflictsWithTheClauseInSameMUSGroup, instance)) {
return false;
}
+ if (!allConflictsWithTheClauseInDifferentMUSGroups.isEmpty()) {
+ if (hasNonMinimalityHeuristicCase2(candidateGMUS, gMUSClause, allConflictsWithTheClauseInDifferentMUSGroups, instance)) {
+ return false;
+ }
+ if (cannotBeProvedByAlternatives(candidateGMUS, gMUSClause, allConflictsWithTheClauseInDifferentMUSGroups, instance)) {
+ stillPotentialConflicts.add(gMUSClause);
+ }
+ }
} else {
// Case 2: there is no a conflicting clause in the same groupe
- if (hasNonMinimalityHeuristicCase2(candidateGMUS, gMUSClause, allConflictsWithTheClauseInTheGroups, instance)) {
+ if (hasNonMinimalityHeuristicCase2(candidateGMUS, gMUSClause, allConflictsWithTheClauseInDifferentMUSGroups, instance)) {
return false;
}
- if (cannotBeProvedByAlternatives(candidateGMUS, gMUSClause, allConflictsWithTheClauseInTheGroups, instance)) {
+ if (cannotBeProvedByAlternatives(candidateGMUS, gMUSClause, allConflictsWithTheClauseInDifferentMUSGroups, instance)) {
stillPotentialConflicts.add(gMUSClause);
}
}
@@ -335,6 +366,28 @@ public class Sat4JSolver implements Solver {
return true;
}
+ /**
+ * @param alreadyFoundGroupMUSes
+ * @param candidateGroupMUS
+ * @param instance
+ * @return true iif there is a group mus that uses less groups
+ */
+ private static boolean checkIfASmallerGroupMUSExists(List<Set<Integer>> alreadyFoundGroupMUSes, Set<Integer> candidateGroupMUS, Instance instance) {
+ for (var musGroups : alreadyFoundGroupMUSes) {
+ if (candidateGroupMUS.size() > musGroups.size()) {
+ boolean containsAllGroups = true;
+ for (var group : musGroups) {
+ containsAllGroups = containsAllGroups && candidateGroupMUS.contains(group);
+ }
+ if (containsAllGroups) {
+ // there is already a group mus that uses strictly less groups
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
/**
* @param candidateGMUS
* @param clause
@@ -488,8 +541,9 @@ public class Sat4JSolver implements Solver {
// Step 2.2: Check if it's possible to derive the head of the clause
// by restricting the theory to only groups in B.
boolean weAlreadyKnowThatWeCanProveTheVariableWithTheGroups = instance.canProveVariableWithGroups.containsKey(clause.getLast())
- && instance.canProveVariableWithGroups.get(clause.getLast()).stream()
- .filter(set -> groupsSupportingConflictingClause.containsAll(set)).findAny().isPresent();;
+ && instance.canProveVariableWithGroups.get(clause.getLast()).stream()
+ .filter(set -> groupsSupportingConflictingClause.containsAll(set)).findAny().isPresent();
+ ;
if (weAlreadyKnowThatWeCanProveTheVariableWithTheGroups) {
// A source of non-minimality has been found.
@@ -497,9 +551,9 @@ public class Sat4JSolver implements Solver {
}
boolean weAlreadyKnowThatWeCanNOTProveTheVariableWithTheGroups = instance.canNOTProveVariableWithGroups.containsKey(clause.getLast())
- && instance.canNOTProveVariableWithGroups.get(clause.getLast()).stream()
- .filter(set -> set.containsAll(groupsSupportingConflictingClause)).findAny().isPresent();
- ;
+ && instance.canNOTProveVariableWithGroups.get(clause.getLast()).stream()
+ .filter(set -> set.containsAll(groupsSupportingConflictingClause)).findAny().isPresent();
+ ;
if (weAlreadyKnowThatWeCanNOTProveTheVariableWithTheGroups) {
continue;
diff --git a/integraal/integraal-explanation/src/test/resources/Debug/query4/query4.dlgp b/integraal/integraal-explanation/src/test/resources/Debug/query4/query4.dlgp
new file mode 100644
index 0000000000000000000000000000000000000000..521625ddf0991f05f828be8996b498d70d05088a
--- /dev/null
+++ b/integraal/integraal-explanation/src/test/resources/Debug/query4/query4.dlgp
@@ -0,0 +1,9 @@
+@facts
+<Rthree>(fInst, dInst).
+
+@rules
+[r10] <B>(constant_3_0), <Rone>(X, constant_1_1), <G>(constant_4_3), <A>(constant_1_1), <Rtwo>(X, constant_3_0), <Rfour>(X, constant_4_3) :- <D>(X).
+[r7] <B>(constant_3_0), <Rone>(X, constant_1_1), <Rthree>(X, constant_2_2), <A>(constant_1_1), <Rtwo>(X, constant_3_0), <D>(constant_2_2) :- <F>(X).
+[r14] <F>(X) :- <Rthree>(X, Graal_EE13).
+[r2] <B>(Graal_EE2) :- <Rtwo>(X, Graal_EE2).
+[r13] <E>(X) :- <B>(Graal_EE12), <Rtwo>(X, Graal_EE12), <Rone>(X, Graal_EE11), <A>(Graal_EE11).
\ No newline at end of file
diff --git a/integraal/integraal-explanation/src/test/resources/Debug/query4/query4_query.dlgp b/integraal/integraal-explanation/src/test/resources/Debug/query4/query4_query.dlgp
new file mode 100644
index 0000000000000000000000000000000000000000..4141404e1980e145b80fabe7a478cd4b94de54cd
--- /dev/null
+++ b/integraal/integraal-explanation/src/test/resources/Debug/query4/query4_query.dlgp
@@ -0,0 +1 @@
+<E>(fInst).
\ No newline at end of file