Commit fb94a3d5 authored by Anne Parrain's avatar Anne Parrain

add a new solver post-processing conflict into a cardinality preserving

implication of all literals => does not suit for instances needing
cutting planes
correct card and clause post-processing to choose "best" assertive
literal (at the upper level of decision, with the biggest coefficient in
case of card post-processing)
parent 30f7829a
Pipeline #116 passed with stage
in 11 minutes and 25 seconds
......@@ -65,6 +65,7 @@ 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;
......@@ -632,6 +633,18 @@ 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>();
......@@ -700,6 +713,12 @@ 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.
......
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";
}
}
......@@ -65,7 +65,7 @@ public class PBSolverCPCardLearning extends PBSolverCPLong {
@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 caonstraints";
+ "Performs a post-processing after conflict analysis in order to learn only cardinality constraints (Dixon's procedure)";
}
}
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