Commit 4330fd16 authored by Anne Parrain's avatar Anne Parrain
Browse files

remove incorrect CardAllImplied solver

parent 51878c17
Pipeline #133 passed with stage
in 11 minutes and 29 seconds
......@@ -65,7 +65,6 @@ import org.sat4j.pb.constraints.PuebloPBMinDataStructure;
import org.sat4j.pb.core.PBDataStructureFactory;
import org.sat4j.pb.core.PBSolver;
import org.sat4j.pb.core.PBSolverCP;
import org.sat4j.pb.core.PBSolverCPCardAllImpliedLearning;
import org.sat4j.pb.core.PBSolverCPCardLearning;
import org.sat4j.pb.core.PBSolverCPClauseLearning;
import org.sat4j.pb.core.PBSolverCPLong;
......@@ -633,18 +632,6 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver;
}
private static PBSolverCP newPBCPStarCardAllImpliedLearning(
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPCardAllImpliedLearning(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>();
......@@ -713,12 +700,6 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
new VarOrderHeapObjective(), true);
}
public static IPBSolver newCuttingPlanesStarCardAllImpliedLearning() {
return newPBCPStarCardAllImpliedLearning(
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.
......
......@@ -49,7 +49,6 @@ public class ConflictMap extends MapPb implements IConflict {
public static final int NOPOSTPROCESS = 0;
public static final int POSTPROCESSTOCLAUSE = 1;
public static final int POSTPROCESSTOCARD = 2;
public static final int POSTPROCESSTOCARDALLIMPLIED = 3;
protected boolean hasBeenReduced = false;
protected long numberOfReductions = 0;
......@@ -111,9 +110,6 @@ public class ConflictMap extends MapPb implements IConflict {
case POSTPROCESSTOCARD:
this.postProcess = new PostProcessToCard();
break;
case POSTPROCESSTOCARDALLIMPLIED:
this.postProcess = new PostProcessToCardAllImplied();
break;
default:
this.postProcess = new NoPostProcess();
break;
......@@ -474,9 +470,6 @@ public class ConflictMap extends MapPb implements IConflict {
.getFromAllLits(lit);
assert this.backtrackLevel == oldGetBacktrackLevel(dl);
// ConflictMap.this.currentSlack = ConflictMap.this
// .computeSlack(this.assertiveLevel);
// assert ConflictMap.this.isAssertive(this.backtrackLevel);
}
}
}
......@@ -548,110 +541,6 @@ public class ConflictMap extends MapPb implements IConflict {
}
private class PostProcessToCardAllImplied implements IPostProcess {
public void postProcess(int dl) {
// keep all the falsified and the implied literals at the current
// level
// construct a cardinality with a degree equals to card(implied
// literals)
if (ConflictMap.this.isAssertive(dl)
&& (!ConflictMap.this.degree.equals(BigInteger.ONE))) {
int litLevel, ilit;
IVecInt toSuppress = new VecInt();
IVecInt toKeep = detectAssertivesLiterals(dl);
int cpt = toKeep.size();
BigInteger slack = computeSlack(this.assertiveLevel)
.subtract(ConflictMap.this.degree);
for (int i = 0; i < ConflictMap.this.size(); i++) {
ilit = ConflictMap.this.weightedLits.getLit(i);
litLevel = ConflictMap.this.voc.getLevel(ilit);
if (litLevel < this.assertiveLevel
&& ConflictMap.this.voc.isFalsified(ilit)) {
toKeep.push(ilit);
} else if (((litLevel < this.assertiveLevel
&& ConflictMap.this.voc.isSatisfied(ilit))
|| (slack.compareTo(ConflictMap.this.weightedLits
.getCoef(i)) >= 0))) {
toSuppress.push(ilit);
}
}
if (cpt > 0) {
for (int i = 0; i < toKeep.size(); i++) {
ilit = ConflictMap.this.weightedLits
.getFromAllLits(toKeep.get(i));
ConflictMap.this.changeCoef(ilit, BigInteger.ONE);
}
for (int i = 0; i < toSuppress.size(); i++) {
ConflictMap.this.removeCoef(toSuppress.get(i));
}
ConflictMap.this.assertiveLiteral = ConflictMap.this.weightedLits
.getFromAllLits(toKeep.get(0));
ConflictMap.this.degree = BigInteger.valueOf(cpt);
assert this.backtrackLevel == oldGetBacktrackLevel(dl);
}
}
}
private int assertiveLevel;
private int backtrackLevel;
public IVecInt detectAssertivesLiterals(int maxLevel) {
// we are looking for a level higher than maxLevel
// where the constraint is still assertive
IVecInt lits;
int level;
int indStop = levelToIndex(maxLevel); // ou maxLevel - 1 ???
int indStart = levelToIndex(0);
BigInteger slack = ConflictMap.this.computeSlack(0)
.subtract(ConflictMap.this.degree);
int previous = 0;
IVecInt literals = new VecInt();
for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
if (ConflictMap.this.byLevel[indLevel] != null) {
level = indexToLevel(indLevel);
assert ConflictMap.this.computeSlack(level)
.subtract(ConflictMap.this.degree).equals(slack);
if (ConflictMap.this.isImplyingLiteralOrdered(level, slack,
literals)) {
this.assertiveLevel = level;
this.backtrackLevel = previous;
break;
}
// updating the new slack
lits = ConflictMap.this.byLevel[indLevel];
int lit;
for (IteratorInt iterator = lits.iterator(); iterator
.hasNext();) {
lit = iterator.next();
if (ConflictMap.this.voc.isFalsified(lit)
&& ConflictMap.this.voc.getLevel(
lit) == indexToLevel(indLevel)) {
slack = slack.subtract(
ConflictMap.this.weightedLits.get(lit));
}
}
if (!lits.isEmpty()) {
previous = level;
}
}
}
assert literals.size() > 0;
assert this.backtrackLevel == oldGetBacktrackLevel(maxLevel);
assert literals.size() > 0;
return literals;
}
public int getBacktrackLevel(int maxLevel) {
return this.backtrackLevel;
}
}
public void postProcess(int dl) {
this.postProcess.postProcess(dl);
}
......
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.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPCardAllImpliedLearning extends PBSolverCPLong {
/**
*
*/
private static final long serialVersionUID = 1L;
public PBSolverCPCardAllImpliedLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(learner, dsf, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPCardAllImpliedLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter) {
super(learner, dsf, params, order, restarter);
// TODO Auto-generated constructor stub
}
public PBSolverCPCardAllImpliedLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order) {
super(learner, dsf, params, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPCardAllImpliedLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
// TODO Auto-generated constructor stub
}
public PBSolverCPCardAllImpliedLearning(
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 PBSolverCPCardAllImpliedLearning(
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 ConflictMapReduceToClause.createConflict(myconfl, level,
noRemove, ConflictMap.POSTPROCESSTOCARDALLIMPLIED);
}
@Override
public String toString(String prefix) {
return super.toString(prefix) + "\n" + prefix
+ "Performs a post-processing after conflict analysis in order to learn only cardinality constraints with all original implied literals";
}
}
package org.sat4j.pb.constraints;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
public class PBCPMaxClauseCardConstrCardAllImpliedLearningTest
extends AbstractEZPseudoBooleanAndPigeonHoleTest {
public PBCPMaxClauseCardConstrCardAllImpliedLearningTest(String arg) {
super(arg);
}
@Override
protected IPBSolver createSolver() {
return SolverFactory.newCuttingPlanesStarCardAllImpliedLearning();
}
}
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