♻ Preproc

org.sat4j.pb/src/main/java/org/sat4j/pb/GaussPreprocessingPBDecorator.java → org.sat4j.pb/src/main/java/org/sat4j/pb/PreprocessibleSolver.java

@@ -8,97 +8,80 @@ import java.util.ArrayList;
 import java.util.List;
 
 import org.sat4j.core.ConstrGroup;
-import org.sat4j.pb.constraints.pb.PBConstr;
-import org.sat4j.pb.constraints.pb.SubsetSum;
 import org.sat4j.pb.preprocessing.IConstraintGroupSelectionStrategy;
+import org.sat4j.pb.preprocessing.PBPreprocessing;
 import org.sat4j.pb.preprocessing.PBPreprocessingConstraint;
-import org.sat4j.pb.preprocessing.PBPreprocessingConstraintGroup;
 import org.sat4j.specs.ContradictionException;
+import org.sat4j.specs.FakeConstr;
 import org.sat4j.specs.IConstr;
 import org.sat4j.specs.IVec;
 import org.sat4j.specs.IVecInt;
+import org.sat4j.specs.TimeoutException;
 
 /**
  * @author Thibault Falque
  * @author Romain Wallon
  */
-public class GaussPreprocessingPBDecorator extends PBSolverDecorator {
-    private final List<PBPreprocessingConstraintGroup> groups;
+public class PreprocessibleSolver extends PBSolverDecorator {
+    private final List<PBPreprocessingConstraint> constraints;
     private IConstraintGroupSelectionStrategy strategy;
+    private final PBPreprocessing preprocessor;
 
-    private final SubsetSum subset;
+    private boolean added;
 
-    private static final int MAX_ELEMENT = 100;
-
-    private static final int MAX_SUM = 4000;
-
-    public GaussPreprocessingPBDecorator(IPBSolver solver) {
+    public PreprocessibleSolver(IPBSolver solver,
+            PBPreprocessing preprocessor) {
         super(solver);
-        this.groups = new ArrayList<>();
-        this.subset = new SubsetSum(MAX_SUM, MAX_ELEMENT);
-    }
-
-    public IConstr updateDegree(IConstr ctr) {
-        if (!(ctr instanceof PBConstr)) {
-            return ctr;
-        }
-        PBConstr pbCtr = (PBConstr) ctr;
-        int[] coeffs = new int[ctr.size()];
-
-        for (int i = 0; i < ctr.size(); i++) {
-            coeffs[i] = (pbCtr.getCoefs()[i].intValue());
-        }
-
-        subset.setElements(coeffs);
+        this.preprocessor = preprocessor;
+        this.constraints = new ArrayList<>();
 
     }
 
     @Override
     public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
             throws ContradictionException {
-        PBConstr ctr = super.addAtMost(literals, coeffs, degree);
-
+        constraints.add(
+                PBPreprocessingConstraint.newAtMost(literals, coeffs, degree));
+        return FakeConstr.instance();
     }
 
     @Override
     public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
             BigInteger degree) throws ContradictionException {
-        // TODO Auto-generated method stub
-        return super.addAtMost(literals, coeffs, degree);
+        constraints.add(
+                PBPreprocessingConstraint.newAtMost(literals, coeffs, degree));
+        return FakeConstr.instance();
     }
 
     @Override
     public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
             throws ContradictionException {
-        // TODO Auto-generated method stub
-        return super.addAtLeast(literals, coeffs, degree);
+        constraints.add(
+                PBPreprocessingConstraint.newAtLeast(literals, coeffs, degree));
+        return FakeConstr.instance();
     }
 
     @Override
     public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
             BigInteger degree) throws ContradictionException {
-        // TODO Auto-generated method stub
-        return super.addAtLeast(literals, coeffs, degree);
+        constraints.add(
+                PBPreprocessingConstraint.newAtLeast(literals, coeffs, degree));
+        return FakeConstr.instance();
     }
 
     @Override
     public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
             BigInteger weight) throws ContradictionException {
-
-        PBPreprocessingConstraint pbCtr = PBPreprocessingConstraint
-                .newInstance(literals, coeffs, weight);
-        if (!strategy.add(groups, pbCtr)) {
-            PBPreprocessingConstraintGroup group = new PBPreprocessingConstraintGroup();
-            group.add(pbCtr);
-            groups.add(group);
-        }
+        constraints.add(
+                PBPreprocessingConstraint.newExactly(literals, coeffs, weight));
         return new ConstrGroup();
     }
 
     @Override
     public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
             throws ContradictionException {
-    
+        constraints.add(
+                PBPreprocessingConstraint.newExactly(literals, coeffs, weight));
         return new ConstrGroup();
     }
 
