Commit eee4ccab authored by parrain's avatar parrain
Browse files

AP: reduce (when possible and as much as possible) by powers of 2 coefficients...

AP: reduce (when possible and as much as possible) by powers of 2 coefficients of learnt constraints

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2546 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent fe44b8c5
......@@ -51,7 +51,8 @@ public interface IDataStructurePB {
BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
BigInteger degreeCons, BigInteger coefMult);
void buildConstraintFromConflict(IVecInt resLits, IVec<BigInteger> resCoefs);
void buildConstraintFromConflict(IVecInt resLits,
IVec<BigInteger> resCoefs);
void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs);
......@@ -67,4 +68,6 @@ public interface IDataStructurePB {
boolean isLongSufficient();
int reduceCoeffsByPower2();
}
......@@ -74,6 +74,26 @@ public class MapPb implements IDataStructurePB {
this.degree = degree;
}
public int reduceCoeffsByPower2() {
int nbBits = 1;
for (int i = 0; i < this.weightedLits.size() && nbBits > 0; i++)
nbBits = Math.min(nbBits,
this.weightedLits.getCoef(i).getLowestSetBit());
if (nbBits > 0) {
for (int i = 0; i < this.weightedLits.size(); i++) {
this.weightedLits.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;
}
public boolean isCardinality() {
boolean newcase = false;
for (int i = 0; i < size(); i++) {
......@@ -276,8 +296,8 @@ public class MapPb implements IDataStructurePB {
}
void decreaseCoef(int lit, BigInteger decCoef) {
this.weightedLits
.put(lit, this.weightedLits.get(lit).subtract(decCoef));
this.weightedLits.put(lit,
this.weightedLits.get(lit).subtract(decCoef));
}
void setCoef(int lit, BigInteger newValue) {
......
......@@ -109,7 +109,8 @@ public class PBSolverCP extends PBSolver {
}
}
public void analyzeCP(Constr myconfl, Pair results) throws TimeoutException {
public void analyzeCP(Constr myconfl, Pair results)
throws TimeoutException {
int litImplied = this.trail.last();
int currentLevel = this.voc.getLevel(litImplied);
IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
......@@ -155,13 +156,19 @@ public class PBSolverCP extends PBSolver {
// are kept from the conflict
if (confl.size() == 0
|| (decisionLevel() == 0 || this.trail.size() == 0)
&& confl.slackConflict().signum() < 0) {
&& confl.slackConflict().signum() < 0) {
results.reason = null;
results.backtrackLevel = -1;
return;
}
// assertive PB-constraint is build and referenced
int nbBits = confl.reduceCoeffsByPower2();
if (nbBits > 0) {
stats.numberOfReductionsByPower2++;
stats.numberOfRightShiftsForCoeffs = stats.numberOfRightShiftsForCoeffs
+ nbBits;
}
PBConstr resConstr = (PBConstr) this.dsfactory
.createUnregisteredPseudoBooleanConstraint(confl);
results.reason = resConstr;
......@@ -169,9 +176,8 @@ public class PBSolverCP extends PBSolver {
// the conflict give the highest decision level for the backtrack
// (which is less than current level)
// assert confl.isAssertive(currentLevel);
if (decisionLevel() == 0
|| (this.trail.size() == 0 && confl
.getBacktrackLevel(currentLevel) > 0)) {
if (decisionLevel() == 0 || (this.trail.size() == 0
&& confl.getBacktrackLevel(currentLevel) > 0)) {
results.backtrackLevel = -1;
results.reason = null;
} else {
......@@ -185,10 +191,8 @@ public class PBSolverCP extends PBSolver {
@Override
public String toString(String prefix) {
return prefix
+ "Cutting planes based inference ("
+ this.getClass().getName()
+ ")"
return prefix + "Cutting planes based inference ("
+ this.getClass().getName() + ")"
+ (this.noRemove ? ""
: " - removing satisfied literals at a higher level before CP -")
+ "\n" + super.toString(prefix);
......
......@@ -42,6 +42,10 @@ public class PBSolverStats extends SolverStats {
public long numberOfReductions;
public long numberOfReductionsByPower2;
public long numberOfRightShiftsForCoeffs;
public long numberOfLearnedConstraintsReduced;
public long numberOfResolution;
......@@ -60,6 +64,8 @@ public class PBSolverStats extends SolverStats {
this.numberOfResolution = 0;
this.numberOfCP = 0;
this.numberOfRoundingOperations = 0;
this.numberOfReductionsByPower2 = 0;
this.numberOfRightShiftsForCoeffs = 0;
}
@Override
......@@ -80,6 +86,12 @@ public class PBSolverStats extends SolverStats {
out.println(
prefix + "number of easy rounding to 1 operations (no literal elimination needed)\t: "
+ this.numberOfEasyRoundingOperations);
out.println(
prefix + "number of reductions of the coefficients by power 2 \t: "
+ this.numberOfReductionsByPower2);
out.println(
prefix + "number of right shift for reduction by power 2 \t: "
+ this.numberOfRightShiftsForCoeffs);
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment