add a new PBCP solver CuttingPlanesReduceByPowersOf2 (divide by 2

coefficients as much as possible during conflict analysis)

org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java

@@ -71,6 +71,7 @@ import org.sat4j.pb.core.PBSolverCPLong;
 import org.sat4j.pb.core.PBSolverCPLongDivideBy2;
 import org.sat4j.pb.core.PBSolverCPLongReduceToCard;
 import org.sat4j.pb.core.PBSolverCPLongRounding;
+import org.sat4j.pb.core.PBSolverCPReduceByPowersOf2;
 //import org.sat4j.pb.core.PBSolverCard;
 import org.sat4j.pb.core.PBSolverCautious;
 import org.sat4j.pb.core.PBSolverClause;
@@ -596,6 +597,31 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
         return solver;
     }
 
+    private static PBSolverCP newPBCPReduceByPowersOf2(
+            PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
+        MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
+        PBSolverCP solver = new PBSolverCPReduceByPowersOf2(learning, dsf,
+                order, noRemove);
+        learning.setDataStructureFactory(solver.getDSFactory());
+        learning.setVarActivityListener(solver);
+        solver.setRestartStrategy(new ArminRestarts());
+        solver.setLearnedConstraintsDeletionStrategy(solver.lbd_based);
+        return solver;
+    }
+
+    // private static PBSolverCP newPBCPReduceByGCD(PBDataStructureFactory dsf,
+    // IOrder order, boolean noRemove) {
+    // MiniSATLearning<PBDataStructureFactory> learning = new
+    // MiniSATLearning<PBDataStructureFactory>();
+    // PBSolverCP solver = new PBSolverCPReduceByGCD(learning, dsf, order,
+    // noRemove);
+    // learning.setDataStructureFactory(solver.getDSFactory());
+    // learning.setVarActivityListener(solver);
+    // solver.setRestartStrategy(new ArminRestarts());
+    // solver.setLearnedConstraintsDeletionStrategy(solver.lbd_based);
+    // return solver;
+    // }
+
     private static PBSolverCP newPBCPStar(PBDataStructureFactory dsf,
             IOrder order, boolean noRemove) {
         MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
@@ -691,6 +717,17 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
         return newCompetPBCPMixedConstraintsMinObjective();
     }
 