@@ -108,4 +91,52 @@ public class GaussPreprocessingPBDecorator extends PBSolverDecorator {
 
     }
 
+    private boolean addConstraints() {
+        if (!added) {
+            added = true;
+            for (PBPreprocessingConstraint c : preprocessor
+                    .preprocess(constraints)) {
+                try {
+                    c.addConstraintToSolver(decorated());
+                } catch (ContradictionException e) {
+                    return false;
+                }
+            }
+        }
+        return true;
+    }
+
+    @Override
+    public boolean isSatisfiable(boolean global) throws TimeoutException {
+        if (!addConstraints()) {
+            return false;
+        }
+        return super.isSatisfiable(global);
+    }
+
+    @Override
+    public boolean isSatisfiable(IVecInt assumps, boolean global)
+            throws TimeoutException {
+        if (!addConstraints()) {
+            return false;
+        }
+        return super.isSatisfiable(assumps, global);
+    }
+
+    @Override
+    public boolean isSatisfiable() throws TimeoutException {
+        if (!addConstraints()) {
+            return false;
+        }
+        return super.isSatisfiable();
+    }
+
+    @Override
+    public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
+        if (!addConstraints()) {
+            return false;
+        }
+        return super.isSatisfiable(assumps);
+    }
+
 }

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

@@ -1330,7 +1330,7 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
     }
 
     public static IPBSolver newGaussPreprocessingSolver() {
-        return new GaussPreprocessingPBDecorator(newCuttingPlanesPOS2020WL());
+        return new PreprocessibleSolver(newCuttingPlanesPOS2020WL());
     }
 
 }
