Commit 4e856a4d authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'cdcl-strategies' into 'master'

Cdcl strategies

See merge request !6
parents c3d638ad 91bce9d3
Pipeline #9496 passed with stages
in 107 minutes and 3 seconds
/dist
/bin
/target
*.class
*.rupproof
*/.gitignore
......@@ -8,9 +8,9 @@
</classpathentry>
<classpathentry kind="src" output="target/test-classes" path="src/test/java">
<attributes>
<attribute name="test" value="true"/>
<attribute name="optional" value="true"/>
<attribute name="maven.pomderived" value="true"/>
<attribute name="test" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
......@@ -19,8 +19,9 @@
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7">
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8">
<attributes>
<attribute name="module" value="true"/>
<attribute name="maven.pomderived" value="true"/>
</attributes>
</classpathentry>
......
......@@ -11,17 +11,18 @@ org.eclipse.jdt.core.codeComplete.staticFinalFieldPrefixes=
org.eclipse.jdt.core.codeComplete.staticFinalFieldSuffixes=
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.6
org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning
org.eclipse.jdt.core.compiler.source=1.6
org.eclipse.jdt.core.compiler.source=1.8
org.eclipse.jdt.core.formatter.align_type_members_on_columns=false
org.eclipse.jdt.core.formatter.alignment_for_additive_operator=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=0
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=16
......@@ -29,17 +30,20 @@ org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_c
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=16
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=16
org.eclipse.jdt.core.formatter.alignment_for_assignment=0
org.eclipse.jdt.core.formatter.alignment_for_binary_expression=16
org.eclipse.jdt.core.formatter.alignment_for_bitwise_operator=16
org.eclipse.jdt.core.formatter.alignment_for_compact_if=16
org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=80
org.eclipse.jdt.core.formatter.alignment_for_enum_constants=0
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=16
org.eclipse.jdt.core.formatter.alignment_for_logical_operator=16
org.eclipse.jdt.core.formatter.alignment_for_method_declaration=0
org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16
org.eclipse.jdt.core.formatter.alignment_for_multiplicative_operator=16
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_resources_in_try=80
org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=16
org.eclipse.jdt.core.formatter.alignment_for_string_concatenation=16
org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=16
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=16
......@@ -123,11 +127,12 @@ org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert
org.eclipse.jdt.core.formatter.insert_space_after_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert
......@@ -157,6 +162,8 @@ org.eclipse.jdt.core.formatter.insert_space_after_comma_in_superinterfaces=inser
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert
org.eclipse.jdt.core.formatter.insert_space_after_logical_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert
......@@ -181,13 +188,17 @@ org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_try_resources=insert
org.eclipse.jdt.core.formatter.insert_space_after_shift_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert
org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert
......@@ -234,6 +245,8 @@ org.eclipse.jdt.core.formatter.insert_space_before_comma_in_superinterfaces=do n
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_logical_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert
......@@ -270,9 +283,12 @@ org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not inser
org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_try_resources=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_shift_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert
......@@ -298,6 +314,10 @@ org.eclipse.jdt.core.formatter.tabulation.char=space
org.eclipse.jdt.core.formatter.tabulation.size=4
org.eclipse.jdt.core.formatter.use_on_off_tags=false
org.eclipse.jdt.core.formatter.use_tabs_only_for_leading_indentations=true
org.eclipse.jdt.core.formatter.wrap_before_binary_operator=true
org.eclipse.jdt.core.formatter.wrap_before_additive_operator=true
org.eclipse.jdt.core.formatter.wrap_before_bitwise_operator=true
org.eclipse.jdt.core.formatter.wrap_before_logical_operator=true
org.eclipse.jdt.core.formatter.wrap_before_multiplicative_operator=true
org.eclipse.jdt.core.formatter.wrap_before_or_operator_multicatch=true
org.eclipse.jdt.core.formatter.wrap_before_string_concatenation=true
org.eclipse.jdt.core.formatter.wrap_outer_expressions_when_nested=true
......@@ -34,12 +34,12 @@ import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
@Feature(value = "deletion", parent = "expert")
final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
private static final long serialVersionUID = 1L;
private final ConflictTimer timer;
private final Solver<? extends DataStructureFactory> solver;
protected final Solver<? extends DataStructureFactory> solver;
ActivityLCDS(Solver<? extends DataStructureFactory> solver,
public ActivityLCDS(Solver<? extends DataStructureFactory> solver,
ConflictTimer timer) {
this.timer = timer;
this.solver = solver;
......@@ -53,6 +53,7 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
if (c.locked() || c.size() == 2) {
learnedConstrs.set(j++, learnedConstrs.get(i));
} else {
onRemove(c);
c.remove(solver);
solver.slistener.delete(c);
}
......@@ -94,7 +95,11 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
}
\ No newline at end of file
......@@ -68,7 +68,8 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
}
if (solver.isVerbose()) {
solver.out.log(solver.getLogPrefix() + "cleaning " //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " + solver.learnts.size()); //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " //$NON-NLS-1$
+ solver.learnts.size());
// out.flush();
}
solver.learnts.shrinkTo(j);
......@@ -97,7 +98,7 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
// do nothing
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -33,11 +33,12 @@ import org.sat4j.annotations.Feature;
import org.sat4j.specs.Constr;
@Feature(value = "deletion", parent = "expert")
class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
public class Glucose2LCDS<D extends DataStructureFactory>
extends GlucoseLCDS<D> {
private static final long serialVersionUID = 1L;
Glucose2LCDS(Solver<D> solver, ConflictTimer timer) {
protected Glucose2LCDS(Solver<D> solver, ConflictTimer timer) {
super(solver, timer);
}
......@@ -48,9 +49,9 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
}
@Override
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
if (from.getActivity() > 2.0) {
int nblevel = computeLBD(from);
int nblevel = computeLBD(from, propagated);
if (nblevel < from.getActivity()) {
getSolver().stats.incUpdateLBD();
from.setActivity(nblevel);
......@@ -58,4 +59,4 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
}
}
}
\ No newline at end of file
}
......@@ -35,11 +35,11 @@ import org.sat4j.specs.IVec;
/**
* LBD based clauses cleaning strategy, as found in Glucose.
*
*
* This strategy expects the constraints to be clauses, i.e. the LBD computation
* may not be correct for other constraints (cardinality constraints, PB
* constraints).
*
*
* @author leberre
*
* @param <D>
......@@ -49,9 +49,9 @@ class GlucoseLCDS<D extends DataStructureFactory>
implements LearnedConstraintsDeletionStrategy {
/**
*
*
*/
private final Solver<D> solver;
protected final Solver<D> solver;
private static final long serialVersionUID = 1L;
private int[] flags = new int[0];
private int flag = 0;
......@@ -59,7 +59,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
private final ConflictTimer timer;
GlucoseLCDS(Solver<D> solver, ConflictTimer timer) {
protected GlucoseLCDS(Solver<D> solver, ConflictTimer timer) {
this.solver = solver;
this.timer = timer;
}
......@@ -75,6 +75,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
} else {
c.remove(solver);
solver.slistener.delete(c);
onRemove(c);
}
}
if (solver.isVerbose()) {
......@@ -88,6 +89,10 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
public ConflictTimer getTimer() {
return this.timer;
}
......@@ -109,11 +114,11 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onClauseLearning(Constr constr) {
int nblevel = computeLBD(constr);
int nblevel = computeLBD(constr, -1);
constr.setActivity(nblevel);
}
protected int computeLBD(Constr constr) {
protected int computeLBD(Constr constr, int propagated) {
int nblevel = 1;
this.flag++;
int currentLevel;
......@@ -131,11 +136,11 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
}
protected Solver<D> getSolver() {
return solver;
}
}
\ No newline at end of file
}
......@@ -80,6 +80,16 @@ public interface IOrder {
*/
void updateVar(int p);
/**
* To be called when the activity of a literal changed.
*
* @param p
* a literal. The associated variable will be updated.
* @param value
* The value to update the literal with.
*/
void updateVar(int p, double value);
/**
* that method has the responsibility to initialize all arrays in the
* heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
......
......@@ -79,5 +79,5 @@ public interface LearnedConstraintsDeletionStrategy extends Serializable {
*
* @param from
*/
void onPropagation(Constr from);
void onPropagation(Constr from, int propagated);
}
\ No newline at end of file
......@@ -96,7 +96,7 @@ final class SizeLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -575,7 +575,7 @@ public class Solver<D extends DataStructureFactory>
this.voc.setReason(p, from);
this.trail.push(p);
if (from != null && from.learnt()) {
this.learnedConstraintsDeletionStrategy.onPropagation(from);
this.learnedConstraintsDeletionStrategy.onPropagation(from, p);
}
return true;
}
......@@ -1074,6 +1074,10 @@ public class Solver<D extends DataStructureFactory>
this.order.updateVar(p);
}
public void varBumpActivity(Constr constr, int i, int p) {
this.order.updateVar(constr.get(i));
}
private void claRescalActivity() {
for (int i = 0; i < this.learnts.size(); i++) {
this.learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
......@@ -1694,7 +1698,7 @@ public class Solver<D extends DataStructureFactory>
return this.aTimer;
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// TODO Auto-generated method stub
}
......@@ -2595,4 +2599,9 @@ public class Solver<D extends DataStructureFactory>
public void setUnitClauseConsumer(UnitClauseConsumer ucc) {
this.unitClauseConsumer = ucc;
}
@Override
public void postBumpActivity(Constr constr) {
// Nothing to do by default.
}
}
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
/**
* Interface providing the capability to increase the activity of a given
* variable.
......@@ -47,4 +49,12 @@ public interface VarActivityListener extends Serializable {
* <code>v&lt;&lt;1^1</code>)
*/
void varBumpActivity(int p);
/**
* Update the activity of a variable v.
*/
void varBumpActivity(Constr constr, int i, int p);
void postBumpActivity(Constr constr);
}
......@@ -81,6 +81,11 @@ public class NaturalStaticOrder implements IOrder {
public void updateVar(int p) {
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
@Override
public void init() {
index = 1;
......
......@@ -69,6 +69,11 @@ public class OrientedOrder implements IOrder {
}
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
@Override
public void init() {
order.init();
......
......@@ -130,6 +130,11 @@ public class RandomWalkDecorator implements IOrder, Serializable {
this.decorated.updateVar(q);
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
public double varActivity(int q) {
return this.decorated.varActivity(q);
}
......
......@@ -127,6 +127,11 @@ public class TabuListDecorator implements IOrder {
this.decorated.updateVar(q);
}
@Override
public void updateVar(int p, double value) {
updateVar(p);
}
public double varActivity(int q) {
return this.decorated.varActivity(q);
}
......
......@@ -150,16 +150,21 @@ public class VarOrderHeap implements IOrder, Serializable {
* a literal
*/
public void updateVar(int p) {
updateVar(p, 1);
}
@Override
public void updateVar(int p, double value) {
int var = var(p);
updateActivity(var);
updateActivity(var, value);
this.phaseStrategy.updateVar(p);
if (this.heap.inHeap(var)) {
this.heap.increase(var);
}
}
protected void updateActivity(final int var) {
if ((this.activity[var] += this.varInc) > VAR_RESCALE_BOUND) {
protected void updateActivity(final int var, double inc) {
if ((this.activity[var] += (inc * varInc)) > VAR_RESCALE_BOUND) {
varRescaleActivity();
}
}
......
......@@ -149,4 +149,9 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
/*******************************************************************************
* 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;
import java.util.Map;
import java.util.TreeMap;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.specs.IVecInt;
/**
*
*
* @author Romain WALLON
*
* @version 0.1.0
*/
public class ConflictMapMinimizeWeakening extends ConflictMap {
private final Map<BigInteger, IVecInt> map = new TreeMap<BigInteger, IVecInt>();
public ConflictMapMinimizeWeakening(PBConstr cpb, int level,
boolean noRemove, SkipStrategy skip, IPreProcess preprocess,
IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, preprocess, postProcessing,
weakeningStrategy, autoDivisionStrategy, stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, SkipStrategy skip, IPreProcess preprocess,
IPostProcess postProcessing, IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy, PBSolverStats stats) {
return new ConflictMapMinimizeWeakening(cpb, level, noRemove, skip,
preprocess, postProcessing, weakeningStrategy,
autoDivisionStrategy, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, SkipStrategy skip, IPreProcess preprocess,
IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy,
AutoDivisionStrategy autoDivisionStrategy,