+    public static IPBSolver newCuttingPlanesReduceByPowersOf2() {
+        return newPBCPReduceByPowersOf2(
+                new PBMaxClauseCardConstrDataStructure(),
+                new VarOrderHeapObjective(), true);
+    }
+
+    // public static IPBSolver newCuttingPlanesReduceByGCD() {
+    // return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
+    // new VarOrderHeapObjective(), true);
+    // }
+
     public static IPBSolver newCuttingPlanesStar() {
         return newPBCPStar(new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective(), true);

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

@@ -356,10 +356,13 @@ public class ConflictMap extends MapPb implements IConflict {
         // saturation
         this.degree = saturation();
         assert slackConflict().signum() < 0;
-
+        decreaseCoefs();
         return this.degree;
     }
 
+    void decreaseCoefs() {
+    }
+
     /**
      * possReducedCoefs is used to update on the fly the slack of the wpb
      * constraint with reduced coefficients. possReducedCoefs is needed in
@@ -534,31 +537,16 @@ public class ConflictMap extends MapPb implements IConflict {
         BigInteger tmp;
         int level = levelToIndex(this.currentLevel);
         if (this.byLevel[level] != null) {
-            // first falsified ones
             for (IteratorInt iterator = this.byLevel[level].iterator(); iterator
                     .hasNext();) {
                 lit = iterator.next();
                 tmp = this.weightedLits.get(lit);
-                if (tmp != null // && !this.voc.isUnassigned(lit)
-                        && slack.compareTo(tmp) < 0) {
+                if (tmp != null && slack.compareTo(tmp) < 0) {
                     this.assertiveLiteral = this.weightedLits
                             .getFromAllLits(lit);
                     return true;
                 }
             }
-            // second, satisfied ones
-            // for (IteratorInt iterator = this.byLevel[level].iterator();
-            // iterator
-            // .hasNext();) {
-            // lit = iterator.next();
-            // tmp = this.weightedLits.get(lit);
-            // if (tmp != null && this.voc.isSatisfied(lit)
-            // && slack.compareTo(tmp) < 0) {
-            // this.assertiveLiteral = this.weightedLits
-            // .getFromAllLits(lit);
-            // return true;
-            // }
-            // }
         }
         return false;
     }

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

-/*******************************************************************************
- * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
- *
- * All rights reserved. This program and the accompanying materials
- * are made available under the terms of the Eclipse Public License v1.0
- * which accompanies this distribution, and is available at
- *  http://www.eclipse.org/legal/epl-v10.html
- *
- * Alternatively, the contents of this file may be used under the terms of
- * either the GNU Lesser General Public License Version 2.1 or later (the
- * "LGPL"), in which case the provisions of the LGPL are applicable instead
- * of those above. If you wish to allow use of your version of this file only
- * under the terms of the LGPL, and not to allow others to use your version of
- * this file under the terms of the EPL, indicate your decision by deleting
- * the provisions above and replace them with the notice and other provisions
- * required by the LGPL. If you do not delete the provisions above, a recipient
- * may use your version of this file under the terms of the EPL or the LGPL.
- *
- * Based on the original MiniSat specification from:
- *
- * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
- * Sixth International Conference on Theory and Applications of Satisfiability
- * Testing, LNCS 2919, pp 502-518, 2003.
- *
- * See www.minisat.se for the original solver in C++.
- *
- * Contributors:
- *   CRIL - initial API and implementation
- *******************************************************************************/
-package org.sat4j.pb.constraints.pb;
-
-public final class ConflictMapCardinality extends ConflictMap {
-
-    public ConflictMapCardinality(PBConstr cpb, int level) {
-        super(cpb, level);
-        // TODO Auto-generated constructor stub
-    }
-
-}

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

+package org.sat4j.pb.constraints.pb;
+
+import java.math.BigInteger;
+
+import org.sat4j.pb.core.PBSolverStats;
+
+public class ConflictMapReduceByPowersOf2 extends ConflictMap {
+
+    public ConflictMapReduceByPowersOf2(PBConstr cpb, int level) {
+        super(cpb, level);
+        // TODO Auto-generated constructor stub
+    }
+
+    public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
+            boolean noRemove) {
+        super(cpb, level, noRemove);
+        // TODO Auto-generated constructor stub
+    }
+
+    public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
+            boolean noRemove, IPostProcess postProcessing,
+            PBSolverStats stats) {
+        super(cpb, level, noRemove, postProcessing, stats);
+        // TODO Auto-generated constructor stub
+    }
+
+    public static IConflict createConflict(PBConstr cpb, int level,
+            PBSolverStats stats) {
+        return new ConflictMapReduceByPowersOf2(cpb, level, true,
+                NoPostProcess.instance(), stats);
+    }
+
+    public static IConflict createConflict(PBConstr cpb, int level,
+            boolean noRemove, PBSolverStats stats) {
+        return new ConflictMapReduceByPowersOf2(cpb, level, noRemove,
+                NoPostProcess.instance(), stats);
+    }
+
+    @Override
+    void decreaseCoefs() {
+        String origine = this.toString();
+        BigInteger previousSlack = this.currentSlack;
+        int nbBits = reduceCoeffsByPower2();
+        if (nbBits > 0) {
+            stats.numberOfReductionsByPower2++;
+            stats.numberOfRightShiftsForCoeffs = stats.numberOfRightShiftsForCoeffs
+                    + nbBits;
+        }
+    }
+
+}

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

