Merge pull request #231 from alpha-asp/clause_minimization_local

Add learned clause minimization.

src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java

@@ -418,12 +418,11 @@ private ConflictCause addAndWatchBinary(final NoGood noGood) {
 			return new ConflictCause(noGood.asAntecedent());
 		}
 
-		ConflictCause conflictCause = binaryWatches[a].add(noGood);
-		if (conflictCause != null) {
-			return conflictCause;
-		}
+		// The above violation check guarantees that adding (and propagation on other literal) results in no conflict.
+		binaryWatches[a].add(noGood);
+		binaryWatches[b].add(noGood);
 		hasBinaryNoGoods = true;
-		return binaryWatches[b].add(noGood);
+		return null;
 	}
 
 	private ConflictCause assignWeakComplement(final int literalIndex, final NoGoodInterface impliedBy, int decisionLevel) {

src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java

@@ -229,11 +229,7 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) {
 		// Add the 1UIP literal.
 		resolutionLiterals.add(atomToLiteral(nextAtom, assignment.getTruth(nextAtom).toBoolean()));
 
-		int[] learnedLiterals = new int[resolutionLiterals.size()];
-		int i = 0;
-		for (Integer resolutionLiteral : resolutionLiterals) {
-			learnedLiterals[i++] = resolutionLiteral;
-		}
+		int[] learnedLiterals = minimizeLearnedLiterals(resolutionLiterals, seenAtoms);
 
 		NoGood learnedNoGood = NoGood.learnt(learnedLiterals);
 		if (LOGGER.isTraceEnabled()) {
@@ -254,6 +250,37 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) {
 		return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, resolutionAtoms, computeLBD(learnedLiterals));
 	}
 
+	private int[] minimizeLearnedLiterals(List<Integer> resolutionLiterals, Set<Integer> seenAtoms) {
+		int[] learnedLiterals = new int[resolutionLiterals.size()];
+		int i = 0;
+		// Do local clause minimization: if an implied literal has all its antecedents seen (i.e., in the clause already), it can be removed.
+		learnedLiteralsLoop:
+		for (Integer resolutionLiteral : resolutionLiterals) {
+			if (assignment.getWeakDecisionLevel(atomOf(resolutionLiteral)) == 0) {
+				// Skip literals from decision level 0.
+				continue;
+			}
+			Antecedent antecedent = assignment.getImpliedBy(atomOf(resolutionLiteral));
+			if (antecedent == null) {
+				// The resolutionLiteral is a decision, keep it.
+				learnedLiterals[i++] = resolutionLiteral;
+			} else {
+				for (int antecedentReasonLiteral : antecedent.getReasonLiterals()) {
+					// Only add current resolutionLiteral if at least one of its antecedents has not been seen already.
+					if (!seenAtoms.contains(atomOf(antecedentReasonLiteral))) {
+						learnedLiterals[i++] = resolutionLiteral;
+						continue learnedLiteralsLoop;
+					}
+				}
+			}
+		}
+		// Shrink array if we did not copy over all literals from resolutionLiterals.
+		if (i < resolutionLiterals.size()) {
+			learnedLiterals = Arrays.copyOf(learnedLiterals, i);
+		}
+		return learnedLiterals;
+	}
+
 	private int computeLBD(int[] literals) {
 		HashSet<Integer> occurringDecisionLevels = new HashSet<>();
 		for (int literal : literals) {