Added support for --rounding-weaken-strategy

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMap.java

@@ -87,26 +87,28 @@ public class ConflictMap extends MapPb implements IConflict {
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove) {
         return new ConflictMap(cpb, level, noRemove, false,
-                NoPostProcess.instance(), null);
+                NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
+                null);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, boolean skip, PBSolverStats stats) {
         return new ConflictMap(cpb, level, noRemove, skip,
-                NoPostProcess.instance(), stats);
+                NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
+                stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, IPostProcess postProcessing) {
         return new ConflictMap(cpb, level, noRemove, false, postProcessing,
-                null);
+                IWeakeningStrategy.UNASSIGNED_FIRST, null);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, boolean skip, IPostProcess postProcessing,
-            PBSolverStats stats) {
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
         return new ConflictMap(cpb, level, noRemove, skip, postProcessing,
-                stats);
+                weakeningStrategy, stats);
     }
 
     public static IConflictFactory factory() {
@@ -114,33 +116,37 @@ public class ConflictMap extends MapPb implements IConflict {
             @Override
             public IConflict createConflict(PBConstr cpb, int level,
                     boolean noRemove, boolean skip, IPostProcess postprocess,
-                    PBSolverStats stats) {
+                    IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
                 return ConflictMap.createConflict(cpb, level, noRemove, skip,
-                        postprocess, stats);
+                        postprocess, weakeningStrategy, stats);
             }
 
             @Override
             public String toString() {
-                return "Default Sat4j cutting planes";
+                return "Use constraints as they come during conflict analysis";
             }
         };
     }
 
     ConflictMap(PBConstr cpb, int level) {
-        this(cpb, level, false, false, NoPostProcess.instance(), null);
+        this(cpb, level, false, false, NoPostProcess.instance(),
+                IWeakeningStrategy.UNASSIGNED_FIRST, null);
     }
 
     ConflictMap(PBConstr cpb, int level, boolean noRemove) {
-        this(cpb, level, noRemove, false, NoPostProcess.instance(), null);
+        this(cpb, level, noRemove, false, NoPostProcess.instance(),
+                IWeakeningStrategy.UNASSIGNED_FIRST, null);
     }
 
     ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
             PBSolverStats stats) {
-        this(cpb, level, noRemove, skip, NoPostProcess.instance(), stats);
+        this(cpb, level, noRemove, skip, NoPostProcess.instance(),
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
-            IPostProcess postProcessing, PBSolverStats stats) {
+            IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy,
+            PBSolverStats stats) {
         super(cpb, level, noRemove);
         this.stats = stats;
         this.allowSkipping = skip;
@@ -149,7 +155,7 @@ public class ConflictMap extends MapPb implements IConflict {
         initStructures();
 
         this.postProcess = postProcessing;
-
+        this.weakeningStrategy = weakeningStrategy;
         if (noRemove)
             this.rmSatLit = new NoRemoveSatisfied();
         else
@@ -255,6 +261,8 @@ public class ConflictMap extends MapPb implements IConflict {
 
     private final IPostProcess postProcess;
 
+    private final IWeakeningStrategy weakeningStrategy;
+
     public void postProcess(int dl) {
         this.postProcess.postProcess(dl, this);
     }
@@ -681,27 +689,9 @@ public class ConflictMap extends MapPb implements IConflict {
             final BigInteger[] coefsBis, final int indLitImplied,
             final BigInteger degreeBis) {
         assert degreeBis.compareTo(BigInteger.ONE) > 0;
-        // search of an unassigned literal
-        int lit = -1;
-        int size = wpb.size();
-        for (int ind = 0; ind < size && lit == -1; ind++) {
-            if (coefsBis[ind].signum() != 0
-                    && this.voc.isUnassigned(wpb.get(ind))) {
-                assert coefsBis[ind].compareTo(degreeBis) < 0;
-                lit = ind;
-            }
-        }
-
-        // else, search of a satisfied literal
-        if (lit == -1) {
-            for (int ind = 0; ind < size && lit == -1; ind++) {
-                if (coefsBis[ind].signum() != 0
-                        && this.voc.isSatisfied(wpb.get(ind))
-                        && ind != indLitImplied) {
-                    lit = ind;
-                }
-            }
-        }
+        // search of a literal to remove
+        int lit = weakeningStrategy.findLiteralToRemove(this.voc, wpb, coefsBis,
+                indLitImplied, degreeBis);
 
         // a literal has been found
         assert lit != -1;

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByGCD.java

@@ -13,21 +13,24 @@ public class ConflictMapReduceByGCD extends ConflictMap {
     }
 
     public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove,
-            boolean skip, IPostProcess postProcessing, PBSolverStats stats) {
-        super(cpb, level, noRemove, skip, postProcessing, stats);
+            boolean skip, IPostProcess postProcessing,
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
+        super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy,
+                stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             PBSolverStats stats) {
         return new ConflictMapReduceByGCD(cpb, level, true, false,
-                NoPostProcess.instance(), stats);
+                NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
+                stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, boolean skip, IPostProcess postprocess,
             PBSolverStats stats) {
         return new ConflictMapReduceByGCD(cpb, level, noRemove, skip,
-                postprocess, stats);
+                postprocess, IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     public static IConflictFactory factory() {
@@ -35,9 +38,9 @@ public class ConflictMapReduceByGCD extends ConflictMap {
             @Override
             public IConflict createConflict(PBConstr cpb, int level,
                     boolean noRemove, boolean skip, IPostProcess postprocess,
-                    PBSolverStats stats) {
+                    IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
                 return ConflictMapReduceByGCD.createConflict(cpb, level,
-                        noRemove, skip, postprocess, stats);
+                        noRemove, skip, postprocess, weakeningStrategy, stats);
             }
 
             @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByPowersOf2.java

@@ -7,7 +7,8 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
     public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
             boolean noRemove, boolean skip, IPostProcess postProcessing,
             PBSolverStats stats) {
-        super(cpb, level, noRemove, skip, postProcessing, stats);
+        super(cpb, level, noRemove, skip, postProcessing,
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
@@ -22,9 +23,9 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
             @Override
             public IConflict createConflict(PBConstr cpb, int level,
                     boolean noRemove, boolean skip, IPostProcess postprocess,
-                    PBSolverStats stats) {
+                    IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
                 return ConflictMapReduceByPowersOf2.createConflict(cpb, level,
-                        noRemove, skip, postprocess, stats);
+                        noRemove, skip, postprocess, weakeningStrategy, stats);
             }
 
             @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToCard.java

@@ -27,15 +27,16 @@ public class ConflictMapReduceToCard extends ConflictMap {
     }
 
     public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove,
-            boolean skip, IPostProcess postprocess, PBSolverStats stats) {
-        super(cpb, level, noRemove, skip, postprocess, stats);
+            boolean skip, IPostProcess postprocess,
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
+        super(cpb, level, noRemove, skip, postprocess, weakeningStrategy, stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, boolean skip, IPostProcess postprocess,
-            PBSolverStats stats) {
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
         return new ConflictMapReduceToCard(cpb, level, noRemove, skip,
-                postprocess, stats);
+                postprocess, weakeningStrategy, stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level) {
@@ -52,9 +53,9 @@ public class ConflictMapReduceToCard extends ConflictMap {
             @Override
             public IConflict createConflict(PBConstr cpb, int level,
                     boolean noRemove, boolean skip, IPostProcess postprocess,
-                    PBSolverStats stats) {
+                    IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
                 return ConflictMapReduceToCard.createConflict(cpb, level,
-                        noRemove, skip, postprocess, stats);
+                        noRemove, skip, postprocess, weakeningStrategy, stats);
             }
 
             @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToClause.java

@@ -45,8 +45,9 @@ public final class ConflictMapReduceToClause extends ConflictMap {
     }
 
     public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove,
-            boolean skip, IPostProcess postprocess, PBSolverStats stats) {
-        super(cpb, level, noRemove, skip, postprocess, stats);
+            boolean skip, IPostProcess postprocess,
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
+        super(cpb, level, noRemove, skip, postprocess, weakeningStrategy, stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level,
@@ -56,9 +57,9 @@ public final class ConflictMapReduceToClause extends ConflictMap {
 
     public static IConflict createConflict(PBConstr cpb, int level,
             boolean noRemove, boolean skip, IPostProcess postprocess,
-            PBSolverStats stats) {
+            IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
         return new ConflictMapReduceToClause(cpb, level, noRemove, skip,
-                postprocess, stats);
+                postprocess, weakeningStrategy, stats);
     }
 
     public static IConflict createConflict(PBConstr cpb, int level) {
@@ -70,9 +71,9 @@ public final class ConflictMapReduceToClause extends ConflictMap {
             @Override
             public IConflict createConflict(PBConstr cpb, int level,
                     boolean noRemove, boolean skip, IPostProcess postprocess,
-                    PBSolverStats stats) {
+                    IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
                 return ConflictMapReduceToClause.createConflict(cpb, level,
-                        noRemove, skip, postprocess, stats);
+                        noRemove, skip, postprocess, weakeningStrategy, stats);
             }
 
             @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IConflictFactory.java

@@ -5,5 +5,6 @@ import org.sat4j.pb.core.PBSolverStats;
 public interface IConflictFactory {
 
     IConflict createConflict(PBConstr cpb, int level, boolean noRemove,
-            boolean skip, IPostProcess postprocess, PBSolverStats stats);
+            boolean skip, IPostProcess postprocess,
+            IWeakeningStrategy removeStrategy, PBSolverStats stats);
 }

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IWeakeningStrategy.java

+package org.sat4j.pb.constraints.pb;
+
+import java.math.BigInteger;
+
+import org.sat4j.minisat.core.ILits;
+
+/**
+ * Strategy used to reduce a PB constraint before applying the canceling
+ * addition operation.
+ * 
+ * @author leberre
+ * @since 2.3.6
+ *
+ */
+public interface IWeakeningStrategy {
+    IWeakeningStrategy UNASSIGNED_FIRST = new IWeakeningStrategy() {
+        @Override
+        public int findLiteralToRemove(ILits voc, IWatchPb wpb,
+                final BigInteger[] coefsBis, final int indLitImplied,
+                final BigInteger degreeBis) {
+            int lit = -1;
+            int size = wpb.size();
+            for (int ind = 0; ind < size && lit == -1; ind++) {
+                if (coefsBis[ind].signum() != 0
+                        && voc.isUnassigned(wpb.get(ind))) {
+                    assert coefsBis[ind].compareTo(degreeBis) < 0;
+                    lit = ind;
+                }
+            }
+
+            if (lit == -1) {
+                for (int ind = 0; ind < size && lit == -1; ind++) {
+                    if (coefsBis[ind].signum() != 0
+                            && voc.isSatisfied(wpb.get(ind))
+                            && ind != indLitImplied) {
+                        lit = ind;
+                    }
+                }
+            }
+            return lit;
+        }
+
+        @Override
+        public String toString() {
+            return "Weaken first using unassigned literals";
+        }
+    };
+
+    IWeakeningStrategy SATISFIED_FIRST = new IWeakeningStrategy() {
+        @Override
+        public int findLiteralToRemove(ILits voc, IWatchPb wpb,
+                final BigInteger[] coefsBis, final int indLitImplied,
+                final BigInteger degreeBis) {
+            int lit = -1;
+            int size = wpb.size();
+            for (int ind = 0; ind < size && lit == -1; ind++) {
+                if (coefsBis[ind].signum() != 0
+                        && voc.isSatisfied(wpb.get(ind))) {
+                    assert coefsBis[ind].compareTo(degreeBis) < 0;
+                    lit = ind;
+                }
+            }
+
+            if (lit == -1) {
+                for (int ind = 0; ind < size && lit == -1; ind++) {
+                    if (coefsBis[ind].signum() != 0
+                            && voc.isUnassigned(wpb.get(ind))
+                            && ind != indLitImplied) {
+                        lit = ind;
+                    }
+                }
+            }
+            return lit;
+        }
+
+        @Override
+        public String toString() {
+            return "Weaken first using satisfied literals";
+        }
+    };
+
+    IWeakeningStrategy ANY = new IWeakeningStrategy() {
+        @Override
+        public int findLiteralToRemove(ILits voc, IWatchPb wpb,
+                final BigInteger[] coefsBis, final int indLitImplied,
+                final BigInteger degreeBis) {
+            int lit = -1;
+            int size = wpb.size();
+            for (int ind = 0; ind < size && lit == -1; ind++) {
+                if (coefsBis[ind].signum() != 0
+                        && !voc.isFalsified(wpb.get(ind))) {
+                    assert coefsBis[ind].compareTo(degreeBis) < 0;
+                    lit = ind;
+                }
+            }
+
+            return lit;
+        }
+
+        @Override
+        public String toString() {
+            return "Weaken with no priority";
+        }
+    };
+
+    int findLiteralToRemove(ILits voc, IWatchPb wpb,
+            final BigInteger[] coefsBis, final int indLitImplied,
+            final BigInteger degreeBis);
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java

@@ -41,6 +41,7 @@ import org.sat4j.pb.constraints.pb.ConflictMap;
 import org.sat4j.pb.constraints.pb.IConflict;
 import org.sat4j.pb.constraints.pb.IConflictFactory;
 import org.sat4j.pb.constraints.pb.IPostProcess;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.NoPostProcess;
 import org.sat4j.pb.constraints.pb.PBConstr;
 import org.sat4j.specs.Constr;
@@ -71,6 +72,8 @@ public class PBSolverCP extends PBSolver {
 
     private IPostProcess postprocess = NoPostProcess.instance();
 
+    private IWeakeningStrategy weakeningStrategy = IWeakeningStrategy.UNASSIGNED_FIRST;
+
     /**
      * @param acg
      * @param learner
@@ -200,7 +203,7 @@ public class PBSolverCP extends PBSolver {
 
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return conflictFactory.createConflict(myconfl, level, noRemove,
-                skipAllow, postprocess, stats);
+                skipAllow, postprocess, weakeningStrategy, stats);
     }
 
     @Override
@@ -208,12 +211,13 @@ public class PBSolverCP extends PBSolver {
         return prefix + "Cutting planes based inference ("
                 + this.getClass().getName() + ")\n"
                 + (this.noRemove ? ""
-                        : prefix + " - removing satisfied literals at a higher level before CP \n")
+                        : prefix + " - Removing satisfied literals at a higher level before CP \n")
                 + (this.skipAllow ? prefix
-                        + " - skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
+                        + " - Skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
                         : "")
-                + prefix + postprocess + "\n" + prefix + conflictFactory + "\n"
-                + super.toString(prefix);
+                + prefix + " - " + postprocess + "\n" + prefix + " - "
+                + conflictFactory + "\n" + prefix + " - " + weakeningStrategy
+                + "\n" + super.toString(prefix);
     }
 
     private final IVec<String> conflictVariables = new Vec<String>();
@@ -266,4 +270,12 @@ public class PBSolverCP extends PBSolver {
         this.postprocess = postprocess;
     }
 
+    public IWeakeningStrategy getWeakeningStrategy() {
+        return weakeningStrategy;
+    }
+
+    public void setWeakeningStrategy(IWeakeningStrategy weakeningStrategy) {
+        this.weakeningStrategy = weakeningStrategy;
+    }
+
 }

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPCardLearning.java

@@ -35,6 +35,7 @@ import org.sat4j.minisat.core.RestartStrategy;
 import org.sat4j.minisat.core.SearchParams;
 import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
 import org.sat4j.pb.constraints.pb.IConflict;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.PBConstr;
 import org.sat4j.pb.constraints.pb.PostProcessToCard;
 
@@ -89,7 +90,7 @@ public class PBSolverCPCardLearning extends PBSolverCPLong {
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceToClause.createConflict(myconfl, level,
                 isNoRemove(), isSkipAllow(), PostProcessToCard.instance(),
-                stats);
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPClauseLearning.java

@@ -35,6 +35,7 @@ import org.sat4j.minisat.core.RestartStrategy;
 import org.sat4j.minisat.core.SearchParams;
 import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
 import org.sat4j.pb.constraints.pb.IConflict;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.PBConstr;
 import org.sat4j.pb.constraints.pb.PostProcessToClause;
 
@@ -94,7 +95,7 @@ public class PBSolverCPClauseLearning extends PBSolverCPLong {
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceToClause.createConflict(myconfl, level,
                 isNoRemove(), isSkipAllow(), PostProcessToClause.instance(),
-                stats);
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongDivideBy2.java

@@ -35,6 +35,7 @@ import org.sat4j.minisat.core.RestartStrategy;
 import org.sat4j.minisat.core.SearchParams;
 import org.sat4j.pb.constraints.pb.ConflictMap;
 import org.sat4j.pb.constraints.pb.IConflict;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.PBConstr;
 import org.sat4j.pb.constraints.pb.PostProcessDivideBy2;
 
@@ -88,7 +89,8 @@ public class PBSolverCPLongDivideBy2 extends PBSolverCPLong {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMap.createConflict(myconfl, level, isNoRemove(),
-                isSkipAllow(), PostProcessDivideBy2.instance(), stats);
+                isSkipAllow(), PostProcessDivideBy2.instance(),
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongDivideByGCD.java

@@ -6,6 +6,7 @@ import org.sat4j.minisat.core.RestartStrategy;
 import org.sat4j.minisat.core.SearchParams;
 import org.sat4j.pb.constraints.pb.ConflictMap;
 import org.sat4j.pb.constraints.pb.IConflict;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.PBConstr;
 import org.sat4j.pb.constraints.pb.PostProcessDivideBy2;
 
@@ -65,7 +66,8 @@ public class PBSolverCPLongDivideByGCD extends PBSolverCPLong {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMap.createConflict(myconfl, level, isNoRemove(),
-                isSkipAllow(), PostProcessDivideBy2.instance(), stats);
+                isSkipAllow(), PostProcessDivideBy2.instance(),
+                IWeakeningStrategy.UNASSIGNED_FIRST, stats);
     }
 
     @Override

org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java

@@ -20,6 +20,7 @@ import org.sat4j.pb.constraints.pb.ConflictMapReduceByGCD;
 import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
 import org.sat4j.pb.constraints.pb.ConflictMapReduceToCard;
 import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
+import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
 import org.sat4j.pb.constraints.pb.PostProcessToCard;
 import org.sat4j.pb.constraints.pb.PostProcessToClause;
 import org.sat4j.pb.core.PBSolverCP;
@@ -205,10 +206,14 @@ public class KTHLauncher {
                 String value = line.getOptionValue("rounding-weaken-priority");
                 switch (value) {
                 case "unassigned": 
-                    // by default
+                    solver.setWeakeningStrategy(IWeakeningStrategy.UNASSIGNED_FIRST);
                     break;
                 case "satisfied":
+                    solver.setWeakeningStrategy(IWeakeningStrategy.SATISFIED_FIRST);
+                    break;
                 case "any":
+                    solver.setWeakeningStrategy(IWeakeningStrategy.ANY);
+                    break;
                 default:
                     log(value
                             + " is not a supported value for option rounding-weaken-priority");