Commit a07b1f0a authored by Anne Parrain's avatar Anne Parrain

add new solvers ReduceBy2, ReduceByGCD, DivideByGCD and correct

DivideBy2
parent fde45e66
Pipeline #146 failed with stage
......@@ -69,8 +69,10 @@ import org.sat4j.pb.core.PBSolverCPCardLearning;
import org.sat4j.pb.core.PBSolverCPClauseLearning;
import org.sat4j.pb.core.PBSolverCPLong;
import org.sat4j.pb.core.PBSolverCPLongDivideBy2;
import org.sat4j.pb.core.PBSolverCPLongDivideByGCD;
import org.sat4j.pb.core.PBSolverCPLongReduceToCard;
import org.sat4j.pb.core.PBSolverCPLongRounding;
import org.sat4j.pb.core.PBSolverCPReduceByGCD;
import org.sat4j.pb.core.PBSolverCPReduceByPowersOf2;
//import org.sat4j.pb.core.PBSolverCard;
import org.sat4j.pb.core.PBSolverCautious;
......@@ -609,18 +611,17 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
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 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) {
......@@ -671,6 +672,18 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver;
}
private static PBSolverCP newPBCPStarDivideByGCD(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongDivideByGCD(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 newPBCPStarRounding(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
......@@ -723,10 +736,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
new VarOrderHeapObjective(), true);
}
// public static IPBSolver newCuttingPlanesReduceByGCD() {
// return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
// new VarOrderHeapObjective(), true);
// }
public static IPBSolver newCuttingPlanesReduceByGCD() {
return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
}
public static IPBSolver newCuttingPlanesStar() {
return newPBCPStar(new PBMaxClauseCardConstrDataStructure(),
......@@ -759,6 +772,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
new VarOrderHeapObjective(), true);
}
public static IPBSolver newCuttingPlanesStarDivideByGCD() {
return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
}
/**
* Cutting Planes based solver. The inference during conflict analysis is
* based on cutting planes instead of resolution as in a SAT solver.
......
......@@ -356,11 +356,11 @@ public class ConflictMap extends MapPb implements IConflict {
// saturation
this.degree = saturation();
assert slackConflict().signum() < 0;
decreaseCoefs();
divideCoefs();
return this.degree;
}
void decreaseCoefs() {
void divideCoefs() {
}
/**
......
package org.sat4j.pb.constraints.pb;
import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapReduceByGCD extends ConflictMap {
public ConflictMapReduceByGCD(PBConstr cpb, int level) {
super(cpb, level);
// TODO Auto-generated constructor stub
}
public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove) {
super(cpb, level, noRemove);
// TODO Auto-generated constructor stub
}
public ConflictMapReduceByGCD(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 ConflictMapReduceByGCD(cpb, level, true,
NoPostProcess.instance(), stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, noRemove,
NoPostProcess.instance(), stats);
}
@Override
void divideCoefs() {
int gcd = reduceCoeffsByGCD();
if (gcd > 1) {
stats.numberOfReductionsByGCD++;
}
}
}
package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapReduceByPowersOf2 extends ConflictMap {
......@@ -37,9 +35,7 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
}
@Override
void decreaseCoefs() {
String origine = this.toString();
BigInteger previousSlack = this.currentSlack;
void divideCoefs() {
int nbBits = reduceCoeffsByPower2();
if (nbBits > 0) {
stats.numberOfReductionsByPower2++;
......
......@@ -98,27 +98,27 @@ public class MapPb implements IDataStructurePB {
return 0;
}
public boolean reduceCoeffsByGCD() {
public int 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.compareTo(BigInteger.ONE) > 0; i++) {
gcd = gcd.gcd(this.weightedLits.getCoef(i));
}
if (gcd.compareTo(BigInteger.ZERO) > 0) {
if (gcd.compareTo(BigInteger.ONE) > 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);
this.degree = result[0];
if (result[1].compareTo(BigInteger.ZERO) > 0) {
this.degree = this.degree.add(BigInteger.ONE);
}
return true;
}
return false;
return gcd.intValue();
} else
return false;
return 1;
}
public boolean isCardinality() {
......
package org.sat4j.pb.constraints.pb;
public class PostProcessDivideByGCD implements IPostProcess {
private static final PostProcessDivideByGCD INSTANCE = new PostProcessDivideByGCD();
private PostProcessDivideByGCD() {
// no instantiation
}
public static final PostProcessDivideByGCD instance() {
return INSTANCE;
}
public void postProcess(int dl, ConflictMap conflictMap) {
int gcd = conflictMap.reduceCoeffsByGCD();
if (gcd > 1) {
conflictMap.stats.numberOfReductionsByGCD++;
}
}
}
......@@ -33,7 +33,7 @@ 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.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.ConflictMap;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.PostProcessDivideBy2;
......@@ -86,8 +86,8 @@ public class PBSolverCPLongDivideBy2 extends PBSolverCPLong {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToClause.createConflict(myconfl, level,
noRemove, PostProcessDivideBy2.instance(), stats);
return ConflictMap.createConflict(myconfl, level, noRemove,
PostProcessDivideBy2.instance(), stats);
}
@Override
......
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.ConflictMap;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.PostProcessDivideBy2;
public class PBSolverCPLongDivideByGCD extends PBSolverCPLong {
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(learner, dsf, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter) {
super(learner, dsf, params, order, restarter);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order) {
super(learner, dsf, params, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
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 PBSolverCPLongDivideByGCD(
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 ConflictMap.createConflict(myconfl, level, noRemove,
PostProcessDivideBy2.instance(), stats);
}
@Override
public String toString(String prefix) {
return super.toString(prefix) + "\n" + prefix
+ "Performs a post-processing after conflict analysis in order to divide by gcd over coefficients of learned constraints";
}
}
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.ConflictMapReduceByGCD;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPReduceByGCD extends PBSolverCP {
public PBSolverCPReduceByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(learner, dsf, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPReduceByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter) {
super(learner, dsf, params, order, restarter);
// TODO Auto-generated constructor stub
}
public PBSolverCPReduceByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order) {
super(learner, dsf, params, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPReduceByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
// TODO Auto-generated constructor stub
}
public PBSolverCPReduceByGCD(
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 PBSolverCPReduceByGCD(
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 ConflictMapReduceByGCD.createConflict(myconfl, level, noRemove,
stats);
}
@Override
public String toString(String prefix) {
return super.toString(prefix) + "\n" + prefix
+ "Reduce coefs as much as possible by GCD over coefficients at each step during conflict analysis";
}
}
......@@ -46,6 +46,8 @@ public class PBSolverStats extends SolverStats {
public long numberOfRightShiftsForCoeffs;
public long numberOfReductionsByGCD;
public long numberOfLearnedConstraintsReduced;
public long numberOfResolution;
......@@ -66,6 +68,7 @@ public class PBSolverStats extends SolverStats {
this.numberOfRoundingOperations = 0;
this.numberOfReductionsByPower2 = 0;
this.numberOfRightShiftsForCoeffs = 0;
this.numberOfReductionsByGCD = 0;
}
@Override
......@@ -92,6 +95,9 @@ public class PBSolverStats extends SolverStats {
out.println(
prefix + "number of right shift for reduction by power 2 \t: "
+ this.numberOfRightShiftsForCoeffs);
out.println(
prefix + "number of reductions of the coefficients by GCD over coefficients \t: "
+ this.numberOfReductionsByGCD);
}
}
package org.sat4j.pb.constraints;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
public class PBCPMaxClauseCardConstrLearningDivideByGCDTest
extends AbstractPseudoBooleanAndPigeonHoleTest {
public PBCPMaxClauseCardConstrLearningDivideByGCDTest(String arg) {
super(arg);
// TODO Auto-generated constructor stub
}
@Override
protected IPBSolver createSolver() {
return SolverFactory.newCuttingPlanesStarDivideByGCD();
}
}
package org.sat4j.pb.constraints;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
public class PBCPMaxClauseCardConstrLearningReduceByGCDTest
extends AbstractPseudoBooleanAndPigeonHoleTest {
public PBCPMaxClauseCardConstrLearningReduceByGCDTest(String arg) {
super(arg);
// TODO Auto-generated constructor stub
}
@Override
protected IPBSolver createSolver() {
return SolverFactory.newCuttingPlanesReduceByGCD();
}
}
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