\ No newline at end of file

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/AbstractPBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.List;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public abstract class AbstractPBPreprocessing implements PBPreprocessing {
+
+    private final PBPreprocessing next;
+
+    public AbstractPBPreprocessing(PBPreprocessing next) {
+        this.next = next;
+    }
+
+    public AbstractPBPreprocessing() {
+        this(NullPBPreprocessing.instance());
+    }
+
+    @Override
+    public List<PBPreprocessingConstraint> preprocess(
+            List<PBPreprocessingConstraint> constraints) {
+        return next.preprocess(internalPreprocess(constraints));
+    }
+
+    protected abstract List<PBPreprocessingConstraint> internalPreprocess(
+            List<PBPreprocessingConstraint> constraints);
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/EqualityConstraintPBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.List;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public class EqualityConstraintPBPreprocessing extends AbstractPBPreprocessing {
+
+    @Override
+    protected List<PBPreprocessingConstraint> internalPreprocess(
+            List<PBPreprocessingConstraint> constraints) {
+        // TODO Auto-generated method stub
+        return null;
+    }
+
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/GaussPBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public class GaussPBPreprocessing extends AbstractPBPreprocessing {
+    private final List<PBPreprocessingConstraintGroup> groups;
+    private IConstraintGroupSelectionStrategy strategy;
+
+    /**
+     * @param next
+     * @param groups
+     */
+    public GaussPBPreprocessing(PBPreprocessing next) {
+        super(next);
+        this.groups = new ArrayList<>();
+    }
+
+    @Override
+    protected List<PBPreprocessingConstraint> internalPreprocess(
+            List<PBPreprocessingConstraint> constraints) {
+        for (PBPreprocessingConstraint pbCtr : constraints) {
+            if (!strategy.add(groups, pbCtr)) {
+                PBPreprocessingConstraintGroup group = new PBPreprocessingConstraintGroup();
+                group.add(pbCtr);
+                groups.add(group);
+            }
+        }
+
+        return null;
+
+    }
+
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/ITransformConstraint.java

@@ -3,12 +3,13 @@
  */
 package org.sat4j.pb.preprocessing;
 
-import org.sat4j.specs.ISolver;
+import org.sat4j.pb.IPBSolver;
+import org.sat4j.specs.ContradictionException;
 
 /**
  * @author Thibault Falque
  *
  */
 public interface ITransformConstraint {
-    void addConstraintToSolver(ISolver solver);
+    void addConstraintToSolver(IPBSolver solver) throws ContradictionException;
 }

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/MaxDegreePBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.List;
+
+import org.sat4j.pb.constraints.pb.SubsetSum;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public class MaxDegreePBPreprocessing extends AbstractPBPreprocessing {
+    private final SubsetSum subset;
+
+    private static final int MAX_ELEMENT = 100;
+
+    private static final int MAX_SUM = 4000;
+
+    public MaxDegreePBPreprocessing(PBPreprocessing next) {
+        super(next);
+        this.subset = new SubsetSum(MAX_SUM, MAX_ELEMENT);
+    }
+
+    @Override
+    protected List<PBPreprocessingConstraint> internalPreprocess(
+            List<PBPreprocessingConstraint> constraints) {
+        // TODO Auto-generated method stub
+        return null;
+    }
+
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/NullPBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.List;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public final class NullPBPreprocessing implements PBPreprocessing {
+    private static final PBPreprocessing INSTANCE = new NullPBPreprocessing();
+
+    private NullPBPreprocessing() {
+
+    }
+
+    public static PBPreprocessing instance() {
+        return INSTANCE;
+    }
+
+    @Override
+    public List<PBPreprocessingConstraint> preprocess(
+            List<PBPreprocessingConstraint> constraints) {
+        return constraints;
+    }
+
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/PBPreprocessing.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.util.List;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public interface PBPreprocessing {
+    List<PBPreprocessingConstraint> preprocess(
+            List<PBPreprocessingConstraint> constraints);
+}

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/PBPreprocessingConstraint.java

@@ -5,9 +5,12 @@ package org.sat4j.pb.preprocessing;
 
 import java.math.BigInteger;
 
-import org.sat4j.specs.ISolver;
+import org.sat4j.core.Vec;
+import org.sat4j.pb.IPBSolver;
+import org.sat4j.specs.ContradictionException;
 import org.sat4j.specs.IVec;
 import org.sat4j.specs.IVecInt;
+import org.sat4j.specs.IteratorInt;
 
 /**
  * @author Thibault Falque
@@ -18,27 +21,80 @@ public class PBPreprocessingConstraint implements ITransformConstraint {
     private final IVec<BigInteger> coeffs;
     private final BigInteger weight;
 
+    private final PBPreprocessingConstraintType type;
+
     /**
      * @param literals
      * @param coeffs
      * @param weight
      */
     private PBPreprocessingConstraint(IVecInt literals, IVec<BigInteger> coeffs,
-            BigInteger weight) {
+            BigInteger weight, PBPreprocessingConstraintType type) {
         this.literals = literals;
         this.coeffs = coeffs;
         this.weight = weight;
+        this.type = type;
+    }
+
+    public static PBPreprocessingConstraint newExactly(IVecInt literals,
+            IVec<BigInteger> coeffs, BigInteger weight) {
+        return new PBPreprocessingConstraint(literals.clone(), coeffs.clone(),
+                weight, PBPreprocessingConstraintType.EQ);
+    }
+
+    public static PBPreprocessingConstraint newExactly(IVecInt literals,
+            IVecInt coeffs, int weight) {
+
+        return new PBPreprocessingConstraint(literals.clone(),
+                toBigInteger(coeffs), BigInteger.valueOf(weight),
+                PBPreprocessingConstraintType.EQ);
+    }
+
+    public static PBPreprocessingConstraint newAtMost(IVecInt literals,
+            IVec<BigInteger> coeffs, BigInteger weight) {
+        return new PBPreprocessingConstraint(literals.clone(), coeffs.clone(),
+                weight, PBPreprocessingConstraintType.LE);
     }
 
-    public static PBPreprocessingConstraint newInstance(IVecInt literals,
+    public static PBPreprocessingConstraint newAtMost(IVecInt literals,
+            IVecInt coeffs, int weight) {
+
+        return new PBPreprocessingConstraint(literals.clone(),
+                toBigInteger(coeffs), BigInteger.valueOf(weight),
+                PBPreprocessingConstraintType.LE);
+    }
+
+    public static PBPreprocessingConstraint newAtLeast(IVecInt literals,
             IVec<BigInteger> coeffs, BigInteger weight) {
         return new PBPreprocessingConstraint(literals.clone(), coeffs.clone(),
-                weight);
+                weight, PBPreprocessingConstraintType.GE);
+    }
+
+    public static PBPreprocessingConstraint newAtLeast(IVecInt literals,
+            IVecInt coeffs, int weight) {
+
+        return new PBPreprocessingConstraint(literals.clone(),
+                toBigInteger(coeffs), BigInteger.valueOf(weight),
+                PBPreprocessingConstraintType.GE);
+    }
+
+    /**
+     * @param coeffs
+     * @return
+     */
+    private static IVec<BigInteger> toBigInteger(IVecInt coeffs) {
+        IVec<BigInteger> localCoeffs = new Vec<>(coeffs.size());
+
+        for (IteratorInt it = coeffs.iterator(); it.hasNext();) {
+            localCoeffs.push(BigInteger.valueOf(it.next()));
+        }
+        return localCoeffs;
     }
 
     @Override
-    public void addConstraintToSolver(ISolver solver) {
-        // TODO Auto-generated method stub
+    public void addConstraintToSolver(IPBSolver solver)
+            throws ContradictionException {
+        this.type.addConstraintToSolver(literals, coeffs, weight, solver);
 
     }
 

org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/PBPreprocessingConstraintType.java

+/**
+ * 
+ */
+package org.sat4j.pb.preprocessing;
+
+import java.math.BigInteger;
+
+import org.sat4j.pb.IPBSolver;
+import org.sat4j.specs.ContradictionException;
+import org.sat4j.specs.IVec;
+import org.sat4j.specs.IVecInt;
+
+/**
+ * @author Thibault Falque
+ *
+ */
+public enum PBPreprocessingConstraintType {
+    LE {
+
+        @Override
+        public void addConstraintToSolver(IVecInt literals,
+                IVec<BigInteger> coeffs, BigInteger degree, IPBSolver solver)
+                throws ContradictionException {
+            solver.addAtMost(literals, coeffs, degree);
+
+        }
+
+    },
+    GE {
+
+        @Override
+        public void addConstraintToSolver(IVecInt literals,
+                IVec<BigInteger> coeffs, BigInteger degree, IPBSolver solver)
+                throws ContradictionException {
+            solver.addAtLeast(literals, coeffs, degree);
+
+        }
+
+    },
+    EQ
+
+    {
+
+        @Override
+        public void addConstraintToSolver(IVecInt literals,
+                IVec<BigInteger> coeffs, BigInteger degree, IPBSolver solver)
+                throws ContradictionException {
+            solver.addExactly(literals, coeffs, degree);
+
+        }
+
+    };
+
+    public abstract void addConstraintToSolver(IVecInt literals,
+            IVec<BigInteger> coeffs, BigInteger degree, IPBSolver solver)
+            throws ContradictionException;
+}