diff --git a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java index 3f4346d0..a19b106e 100644 --- a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java +++ b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java @@ -5,15 +5,10 @@ package com.booleworks.logicng.datastructures.encodingresult; import com.booleworks.logicng.collections.LngVector; -import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.InternalAuxVarType; import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; -import com.booleworks.logicng.propositions.Proposition; -import com.booleworks.logicng.solvers.sat.LngCoreSolver; - -import java.util.List; /** * The result of an encoding. @@ -87,34 +82,4 @@ default Variable newCnfVariable() { * @return the {@link FormulaFactory} */ FormulaFactory getFactory(); - - /** - * Returns the result. The result might not be complete if the encoding - * result materialize its input as formulas on the formula factory only - * partially. E.g. the encoding result for a SAT Solver does not materialize - * any formulas. - * @return the result - */ - List getResult(); - - /** - * Constructs a new result which stores the result in a formula. - * @param f the formula factory - * @return the result - */ - static EncodingResultFF forFormulaFactory(final FormulaFactory f) { - return new EncodingResultFF(f); - } - - /** - * Constructs a new result which adds the result directly to a given solver. - * @param solver the solver - * @param proposition the original proposition of the cardinality constraint - * @return the result - */ - static EncodingResultSolver forSatSolver(final FormulaFactory f, final LngCoreSolver solver, - final Proposition proposition) { - return new EncodingResultSolver(f, solver, proposition); - } - } diff --git a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java index 881f8f94..fb840dd1 100644 --- a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java +++ b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java @@ -23,7 +23,7 @@ public final class EncodingResultFF implements EncodingResult { * {@link FormulaFactory}. * @param f the formula factory */ - EncodingResultFF(final FormulaFactory f) { + public EncodingResultFF(final FormulaFactory f) { this.f = f; result = new ArrayList<>(); } @@ -47,7 +47,6 @@ public Variable newVariable(final String auxType) { return f.newAuxVariable(auxType); } - @Override public List getResult() { return result; } diff --git a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java index 13fe50a0..03f20abb 100644 --- a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java +++ b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java @@ -2,16 +2,12 @@ import com.booleworks.logicng.collections.LngIntVector; import com.booleworks.logicng.collections.LngVector; -import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.propositions.Proposition; import com.booleworks.logicng.solvers.sat.LngCoreSolver; -import java.util.ArrayList; -import java.util.List; - /** * An encoding result that writes the encoding directly to a solver. */ @@ -25,7 +21,7 @@ public final class EncodingResultSolver implements EncodingResult { * @param solver the solver instance * @param proposition the original proposition */ - EncodingResultSolver(final FormulaFactory f, final LngCoreSolver solver, final Proposition proposition) { + public EncodingResultSolver(final FormulaFactory f, final LngCoreSolver solver, final Proposition proposition) { this.f = f; this.solver = solver; this.proposition = proposition; @@ -77,11 +73,6 @@ public FormulaFactory getFactory() { return f; } - @Override - public List getResult() { - return new ArrayList<>(); - } - /** * Returns the original proposition. * @return the original proposition diff --git a/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java b/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java index 71136fa0..78c09b8f 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java @@ -65,7 +65,7 @@ public static List encode(final FormulaFactory f, final CardinalityCons */ public static List encode(final FormulaFactory f, final CardinalityConstraint cc, final EncoderConfig config) { - final EncodingResultFF result = EncodingResult.forFormulaFactory(f); + final EncodingResultFF result = new EncodingResultFF(f); encodeConstraint(cc, result, config); return Collections.unmodifiableList(result.getResult()); } @@ -95,10 +95,10 @@ public static void encode(final CardinalityConstraint cc, final EncodingResult r * @param cc the cardinality constraint * @return the encoding of the constraint and the incremental data */ - public static Pair, CcIncrementalData> encodeIncremental(final FormulaFactory f, - final CardinalityConstraint cc) { - final EncodingResultFF result = EncodingResult.forFormulaFactory(f); - final CcIncrementalData incData = encodeIncremental(cc, result); + public static Pair, CcIncrementalData> encodeIncremental(final FormulaFactory f, + final CardinalityConstraint cc) { + final EncodingResultFF result = new EncodingResultFF(f); + final CcIncrementalData incData = encodeIncremental(cc, result); return new Pair<>(Collections.unmodifiableList(result.getResult()), incData); } @@ -109,10 +109,10 @@ public static Pair, CcIncrementalData> encodeIncremental(final For * @param config the configuration for the encoder * @return the encoding of the constraint and the incremental data */ - public static Pair, CcIncrementalData> + public static Pair, CcIncrementalData> encodeIncremental(final FormulaFactory f, final CardinalityConstraint cc, final EncoderConfig config) { - final EncodingResultFF result = EncodingResult.forFormulaFactory(f); - final CcIncrementalData incData = encodeIncremental(cc, result, config); + final EncodingResultFF result = new EncodingResultFF(f); + final CcIncrementalData incData = encodeIncremental(cc, result, config); return new Pair<>(Collections.unmodifiableList(result.getResult()), incData); } @@ -122,7 +122,8 @@ public static Pair, CcIncrementalData> encodeIncremental(final For * @param result the result of the encoding * @return the incremental data */ - public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, final EncodingResult result) { + public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, + final T result) { return encodeIncrementalConstraint(cc, result, null); } @@ -133,14 +134,14 @@ public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc * @param config the configuration for the encoder * @return the incremental data */ - public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, final EncodingResult result, - final EncoderConfig config) { + public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, + final T result, + final EncoderConfig config) { return encodeIncrementalConstraint(cc, result, config); } - protected static CcIncrementalData encodeIncrementalConstraint(final CardinalityConstraint cc, - final EncodingResult result, - final EncoderConfig initConfig) { + protected static CcIncrementalData encodeIncrementalConstraint( + final CardinalityConstraint cc, final T result, final EncoderConfig initConfig) { final var config = initConfig != null ? initConfig : (EncoderConfig) result.getFactory() .configurationFor(ConfigurationType.ENCODER); @@ -279,8 +280,10 @@ protected static void amk(final EncodingResult result, final EncoderConfig confi } } - protected static CcIncrementalData amkIncremental(final EncodingResult result, final EncoderConfig config, - final Variable[] vars, final int rhs) { + protected static CcIncrementalData amkIncremental(final T result, + final EncoderConfig config, + final Variable[] vars, + final int rhs) { if (rhs < 0) { throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs); } @@ -344,8 +347,10 @@ protected static void alk(final EncodingResult result, final EncoderConfig confi } } - protected static CcIncrementalData alkIncremental(final EncodingResult result, final EncoderConfig config, - final Variable[] vars, final int rhs) { + protected static CcIncrementalData alkIncremental(final T result, + final EncoderConfig config, + final Variable[] vars, + final int rhs) { if (rhs < 0) { throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs); } diff --git a/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java b/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java index f2f6457b..37b194cb 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java @@ -28,12 +28,9 @@ import com.booleworks.logicng.collections.LngVector; import com.booleworks.logicng.datastructures.encodingresult.EncodingResult; -import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; -import java.util.List; - /** * Incremental data for an at-most-k cardinality constraint. When an at-most-k * cardinality constraint is constructed, it is possible to save incremental @@ -42,8 +39,8 @@ * @version 3.0.0 * @since 1.1 */ -public final class CcIncrementalData { - private final EncodingResult result; +public final class CcIncrementalData { + private final T result; private final EncoderConfig.AmkEncoder amkEncoder; private final EncoderConfig.AlkEncoder alkEncoder; private final LngVector vector1; @@ -62,7 +59,7 @@ public final class CcIncrementalData { * @param vector2 the second internal vector * @param mod the modulo value */ - public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEncoder amkEncoder, final int rhs, + public CcIncrementalData(final T result, final EncoderConfig.AmkEncoder amkEncoder, final int rhs, final LngVector vector1, final LngVector vector2, final int mod) { this.result = result; @@ -82,7 +79,7 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEnc * @param rhs the current right-hand-side * @param vector1 the first internal vector */ - public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEncoder encoder, final int rhs, + public CcIncrementalData(final T result, final EncoderConfig.AmkEncoder encoder, final int rhs, final LngVector vector1) { this(result, encoder, rhs, vector1, null, -1); } @@ -98,7 +95,7 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEnc * @param vector2 the second internal vector * @param mod the modulo value */ - public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs, + public CcIncrementalData(final T result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs, final int nVars, final LngVector vector1, final LngVector vector2, final int mod) { @@ -122,20 +119,17 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEnc * @param nVars the number of variables * @param vector1 the first internal vector */ - public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs, + public CcIncrementalData(final T result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs, final int nVars, final LngVector vector1) { this(result, alkEncoder, rhs, nVars, vector1, null, -1); } /** - * Tightens the upper bound of an at-most-k constraint and returns the - * resulting formula. + * Tightens the upper bound of an at-most-k constraint. * @param rhs the new upperBound - * @return the incremental encoding of the new upper bound */ - public List newUpperBound(final int rhs) { + public void newUpperBound(final int rhs) { computeUbConstraint(result, rhs); - return result.getResult(); } /** @@ -201,14 +195,11 @@ private void computeUbConstraint(final EncodingResult result, final int rhs) { } /** - * Tightens the lower bound of an at-least-k constraint and returns the - * resulting formula. + * Tightens the lower bound of an at-least-k constraint. * @param rhs the new upperBound - * @return the incremental encoding of the new lower bound */ - public List newLowerBound(final int rhs) { + public void newLowerBound(final int rhs) { computeLbConstraint(result, rhs); - return result.getResult(); } /** @@ -283,6 +274,14 @@ public int getCurrentRhs() { return currentRhs; } + /** + * Returns the {@link EncodingResult} that is used as the target for the encodings. + * @return the {@link EncodingResult} that is used as the target for the encodings + */ + public T getEncodingResult() { + return result; + } + @Override public String toString() { return "CcIncrementalData{" + diff --git a/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java b/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java index b7471aaa..368752ca 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java @@ -39,7 +39,7 @@ private PbEncoder() { * @return the CNF encoding of the pseudo-Boolean constraint */ public static List encode(final FormulaFactory f, final PbConstraint constraint) { - final EncodingResultFF result = EncodingResult.forFormulaFactory(f); + final EncodingResultFF result = new EncodingResultFF(f); encode(constraint, result, null); return Collections.unmodifiableList(result.getResult()); } @@ -62,7 +62,7 @@ public static void encode(final PbConstraint constraint, final EncodingResult re */ public static List encode(final FormulaFactory f, final PbConstraint constraint, final EncoderConfig config) { - final EncodingResult result = EncodingResult.forFormulaFactory(f); + final EncodingResultFF result = new EncodingResultFF(f); encode(constraint, result, config); return Collections.unmodifiableList(result.getResult()); } diff --git a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java index c23c0200..b5d727a4 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java @@ -65,8 +65,9 @@ public static void amk(final EncodingResult result, final Variable[] vars, final } } - public static CcIncrementalData amkForIncremental(final EncodingResult result, final Variable[] vars, - final int rhs) { + public static CcIncrementalData amkForIncremental(final T result, + final Variable[] vars, + final int rhs) { final FormulaFactory f = result.getFactory(); final LngVector input = new LngVector<>(); final LngVector output = new LngVector<>(); @@ -76,7 +77,7 @@ public static CcIncrementalData amkForIncremental(final EncodingResult result, f CcSorting.sort(f, rhs + 1, input, result, output, CcSorting.ImplicationDirection.INPUT_TO_OUTPUT); assert output.size() > rhs; result.addClause(output.get(rhs).negate(f)); - return new CcIncrementalData(result, EncoderConfig.AmkEncoder.CARDINALITY_NETWORK, rhs, output); + return new CcIncrementalData<>(result, EncoderConfig.AmkEncoder.CARDINALITY_NETWORK, rhs, output); } public static void alk(final EncodingResult result, final Variable[] vars, final int rhs) { @@ -103,8 +104,9 @@ public static void alk(final EncodingResult result, final Variable[] vars, final } } - public static CcIncrementalData alkForIncremental(final EncodingResult result, final Variable[] vars, - final int rhs) { + public static CcIncrementalData alkForIncremental(final T result, + final Variable[] vars, + final int rhs) { final FormulaFactory f = result.getFactory(); final LngVector input = new LngVector<>(); final LngVector output = new LngVector<>(); @@ -115,7 +117,7 @@ public static CcIncrementalData alkForIncremental(final EncodingResult result, f CcSorting.sort(f, newRhs + 1, input, result, output, CcSorting.ImplicationDirection.INPUT_TO_OUTPUT); assert output.size() > newRhs; result.addClause(output.get(newRhs).negate(f)); - return new CcIncrementalData(result, EncoderConfig.AlkEncoder.CARDINALITY_NETWORK, rhs, vars.length, output); + return new CcIncrementalData<>(result, EncoderConfig.AlkEncoder.CARDINALITY_NETWORK, rhs, vars.length, output); } public static void exk(final EncodingResult result, final Variable[] vars, final int rhs) { diff --git a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcModularTotalizer.java b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcModularTotalizer.java index b1d48e25..a1a3cdce 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcModularTotalizer.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcModularTotalizer.java @@ -48,7 +48,8 @@ private CcModularTotalizer() { * @param rhs the right-hand side of the constraint * @return the incremental data for this constraint */ - public static CcIncrementalData amk(final EncodingResult result, final Variable[] vars, final int rhs) { + public static CcIncrementalData amk(final T result, final Variable[] vars, + final int rhs) { final var state = new State(result.getFactory()); final int mod = initialize(result, rhs, vars.length, state); for (final Variable var : vars) { @@ -58,7 +59,7 @@ public static CcIncrementalData amk(final EncodingResult result, final Variable[ assert state.inlits.isEmpty(); encodeOutput(result, rhs, mod, state); state.currentCardinalityRhs = rhs + 1; - return new CcIncrementalData(result, EncoderConfig.AmkEncoder.MODULAR_TOTALIZER, rhs, + return new CcIncrementalData<>(result, EncoderConfig.AmkEncoder.MODULAR_TOTALIZER, rhs, state.cardinalityUpOutvars, state.cardinalityLwOutvars, mod); } @@ -70,7 +71,8 @@ public static CcIncrementalData amk(final EncodingResult result, final Variable[ * @param rhs the right-hand side of the constraint * @return the incremental data for this constraint */ - public static CcIncrementalData alk(final EncodingResult result, final Variable[] vars, final int rhs) { + public static CcIncrementalData alk(final T result, final Variable[] vars, + final int rhs) { final var state = new State(result.getFactory()); final int newRhs = vars.length - rhs; final int mod = initialize(result, newRhs, vars.length, state); @@ -81,7 +83,7 @@ public static CcIncrementalData alk(final EncodingResult result, final Variable[ assert state.inlits.isEmpty(); encodeOutput(result, newRhs, mod, state); state.currentCardinalityRhs = newRhs + 1; - return new CcIncrementalData(result, EncoderConfig.AlkEncoder.MODULAR_TOTALIZER, rhs, vars.length, + return new CcIncrementalData<>(result, EncoderConfig.AlkEncoder.MODULAR_TOTALIZER, rhs, vars.length, state.cardinalityUpOutvars, state.cardinalityLwOutvars, mod); } diff --git a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcTotalizer.java b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcTotalizer.java index f5e17b04..2ef31df6 100644 --- a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcTotalizer.java +++ b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcTotalizer.java @@ -55,14 +55,15 @@ private CcTotalizer() { * @throws IllegalArgumentException if the right-hand side of the constraint * was negative */ - public static CcIncrementalData amk(final EncodingResult result, final Variable[] vars, final int rhs) { + public static CcIncrementalData amk(final T result, final Variable[] vars, + final int rhs) { final TotalizerVars tv = initializeConstraint(result, vars); toCnf(result, tv, rhs, Bound.UPPER); assert tv.invars.isEmpty(); for (int i = rhs; i < tv.outvars.size(); i++) { result.addClause(tv.outvars.get(i).negate(result.getFactory())); } - return new CcIncrementalData(result, EncoderConfig.AmkEncoder.TOTALIZER, rhs, tv.outvars); + return new CcIncrementalData<>(result, EncoderConfig.AmkEncoder.TOTALIZER, rhs, tv.outvars); } /** @@ -74,14 +75,15 @@ public static CcIncrementalData amk(final EncodingResult result, final Variable[ * @throws IllegalArgumentException if the right-hand side of the constraint * was negative */ - public static CcIncrementalData alk(final EncodingResult result, final Variable[] vars, final int rhs) { + public static CcIncrementalData alk(final T result, + final Variable[] vars, final int rhs) { final TotalizerVars tv = initializeConstraint(result, vars); toCnf(result, tv, rhs, Bound.LOWER); assert tv.invars.isEmpty(); for (int i = 0; i < rhs; i++) { result.addClause(tv.outvars.get(i)); } - return new CcIncrementalData(result, EncoderConfig.AlkEncoder.TOTALIZER, rhs, vars.length, tv.outvars); + return new CcIncrementalData<>(result, EncoderConfig.AlkEncoder.TOTALIZER, rhs, vars.length, tv.outvars); } /** diff --git a/core/src/main/java/com/booleworks/logicng/solvers/SatSolver.java b/core/src/main/java/com/booleworks/logicng/solvers/SatSolver.java index 42b0f937..80478b05 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/SatSolver.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/SatSolver.java @@ -9,7 +9,7 @@ import com.booleworks.logicng.collections.LngIntVector; import com.booleworks.logicng.configurations.ConfigurationType; import com.booleworks.logicng.datastructures.Model; -import com.booleworks.logicng.datastructures.encodingresult.EncodingResult; +import com.booleworks.logicng.datastructures.encodingresult.EncodingResultSolver; import com.booleworks.logicng.encodings.CcEncoder; import com.booleworks.logicng.encodings.CcIncrementalData; import com.booleworks.logicng.encodings.PbEncoder; @@ -130,14 +130,14 @@ public void add(final Formula formula, final Proposition proposition) { proposition); } else { CcEncoder.encode((CardinalityConstraint) constraint, - EncodingResult.forSatSolver(f, solver, proposition)); + new EncodingResultSolver(f, solver, proposition)); } } else { CcEncoder.encode((CardinalityConstraint) constraint, - EncodingResult.forSatSolver(f, solver, proposition)); + new EncodingResultSolver(f, solver, proposition)); } } else { - PbEncoder.encode(constraint, EncodingResult.forSatSolver(f, solver, proposition)); + PbEncoder.encode(constraint, new EncodingResultSolver(f, solver, proposition)); } } else { addFormulaAsCnf(formula, proposition); @@ -227,8 +227,8 @@ public void addWithRelaxation(final Variable relaxationVar, final Collection addIncrementalCc(final CardinalityConstraint cc) { + final EncodingResultSolver result = new EncodingResultSolver(f, solver, null); return CcEncoder.encodeIncremental(cc, result); } diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java index 82cc4820..94661cab 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java @@ -7,6 +7,7 @@ import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.OPTIMIZATION_FUNCTION_STARTED; import com.booleworks.logicng.datastructures.Model; +import com.booleworks.logicng.datastructures.encodingresult.EncodingResultSolver; import com.booleworks.logicng.encodings.CcIncrementalData; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; @@ -149,7 +150,8 @@ private LngResult maximize( } final Formula cc = f.cc(CType.GE, currentBound + 1, selectors); assert cc instanceof CardinalityConstraint; - final CcIncrementalData incrementalData = solver.addIncrementalCc((CardinalityConstraint) cc); + final CcIncrementalData incrementalData = + solver.addIncrementalCc((CardinalityConstraint) cc); while (true) { try (final SatCall satCall = solver.satCall().handler(handler).solve()) { final LngResult satResult = satCall.getSatResult(); @@ -159,7 +161,8 @@ private LngResult maximize( return LngResult.of(lastResultModel); } lastResultModel = satCall.model(resultModelVariables); - final OptimizationFoundBetterBoundEvent betterBoundEvent = new OptimizationFoundBetterBoundEvent(() -> satCall.model(resultModelVariables)); + final OptimizationFoundBetterBoundEvent betterBoundEvent = + new OptimizationFoundBetterBoundEvent(() -> satCall.model(resultModelVariables)); if (!handler.shouldResume(betterBoundEvent)) { return LngResult.partial(lastResultModel, betterBoundEvent); } diff --git a/core/src/main/java/com/booleworks/logicng/transformations/PureExpansionTransformation.java b/core/src/main/java/com/booleworks/logicng/transformations/PureExpansionTransformation.java index 8c45a41c..67defb7b 100644 --- a/core/src/main/java/com/booleworks/logicng/transformations/PureExpansionTransformation.java +++ b/core/src/main/java/com/booleworks/logicng/transformations/PureExpansionTransformation.java @@ -4,7 +4,6 @@ package com.booleworks.logicng.transformations; -import com.booleworks.logicng.datastructures.encodingresult.EncodingResult; import com.booleworks.logicng.datastructures.encodingresult.EncodingResultFF; import com.booleworks.logicng.encodings.cc.CcAmo; import com.booleworks.logicng.formulas.BinaryOperator; @@ -68,7 +67,7 @@ private Formula expand(final Formula formula) { case PBC: final PbConstraint pbc = (PbConstraint) formula; if (pbc.isAmo() || pbc.isExo()) { - final EncodingResultFF encodingResult = EncodingResult.forFormulaFactory(f); + final EncodingResultFF encodingResult = new EncodingResultFF(f); final Variable[] vars = FormulaHelper.literalsAsVariables(pbc.getOperands()); CcAmo.pure(encodingResult, vars); final List encoding = encodingResult.getResult(); diff --git a/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalFormulaTest.java b/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalFormulaTest.java index 0140ad65..856e2e38 100644 --- a/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalFormulaTest.java +++ b/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalFormulaTest.java @@ -9,6 +9,7 @@ import com.booleworks.logicng.LogicNGTest; import com.booleworks.logicng.LongRunningTag; +import com.booleworks.logicng.datastructures.encodingresult.EncodingResultFF; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; import com.booleworks.logicng.formulas.Formula; @@ -48,9 +49,9 @@ public void testSimpleIncrementalAMK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.LE, 9, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); final SatSolver solver = SatSolver.newSolver(f); solver.add(CcEncoder.encode(f, (CardinalityConstraint) f.cc(CType.GE, 4, vars), config)); // >= @@ -61,25 +62,32 @@ public void testSimpleIncrementalAMK() { solver.add(cc.getFirst()); assertSolverSat(solver); assertSolverSat(solver); // <= 9 - solver.add(incData.newUpperBound(8)); // <= 8 + incData.newUpperBound(8); + solver.add(incData.getEncodingResult().getResult()); // <= 8 assertSolverSat(solver); assertThat(incData.getCurrentRhs()).isEqualTo(8); - solver.add(incData.newUpperBound(7)); // <= 7 + incData.newUpperBound(7); + solver.add(incData.getEncodingResult().getResult()); // <= 7 assertSolverSat(solver); - solver.add(incData.newUpperBound(6)); // <= 6 + incData.newUpperBound(6); + solver.add(incData.getEncodingResult().getResult()); // <= 6 assertSolverSat(solver); - solver.add(incData.newUpperBound(5)); // <= 5 + incData.newUpperBound(5); + solver.add(incData.getEncodingResult().getResult()); // <= 5 assertSolverSat(solver); - solver.add(incData.newUpperBound(4)); // <= 4 + incData.newUpperBound(4); + solver.add(incData.getEncodingResult().getResult()); // <= 4 assertSolverSat(solver); final SolverState state = solver.saveState(); - solver.add(incData.newUpperBound(3)); // <= 3 + incData.newUpperBound(3); + solver.add(incData.getEncodingResult().getResult()); // <= 3 assertSolverUnsat(solver); solver.loadState(state); assertSolverSat(solver); - solver.add(incData.newUpperBound(2)); // <= 2 + incData.newUpperBound(2); + solver.add(incData.getEncodingResult().getResult()); // <= 2 assertSolverUnsat(solver); } } @@ -92,9 +100,9 @@ public void testIncrementalData() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - Pair, CcIncrementalData> cc = + Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.LT, 10, vars), config); - CcIncrementalData incData = cc.getSecond(); + CcIncrementalData incData = cc.getSecond(); assertThat(incData.toString()).contains("currentRhs=9"); cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.GT, 1, vars), config); @@ -136,9 +144,9 @@ public void testSimpleIncrementalALK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.GE, 2, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); final SatSolver solver = SatSolver.newSolver(f); // >= 4 @@ -148,23 +156,30 @@ public void testSimpleIncrementalALK() { solver.add(cc.getFirst()); assertSolverSat(solver); // >= 2 - solver.add(incData.newLowerBound(3)); // >= 3 + incData.newLowerBound(3); + solver.add(incData.getEncodingResult().getResult()); // >= 3 assertSolverSat(solver); - solver.add(incData.newLowerBound(4)); // >= 4 + incData.newLowerBound(4); + solver.add(incData.getEncodingResult().getResult()); // >= 4 assertSolverSat(solver); - solver.add(incData.newLowerBound(5)); // >= 5 + incData.newLowerBound(5); + solver.add(incData.getEncodingResult().getResult()); // >= 5 assertSolverSat(solver); - solver.add(incData.newLowerBound(6)); // >= 6 + incData.newLowerBound(6); + solver.add(incData.getEncodingResult().getResult()); // >= 6 assertSolverSat(solver); - solver.add(incData.newLowerBound(7)); // >= 7 + incData.newLowerBound(7); + solver.add(incData.getEncodingResult().getResult()); // >= 7 assertSolverSat(solver); final SolverState state = solver.saveState(); - solver.add(incData.newLowerBound(8)); // >= 8 + incData.newLowerBound(8); + solver.add(incData.getEncodingResult().getResult()); // >= 8 assertSolverUnsat(solver); solver.loadState(state); assertSolverSat(solver); - solver.add(incData.newLowerBound(9)); // <= 9 + incData.newLowerBound(9); + solver.add(incData.getEncodingResult().getResult()); // <= 9 assertSolverUnsat(solver); } } @@ -179,9 +194,9 @@ public void testLargeTotalizerUpperBoundAMK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.LE, currentBound, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); // >= 42 solver.add(CcEncoder.encode(f, (CardinalityConstraint) f.cc(CType.GE, 42, vars), config)); @@ -190,7 +205,8 @@ public void testLargeTotalizerUpperBoundAMK() { // search the lower bound while (solver.sat()) { // <= currentBound - 1 - solver.add(incData.newUpperBound(--currentBound)); + incData.newUpperBound(--currentBound); + solver.add(incData.getEncodingResult().getResult()); } assertThat(currentBound).isEqualTo(41); } @@ -206,9 +222,9 @@ public void testLargeTotalizerLowerBoundALK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.GE, currentBound, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); // <= 42 solver.add(CcEncoder.encode(f, (CardinalityConstraint) f.cc(CType.LE, 87, vars), config)); @@ -217,7 +233,8 @@ public void testLargeTotalizerLowerBoundALK() { // search the lower bound while (solver.sat()) { // <= currentBound + 1 - solver.add(incData.newLowerBound(++currentBound)); + incData.newLowerBound(++currentBound); + solver.add(incData.getEncodingResult().getResult()); } assertThat(currentBound).isEqualTo(88); } @@ -234,10 +251,10 @@ public void testLargeModularTotalizerAMK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.LE, currentBound, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); // >= 42 solver.add(CcEncoder.encode(f, (CardinalityConstraint) f.cc(CType.GE, 42, vars), config)); @@ -246,7 +263,8 @@ public void testLargeModularTotalizerAMK() { // search the lower bound while (solver.sat()) { // <= currentBound - 1 - solver.add(incData.newUpperBound(--currentBound)); + incData.newUpperBound(--currentBound); + solver.add(incData.getEncodingResult().getResult()); } assertThat(currentBound).isEqualTo(41); } @@ -263,16 +281,17 @@ public void testVeryLargeModularTotalizerAMK() { for (int i = 0; i < numLits; i++) { vars[i] = f.variable("v" + i); } - final Pair, CcIncrementalData> cc = + final Pair, CcIncrementalData> cc = CcEncoder.encodeIncremental(f, (CardinalityConstraint) f.cc(CType.LE, currentBound, vars), config); - final CcIncrementalData incData = cc.getSecond(); + final CcIncrementalData incData = cc.getSecond(); solver.add(CcEncoder.encode(f, (CardinalityConstraint) f.cc(CType.GE, 234, vars), config)); solver.add(cc.getFirst()); // search the lower bound while (solver.sat()) { - solver.add(incData.newUpperBound(--currentBound)); + incData.newUpperBound(--currentBound); + solver.add(incData.getEncodingResult().getResult()); } assertThat(currentBound).isEqualTo(233); } diff --git a/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalSolverTest.java b/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalSolverTest.java index df073a5e..70c528e3 100644 --- a/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalSolverTest.java +++ b/core/src/test/java/com/booleworks/logicng/encodings/CcIncrementalSolverTest.java @@ -8,6 +8,7 @@ import com.booleworks.logicng.LogicNGTest; import com.booleworks.logicng.LongRunningTag; +import com.booleworks.logicng.datastructures.encodingresult.EncodingResultSolver; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; import com.booleworks.logicng.formulas.FormulaFactory; @@ -54,7 +55,8 @@ public void testSimpleIncrementalAMK() { f.putConfiguration(config); - final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.LE, 9, vars)); + final CcIncrementalData incData = + solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.LE, 9, vars)); assertSolverSat(solver); // <= 9 incData.newUpperBoundForSolver(8); // <= 8 assertSolverSat(solver); @@ -95,7 +97,7 @@ public void testSimpleIncrementalALK() { f.putConfiguration(config); - final CcIncrementalData incData = + final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.GE, 2, vars)); assertSolverSat(solver); // >=2 incData.newLowerBoundForSolver(3); // >= 3 @@ -133,7 +135,7 @@ public void testLargeTotalizerUpperBoundAMK() { for (final SatSolver solver : solvers) { solver.add(f.cc(CType.GE, 42, vars)); // >= 42 f.putConfiguration(configs[0]); - final CcIncrementalData incData = + final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.LE, currentBound, vars)); // search the lower bound while (solver.sat()) { @@ -157,7 +159,7 @@ public void testLargeTotalizerLowerBoundALK() { } solver.add(f.cc(CType.LE, 87, vars)); f.putConfiguration(configs[0]); - final CcIncrementalData incData = + final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.GE, currentBound, vars)); // search the lower bound while (solver.sat()) { @@ -178,7 +180,7 @@ public void testLargeModularTotalizerAMK() { vars[i] = f.variable("v" + i); } solver.add(f.cc(CType.GE, 42, vars)); // >= 42 - final CcIncrementalData incData = + final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.LE, currentBound, vars)); // search the lower bound while (solver.sat()) { @@ -202,7 +204,7 @@ public void testVeryLargeModularTotalizerAMK() { vars[i] = f.variable("v" + i); } solver.add(f.cc(CType.GE, 234, vars)); - final CcIncrementalData incData = + final CcIncrementalData incData = solver.addIncrementalCc((CardinalityConstraint) f.cc(CType.LE, currentBound, vars)); // search the lower bound while (solver.sat()) {