Commit 185a687f authored by Romain WALLON's avatar Romain WALLON

Adds the possibility to choose whether obvious divisions should be applied automatically

parent 040fd01d
/*******************************************************************************
* 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;
import java.math.BigInteger;
/**
* The AutoDivisionStrategy enables to specify whether division should be
* applied automatically, when a common factor is identified.
*
* @author Romain WALLON
*/
public enum AutoDivisionStrategy {
/**
* The DISABLED auto-division strategy.
*/
DISABLED {
@Override
boolean isCardinality(InternalMapPBStructure weightedLits) {
return false;
}
},
/**
* The DISABLED auto-division strategy.
*/
ENABLED {
@Override
boolean isCardinality(InternalMapPBStructure weightedLits) {
BigInteger value = weightedLits.getCoef(0);
for (int i = 1; i < weightedLits.size(); i++) {
if (!weightedLits.getCoef(i).equals(value)) {
return false;
}
}
return true;
}
};
/**
* Checks out if the constraint represented by {@code weightedLits} is a
* cardinality constraint.
*
* @param weightedLits
* The structure representing the constraint.
* @return If the constraint is a cardinality constraint.
*/
abstract boolean isCardinality(InternalMapPBStructure weightedLits);
/*
* (non-Javadoc)
*
* @see java.lang.Enum#toString()
*/
@Override
public String toString() {
return "Auto-division on coefficients is " + name().toLowerCase();
}
}
...@@ -53,7 +53,6 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -53,7 +53,6 @@ public class ConflictMap extends MapPb implements IConflict {
protected long numberOfReductions = 0; protected long numberOfReductions = 0;
private boolean allowSkipping = false; private boolean allowSkipping = false;
private boolean endingSkipping = true; private boolean endingSkipping = true;
/** /**
* to store the slack of the current resolvant * to store the slack of the current resolvant
*/ */
...@@ -89,27 +88,29 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -89,27 +88,29 @@ public class ConflictMap extends MapPb implements IConflict {
boolean noRemove) { boolean noRemove) {
return new ConflictMap(cpb, level, noRemove, false, return new ConflictMap(cpb, level, noRemove, false,
NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST, NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
null); AutoDivisionStrategy.ENABLED, null);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) { boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, skip, return new ConflictMap(cpb, level, noRemove, skip,
NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST, NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
stats); AutoDivisionStrategy.ENABLED, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, IPostProcess postProcessing) { boolean noRemove, IPostProcess postProcessing) {
return new ConflictMap(cpb, level, noRemove, false, postProcessing, return new ConflictMap(cpb, level, noRemove, false, postProcessing,
IWeakeningStrategy.UNASSIGNED_FIRST, null); IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, null);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postProcessing, boolean noRemove, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, skip, postProcessing, return new ConflictMap(cpb, level, noRemove, skip, postProcessing,
weakeningStrategy, stats); weakeningStrategy, autoDivisionStrategy, stats);
} }
public static IConflictFactory factory() { public static IConflictFactory factory() {
...@@ -117,9 +118,12 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -117,9 +118,12 @@ public class ConflictMap extends MapPb implements IConflict {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMap.createConflict(cpb, level, noRemove, skip, return ConflictMap.createConflict(cpb, level, noRemove, skip,
postprocess, weakeningStrategy, stats); postprocess, weakeningStrategy, autoDivisionStrategy,
stats);
} }
@Override @Override
...@@ -131,24 +135,27 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -131,24 +135,27 @@ public class ConflictMap extends MapPb implements IConflict {
ConflictMap(PBConstr cpb, int level) { ConflictMap(PBConstr cpb, int level) {
this(cpb, level, false, false, NoPostProcess.instance(), this(cpb, level, false, false, NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST, null); IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, null);
} }
ConflictMap(PBConstr cpb, int level, boolean noRemove) { ConflictMap(PBConstr cpb, int level, boolean noRemove) {
this(cpb, level, noRemove, false, NoPostProcess.instance(), this(cpb, level, noRemove, false, NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST, null); IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, null);
} }
ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip, ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
PBSolverStats stats) { PBSolverStats stats) {
this(cpb, level, noRemove, skip, NoPostProcess.instance(), this(cpb, level, noRemove, skip, NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST, stats); IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
} }
ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip, ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy, IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy,
PBSolverStats stats) { AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove); super(cpb, level, noRemove, autoDivisionStrategy);
this.stats = stats; this.stats = stats;
this.allowSkipping = skip; this.allowSkipping = skip;
this.voc = cpb.getVocabulary(); this.voc = cpb.getVocabulary();
......
...@@ -14,23 +14,25 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -14,23 +14,25 @@ public class ConflictMapReduceByGCD extends ConflictMap {
public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postProcessing, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy, super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy,
stats); autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
PBSolverStats stats) { PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, true, false, return new ConflictMapReduceByGCD(cpb, level, true, false,
NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST, NoPostProcess.instance(), IWeakeningStrategy.UNASSIGNED_FIRST,
stats); AutoDivisionStrategy.ENABLED, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, noRemove, skip, return new ConflictMapReduceByGCD(cpb, level, noRemove, skip,
postprocess, IWeakeningStrategy.UNASSIGNED_FIRST, stats); postprocess, weakeningStrategy, autoDivisionStrategy, stats);
} }
public static IConflictFactory factory() { public static IConflictFactory factory() {
...@@ -38,9 +40,12 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -38,9 +40,12 @@ public class ConflictMapReduceByGCD extends ConflictMap {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMapReduceByGCD.createConflict(cpb, level, return ConflictMapReduceByGCD.createConflict(cpb, level,
noRemove, skip, postprocess, weakeningStrategy, stats); noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
@Override @Override
......
...@@ -6,16 +6,18 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap { ...@@ -6,16 +6,18 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
public ConflictMapReduceByPowersOf2(PBConstr cpb, int level, public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postProcessing, boolean noRemove, boolean skip, IPostProcess postProcessing,
PBSolverStats stats) { AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, super(cpb, level, noRemove, skip, postProcessing,
IWeakeningStrategy.UNASSIGNED_FIRST, stats); IWeakeningStrategy.UNASSIGNED_FIRST, autoDivisionStrategy,
stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapReduceByPowersOf2(cpb, level, noRemove, skip, return new ConflictMapReduceByPowersOf2(cpb, level, noRemove, skip,
postprocess, stats); postprocess, autoDivisionStrategy, stats);
} }
public static IConflictFactory factory() { public static IConflictFactory factory() {
...@@ -23,9 +25,12 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap { ...@@ -23,9 +25,12 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMapReduceByPowersOf2.createConflict(cpb, level, return ConflictMapReduceByPowersOf2.createConflict(cpb, level,
noRemove, skip, postprocess, weakeningStrategy, stats); noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
@Override @Override
......
...@@ -28,15 +28,18 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -28,15 +28,18 @@ public class ConflictMapReduceToCard extends ConflictMap {
public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postprocess, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
super(cpb, level, noRemove, skip, postprocess, weakeningStrategy, stats); AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapReduceToCard(cpb, level, noRemove, skip, return new ConflictMapReduceToCard(cpb, level, noRemove, skip,
postprocess, weakeningStrategy, stats); postprocess, weakeningStrategy, autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level) { public static IConflict createConflict(PBConstr cpb, int level) {
...@@ -53,9 +56,12 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -53,9 +56,12 @@ public class ConflictMapReduceToCard extends ConflictMap {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMapReduceToCard.createConflict(cpb, level, return ConflictMapReduceToCard.createConflict(cpb, level,
noRemove, skip, postprocess, weakeningStrategy, stats); noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
@Override @Override
......
...@@ -46,8 +46,10 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -46,8 +46,10 @@ public final class ConflictMapReduceToClause extends ConflictMap {
public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postprocess, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
super(cpb, level, noRemove, skip, postprocess, weakeningStrategy, stats); AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
...@@ -57,9 +59,10 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -57,9 +59,10 @@ public final class ConflictMapReduceToClause extends ConflictMap {
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapReduceToClause(cpb, level, noRemove, skip, return new ConflictMapReduceToClause(cpb, level, noRemove, skip,
postprocess, weakeningStrategy, stats); postprocess, weakeningStrategy, autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level) { public static IConflict createConflict(PBConstr cpb, int level) {
...@@ -71,9 +74,12 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -71,9 +74,12 @@ public final class ConflictMapReduceToClause extends ConflictMap {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMapReduceToClause.createConflict(cpb, level, return ConflictMapReduceToClause.createConflict(cpb, level,
noRemove, skip, postprocess, weakeningStrategy, stats); noRemove, skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
@Override @Override
......
...@@ -55,16 +55,18 @@ public class ConflictMapRounding extends ConflictMap { ...@@ -55,16 +55,18 @@ public class ConflictMapRounding extends ConflictMap {
public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove, public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postProcessing, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy, super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy,
stats); autoDivisionStrategy, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postProcessing, boolean noRemove, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, noRemove, skip, return new ConflictMapRounding(cpb, level, noRemove, skip,
postProcessing, weakeningStrategy, stats); postProcessing, weakeningStrategy, autoDivisionStrategy, stats);
} }
public static IConflictFactory factory() { public static IConflictFactory factory() {
...@@ -72,9 +74,12 @@ public class ConflictMapRounding extends ConflictMap { ...@@ -72,9 +74,12 @@ public class ConflictMapRounding extends ConflictMap {
@Override @Override
public IConflict createConflict(PBConstr cpb, int level, public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess, boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) { IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,
PBSolverStats stats) {
return ConflictMapRounding.createConflict(cpb, level, noRemove, return ConflictMapRounding.createConflict(cpb, level, noRemove,
skip, postprocess, weakeningStrategy, stats); skip, postprocess, weakeningStrategy,
autoDivisionStrategy, stats);
} }
@Override @Override
......
...@@ -6,5 +6,6 @@ public interface IConflictFactory { ...@@ -6,5 +6,6 @@ public interface IConflictFactory {
IConflict createConflict(PBConstr cpb, int level, boolean noRemove, IConflict createConflict(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postprocess, boolean skip, IPostProcess postprocess,
IWeakeningStrategy removeStrategy, PBSolverStats stats); IWeakeningStrategy removeStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats);
} }
...@@ -57,14 +57,19 @@ public class MapPb implements IDataStructurePB { ...@@ -57,14 +57,19 @@ public class MapPb implements IDataStructurePB {
private BigInteger cardDegree; private BigInteger cardDegree;
MapPb(PBConstr cpb, int level, boolean noRemove) { protected final AutoDivisionStrategy autoDivisionStrategy;
MapPb(PBConstr cpb, int level, boolean noRemove,
AutoDivisionStrategy autoDivisionStrategy) {
this.weightedLits = new InternalMapPBStructure(cpb, level, noRemove); this.weightedLits = new InternalMapPBStructure(cpb, level, noRemove);
this.degree = this.weightedLits.getComputedDegree(); this.degree = this.weightedLits.getComputedDegree();
this.autoDivisionStrategy = autoDivisionStrategy;
} }
MapPb(int size) { MapPb(int size) {
this.weightedLits = new InternalMapPBStructure(size); this.weightedLits = new InternalMapPBStructure(size);
this.degree = BigInteger.ZERO; this.degree = BigInteger.ZERO;
this.autoDivisionStrategy = AutoDivisionStrategy.ENABLED;
} }
// temporarily : just for the case where an InternalMapPBStructure // temporarily : just for the case where an InternalMapPBStructure
...@@ -72,6 +77,7 @@ public class MapPb implements IDataStructurePB { ...@@ -72,6 +77,7 @@ public class MapPb implements IDataStructurePB {
public MapPb(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree) { public MapPb(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree) {
this.weightedLits = new InternalMapPBStructure(literals, coefs); this.weightedLits = new InternalMapPBStructure(literals, coefs);
this.degree = degree; this.degree = degree;
this.autoDivisionStrategy = AutoDivisionStrategy.ENABLED;
} }
public int reduceCoeffsByPower2() { public int reduceCoeffsByPower2() {
...@@ -130,19 +136,20 @@ public class MapPb implements IDataStructurePB { ...@@ -130,19 +136,20 @@ public class MapPb implements IDataStructurePB {
break; break;
} }
} }
if (newcase) { if (newcase) {
return false; if (autoDivisionStrategy.isCardinality(this.weightedLits)) {
/*BigInteger value = this.weightedLits.getCoef(0); this.cpCardsReduction++;
for (int i = 1; i < size(); i++) { BigInteger[] division = degree
if (!this.weightedLits.getCoef(i).equals(value)) { .divideAndRemainder(this.weightedLits.getCoef(0));
return false; if (!division[1].equals(BigInteger.ZERO)) {
division[0] = division[0].add(BigInteger.ONE);
} }
this.cardDegree = division[0];
} else {
return false;
} }
this.cpCardsReduction++;
BigInteger[] division = degree.divideAndRemainder(value);
if (!division[1].equals(BigInteger.ZERO))
division[0] = division[0].add(BigInteger.ONE);
this.cardDegree = division[0];*/
} else } else
this.cardDegree = degree; this.cardDegree = degree;
return true; return true;
......
...@@ -37,6 +37,7 @@ import org.sat4j.minisat.core.Pair; ...@@ -37,6 +37,7 @@ import org.sat4j.minisat.core.Pair;
import org.sat4j.minisat.core.RestartStrategy; import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams; import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.restarts.MiniSATRestarts; import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMap; import org.sat4j.pb.constraints.pb.ConflictMap;
import org.sat4j.pb.constraints.pb.IConflict; import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IConflictFactory; import org.sat4j.pb.constraints.pb.IConflictFactory;
...@@ -74,6 +75,8 @@ public class PBSolverCP extends PBSolver { ...@@ -74,6 +75,8 @@ public class PBSolverCP extends PBSolver {
private IWeakeningStrategy weakeningStrategy = IWeakeningStrategy.UNASSIGNED_FIRST; private IWeakeningStrategy weakeningStrategy = IWeakeningStrategy.UNASSIGNED_FIRST;
private AutoDivisionStrategy autoDivisionStrategy = AutoDivisionStrategy.DISABLED;
/** /**
* @param acg * @param acg
* @param learner * @param learner
...@@ -197,7 +200,8 @@ public class PBSolverCP extends PBSolver { ...@@ -197,7 +200,8 @@ public class PBSolverCP extends PBSolver {
protected IConflict chooseConflict(PBConstr myconfl, int level) { protected IConflict chooseConflict(PBConstr myconfl, int level) {
return conflictFactory.createConflict(myconfl, level, noRemove, return conflictFactory.createConflict(myconfl, level, noRemove,
skipAllow, postprocess, weakeningStrategy, stats); skipAllow, postprocess, weakeningStrategy, autoDivisionStrategy,
stats);
} }
@Override @Override
...@@ -206,12 +210,13 @@ public class PBSolverCP extends PBSolver { ...@@ -206,12 +210,13 @@ public class PBSolverCP extends PBSolver {
+ this.getClass().getName() + ")\n" + this.getClass().getName() + ")\n"
+ (this.noRemove ? "" + (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 + (this.skipAllow ? prefix
? 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 + " - " + prefix + " - " + autoDivisionStrategy + "\n" + prefix + " - "
+ conflictFactory + "\n" + prefix + " - " + weakeningStrategy + postprocess + "\n" + prefix + " - " + conflictFactory + "\n"
+ "\n" + super.toString(prefix); + prefix + " - " + weakeningStrategy + "\n"
+ super.toString(prefix);
} }
private final IVec<String> conflictVariables = new Vec<String>(); private final IVec<String> conflictVariables = new Vec<String>();
...@@ -272,4 +277,9 @@ public class PBSolverCP extends PBSolver { ...@@ -272,4 +277,9 @@ public class PBSolverCP extends PBSolver {
this.weakeningStrategy = weakeningStrategy; this.weakeningStrategy = weakeningStrategy;
} }
public void setAutoDivisionStrategy(
AutoDivisionStrategy autoDivisionStrategy) {
this.autoDivisionStrategy = autoDivisionStrategy;
}