@@ -75,27 +75,50 @@ public class MapPb implements IDataStructurePB {
     }
 
     public int reduceCoeffsByPower2() {
-        assert this.weightedLits.size() > 0;
-        int nbBits = this.weightedLits.getCoef(0).bitLength();
-        for (int i = 0; i < this.weightedLits.size() && nbBits > 0; i++) {
-            nbBits = Math.min(nbBits,
-                    this.weightedLits.getCoef(i).getLowestSetBit());
-            if (nbBits == 0)
-                break;
-        }
-        if (nbBits > 0) {
-            for (int i = 0; i < this.weightedLits.size(); i++) {
-                this.weightedLits.changeCoef(i,
-                        this.weightedLits.getCoef(i).shiftRight(nbBits));
+        if (this.weightedLits.size() > 0) {
+            int nbBits = this.weightedLits.getCoef(0).bitLength();
+            for (int i = 0; i < this.weightedLits.size() && nbBits > 0; i++) {
+                nbBits = Math.min(nbBits,
+                        this.weightedLits.getCoef(i).getLowestSetBit());
             }
-            // diviser le degre
-            int nbBitsDegree = this.degree.getLowestSetBit();
-            this.degree = this.degree.shiftRight(nbBits);
-            if (nbBitsDegree < nbBits) {
-                this.degree = this.degree.add(BigInteger.ONE);
+            if (nbBits > 0) {
+                for (int i = 0; i < this.weightedLits.size(); i++) {
+                    changeCoef(i,
+                            this.weightedLits.getCoef(i).shiftRight(nbBits));
+                }
+                // diviser le degre
+                int nbBitsDegree = this.degree.getLowestSetBit();
+                this.degree = this.degree.shiftRight(nbBits);
+                if (nbBitsDegree < nbBits) {
+                    this.degree = this.degree.add(BigInteger.ONE);
+                }
             }
-        }
-        return nbBits;
+            return nbBits;
+        } else
+            return 0;
+    }
+
+    public boolean reduceCoeffsByGCD() {
+        if (this.weightedLits.size() > 0) {
+            BigInteger gcd = this.weightedLits.getCoef(0);
+            for (int i = 0; i < this.weightedLits.size()
+                    && gcd.compareTo(BigInteger.ZERO) > 0; i++) {
+                gcd = gcd.gcd(this.weightedLits.getCoef(i));
+            }
+            if (gcd.compareTo(BigInteger.ZERO) > 0) {
+                for (int i = 0; i < this.weightedLits.size(); i++) {
+                    changeCoef(i, this.weightedLits.getCoef(i).divide(gcd));
+                }
+                // diviser le degre
+                BigInteger[] result = this.degree.divideAndRemainder(gcd);
+                if (result[1].compareTo(BigInteger.ZERO) > 0) {
+                    this.degree = this.degree.add(BigInteger.ONE);
+                }
+                return true;
+            }
+            return false;
+        } else
+            return false;
     }
 
     public boolean isCardinality() {

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

+package org.sat4j.pb.core;
+
+import org.sat4j.minisat.core.IOrder;
+import org.sat4j.minisat.core.LearningStrategy;
+import org.sat4j.minisat.core.RestartStrategy;
+import org.sat4j.minisat.core.SearchParams;
+import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
+import org.sat4j.pb.constraints.pb.IConflict;
+import org.sat4j.pb.constraints.pb.PBConstr;
+
+public class PBSolverCPReduceByPowersOf2 extends PBSolverCP {
+
+    /**
+     * 
+     */
+    private static final long serialVersionUID = 1L;
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, IOrder order) {
+        super(learner, dsf, order);
+        // TODO Auto-generated constructor stub
+    }
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, SearchParams params, IOrder order,
+            RestartStrategy restarter) {
+        super(learner, dsf, params, order, restarter);
+        // TODO Auto-generated constructor stub
+    }
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, SearchParams params, IOrder order) {
+        super(learner, dsf, params, order);
+        // TODO Auto-generated constructor stub
+    }
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
+        super(learner, dsf, order, noRemove);
+        // TODO Auto-generated constructor stub
+    }
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, SearchParams params, IOrder order,
+            RestartStrategy restarter, boolean noRemove) {
+        super(learner, dsf, params, order, restarter, noRemove);
+        // TODO Auto-generated constructor stub
+    }
+
+    public PBSolverCPReduceByPowersOf2(
+            LearningStrategy<PBDataStructureFactory> learner,
+            PBDataStructureFactory dsf, SearchParams params, IOrder order,
+            boolean noRemove) {
+        super(learner, dsf, params, order, noRemove);
+        // TODO Auto-generated constructor stub
+    }
+
+    @Override
+    protected IConflict chooseConflict(PBConstr myconfl, int level) {
+        return ConflictMapReduceByPowersOf2.createConflict(myconfl, level,
+                noRemove, stats);
+    }
+
+    @Override
+    public String toString(String prefix) {
+        return super.toString(prefix) + "\n" + prefix
+                + "Reduce coefs as much as possible by powers of 2 at each step during conflict analysis";
+    }
+
+}

org.sat4j.pb/src/test/java/org/sat4j/pb/constraints/PBCPMaxClauseCardConstrLearningReduceCoefsByPowersOf2Test.java

+package org.sat4j.pb.constraints;
+
+import org.sat4j.pb.IPBSolver;
+import org.sat4j.pb.SolverFactory;
+
+public class PBCPMaxClauseCardConstrLearningReduceCoefsByPowersOf2Test
+        extends AbstractPseudoBooleanAndPigeonHoleTest {
+
+    public PBCPMaxClauseCardConstrLearningReduceCoefsByPowersOf2Test(String arg) {
+        super(arg);
+        // TODO Auto-generated constructor stub
+    }
+
+    @Override
+    protected IPBSolver createSolver() {
+        return SolverFactory.newCuttingPlanesReduceByPowersOf2();
+    }
+
+}