From 614421523655cd80b95c7cb9c67df1a767b2767c Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 3 Jan 2022 18:57:09 +0100 Subject: [PATCH] [CP-SAT] add BoolVar class to the java modelling layer --- .../java/com/google/ortools/sat/BoolVar.java | 51 +++++++++++++ ...{Constant.java => ConstantExpression.java} | 4 +- .../java/com/google/ortools/sat/CpModel.java | 60 ++++++++------- .../java/com/google/ortools/sat/IntVar.java | 56 ++++++-------- .../com/google/ortools/sat/LinearExpr.java | 33 ++++++--- .../google/ortools/sat/LinearExprBuilder.java | 74 ++++++++++--------- .../java/com/google/ortools/sat/Literal.java | 8 +- .../ortools/sat/NotBooleanVariable.java | 41 +++++++++- ...SumOfVariables.java => SumExpression.java} | 4 +- ...alProd.java => WeightedSumExpression.java} | 6 +- ortools/sat/doc/README.md | 2 + ortools/sat/doc/boolean_logic.md | 22 +++--- ortools/sat/doc/channeling.md | 8 +- ortools/sat/doc/integer_arithmetic.md | 2 + ortools/sat/doc/model.md | 4 +- ortools/sat/doc/scheduling.md | 14 ++-- ortools/sat/doc/solver.md | 4 +- ortools/sat/samples/BinPackingProblemSat.java | 3 +- ortools/sat/samples/BoolOrSampleSat.java | 6 +- ortools/sat/samples/ChannelingSampleSat.java | 3 +- ortools/sat/samples/CpIsFunSat.java | 2 +- ortools/sat/samples/CpSatExample.java | 8 +- ortools/sat/samples/LiteralSampleSat.java | 4 +- ortools/sat/samples/RankingSampleSat.java | 12 +-- ortools/sat/samples/ReifiedSampleSat.java | 8 +- .../sat/samples/SolutionHintingSampleSat.java | 2 +- ...ndPrintIntermediateSolutionsSampleSat.java | 2 +- 27 files changed, 286 insertions(+), 157 deletions(-) create mode 100644 ortools/java/com/google/ortools/sat/BoolVar.java rename ortools/java/com/google/ortools/sat/{Constant.java => ConstantExpression.java} (91%) rename ortools/java/com/google/ortools/sat/{SumOfVariables.java => SumExpression.java} (91%) rename ortools/java/com/google/ortools/sat/{ScalProd.java => WeightedSumExpression.java} (89%) diff --git a/ortools/java/com/google/ortools/sat/BoolVar.java b/ortools/java/com/google/ortools/sat/BoolVar.java new file mode 100644 index 0000000000..3f45b1f00f --- /dev/null +++ b/ortools/java/com/google/ortools/sat/BoolVar.java @@ -0,0 +1,51 @@ +// Copyright 2010-2021 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package com.google.ortools.sat; + +import com.google.ortools.sat.CpModelProto; +import com.google.ortools.util.Domain; + +/** An Boolean variable. */ +public final class BoolVar extends IntVar implements Literal { + BoolVar(CpModelProto.Builder builder, Domain domain, String name) { + super(builder, domain, name); + this.negation_ = null; + } + + BoolVar(CpModelProto.Builder builder, int index) { + super(builder, index); + this.negation_ = null; + } + + /** Returns the negation of a boolean variable. */ + @Override + public Literal not() { + if (negation_ == null) { + negation_ = new NotBooleanVariable(this); + } + return negation_; + } + + @Override + public BoolVar getBoolVar() { + return this; + } + + @Override + public boolean negated() { + return false; + } + + private NotBooleanVariable negation_ = null; +} diff --git a/ortools/java/com/google/ortools/sat/Constant.java b/ortools/java/com/google/ortools/sat/ConstantExpression.java similarity index 91% rename from ortools/java/com/google/ortools/sat/Constant.java rename to ortools/java/com/google/ortools/sat/ConstantExpression.java index 1f5ebffc54..05c70d15b0 100644 --- a/ortools/java/com/google/ortools/sat/Constant.java +++ b/ortools/java/com/google/ortools/sat/ConstantExpression.java @@ -14,10 +14,10 @@ package com.google.ortools.sat; /** A specialized constant linear expression. */ -public final class Constant implements LinearExpr { +public final class ConstantExpression implements LinearExpr { private final long offset; - public Constant(long offset) { + public ConstantExpression(long offset) { this.offset = offset; } diff --git a/ortools/java/com/google/ortools/sat/CpModel.java b/ortools/java/com/google/ortools/sat/CpModel.java index b4d8a8414d..a4aa8e42ad 100644 --- a/ortools/java/com/google/ortools/sat/CpModel.java +++ b/ortools/java/com/google/ortools/sat/CpModel.java @@ -85,28 +85,38 @@ public final class CpModel { } /** Creates a Boolean variable with the given name. */ - public IntVar newBoolVar(String name) { - return new IntVar(modelBuilder, new Domain(0, 1), name); + public BoolVar newBoolVar(String name) { + return new BoolVar(modelBuilder, new Domain(0, 1), name); } /** Creates a constant variable. */ public IntVar newConstant(long value) { if (constantMap.containsKey(value)) { - return constantMap.get(value); + return new IntVar(modelBuilder, constantMap.get(value)); } IntVar cste = new IntVar(modelBuilder, new Domain(value), ""); // bounds and name. - constantMap.put(value, cste); + constantMap.put(value, cste.getIndex()); return cste; } /** Returns the true literal. */ public Literal trueLiteral() { - return newConstant(1); + if (constantMap.containsKey(1L)) { + return new BoolVar(modelBuilder, constantMap.get(1L)); + } + BoolVar cste = new BoolVar(modelBuilder, new Domain(1), ""); // bounds and name. + constantMap.put(1L, cste.getIndex()); + return cste; } /** Returns the false literal. */ public Literal falseLiteral() { - return newConstant(0); + if (constantMap.containsKey(0L)) { + return new BoolVar(modelBuilder, constantMap.get(0L)); + } + BoolVar cste = new BoolVar(modelBuilder, new Domain(0), ""); // bounds and name. + constantMap.put(0L, cste.getIndex()); + return cste; } // Boolean Constraints. @@ -268,8 +278,8 @@ public final class CpModel { /** Adds {@code left == right}. */ public Constraint addEquality(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), new Domain(0)); } @@ -281,8 +291,8 @@ public final class CpModel { /** Adds {@code left <= right}. */ public Constraint addLessOrEqual(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, 0)); } @@ -294,8 +304,8 @@ public final class CpModel { /** Adds {@code left < right}. */ public Constraint addLessThan(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, -1)); } @@ -307,8 +317,8 @@ public final class CpModel { /** Adds {@code left >= right}. */ public Constraint addGreaterOrEqual(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), new Domain(0, Long.MAX_VALUE)); } @@ -320,8 +330,8 @@ public final class CpModel { /** Adds {@code left > right}. */ public Constraint addGreaterThan(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), new Domain(1, Long.MAX_VALUE)); } @@ -335,8 +345,8 @@ public final class CpModel { /** Adds {@code left != right}. */ public Constraint addDifferent(LinearExpr left, LinearExpr right) { LinearExprBuilder difference = LinearExpr.newBuilder(); - difference.addExpression(left, 1); - difference.addExpression(right, -1); + difference.addTerm(left, 1); + difference.addTerm(right, -1); return addLinearExpressionInDomain(difference.build(), Domain.fromFlatIntervals(new long[] {Long.MIN_VALUE, -1, 1, Long.MAX_VALUE})); } @@ -798,10 +808,7 @@ public final class CpModel { */ public IntervalVar newIntervalVar( LinearExpr start, LinearExpr size, LinearExpr end, String name) { - LinearExprBuilder expr = LinearExpr.newBuilder(); - expr.addExpression(start); - expr.addExpression(size); - addEquality(expr.build(), end); + addEquality(LinearExpr.newBuilder().add(start).add(size).build(), end); return new IntervalVar(modelBuilder, getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false), getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false), @@ -824,7 +831,7 @@ public final class CpModel { getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false), getLinearExpressionProtoBuilderFromLong(size), getLinearExpressionProtoBuilderFromLinearExpr( - LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false), + LinearExpr.newBuilder().add(start).add(size).build(), /*negate=*/false), name); } @@ -855,8 +862,7 @@ public final class CpModel { */ public IntervalVar newOptionalIntervalVar( LinearExpr start, LinearExpr size, LinearExpr end, Literal isPresent, String name) { - addEquality(LinearExpr.newBuilder().addExpression(start).addExpression(size).build(), end) - .onlyEnforceIf(isPresent); + addEquality(LinearExpr.newBuilder().add(start).add(size).build(), end).onlyEnforceIf(isPresent); return new IntervalVar(modelBuilder, getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false), getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false), @@ -883,7 +889,7 @@ public final class CpModel { getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false), getLinearExpressionProtoBuilderFromLong(size), getLinearExpressionProtoBuilderFromLinearExpr( - LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false), + LinearExpr.newBuilder().add(start).add(size).build(), /*negate=*/false), isPresent.getIndex(), name); } @@ -1124,5 +1130,5 @@ public final class CpModel { } private final CpModelProto.Builder modelBuilder; - private final Map constantMap; + private final Map constantMap; } diff --git a/ortools/java/com/google/ortools/sat/IntVar.java b/ortools/java/com/google/ortools/sat/IntVar.java index 75b52b6eb1..a41c1581b0 100644 --- a/ortools/java/com/google/ortools/sat/IntVar.java +++ b/ortools/java/com/google/ortools/sat/IntVar.java @@ -18,7 +18,7 @@ import com.google.ortools.sat.IntegerVariableProto; import com.google.ortools.util.Domain; /** An integer variable. */ -public final class IntVar implements Literal, LinearExpr { +public class IntVar implements LinearExpr { IntVar(CpModelProto.Builder builder, Domain domain, String name) { this.modelBuilder = builder; this.variableIndex = modelBuilder.getVariablesCount(); @@ -27,14 +27,12 @@ public final class IntVar implements Literal, LinearExpr { for (long b : domain.flattenedIntervals()) { this.varBuilder.addDomain(b); } - this.negation_ = null; } IntVar(CpModelProto.Builder builder, int index) { this.modelBuilder = builder; this.variableIndex = index; this.varBuilder = modelBuilder.getVariablesBuilder(index); - this.negation_ = null; } @Override @@ -48,7 +46,6 @@ public final class IntVar implements Literal, LinearExpr { } /** Internal, returns the index of the variable in the underlying CpModelProto. */ - @Override public int getIndex() { return variableIndex; } @@ -66,13 +63,17 @@ public final class IntVar implements Literal, LinearExpr { @Override public IntVar getVariable(int index) { - assert (index == 0); + if (index != 0) { + throw new IllegalArgumentException("wrong index in LinearExpr.getVariable(): " + index); + } return this; } @Override public long getCoefficient(int index) { - assert (index == 0); + if (index != 0) { + throw new IllegalArgumentException("wrong index in LinearExpr.getCoefficient(): " + index); + } return 1; } @@ -81,20 +82,6 @@ public final class IntVar implements Literal, LinearExpr { return 0; } - /** Returns a short string describing the variable. */ - @Override - public String getShortString() { - if (varBuilder.getName().isEmpty()) { - if (varBuilder.getDomainCount() == 2 && varBuilder.getDomain(0) == varBuilder.getDomain(1)) { - return String.format("%d", varBuilder.getDomain(0)); - } else { - return String.format("var_%d(%s)", getIndex(), displayBounds()); - } - } else { - return String.format("%s(%s)", getName(), displayBounds()); - } - } - /** Returns the domain as a string without the enclosing []. */ public String displayBounds() { String out = ""; @@ -111,22 +98,25 @@ public final class IntVar implements Literal, LinearExpr { return out; } - /** Returns the negation of a boolean variable. */ - @Override - public Literal not() { - if (negation_ == null) { - negation_ = new NotBooleanVariable(this); - } - return negation_; - } - /** Returns the domain of the variable. */ public Domain getDomain() { return CpSatHelper.variableDomain(varBuilder.build()); } - private final CpModelProto.Builder modelBuilder; - private final int variableIndex; - private final IntegerVariableProto.Builder varBuilder; - private NotBooleanVariable negation_ = null; + /** Returns a short string describing the variable. */ + public String getShortString() { + if (varBuilder.getName().isEmpty()) { + if (varBuilder.getDomainCount() == 2 && varBuilder.getDomain(0) == varBuilder.getDomain(1)) { + return String.format("%d", varBuilder.getDomain(0)); + } else { + return String.format("var_%d(%s)", getIndex(), displayBounds()); + } + } else { + return String.format("%s(%s)", getName(), displayBounds()); + } + } + + protected final CpModelProto.Builder modelBuilder; + protected final int variableIndex; + protected final IntegerVariableProto.Builder varBuilder; } diff --git a/ortools/java/com/google/ortools/sat/LinearExpr.java b/ortools/java/com/google/ortools/sat/LinearExpr.java index a1b2f19eae..b92e914f03 100644 --- a/ortools/java/com/google/ortools/sat/LinearExpr.java +++ b/ortools/java/com/google/ortools/sat/LinearExpr.java @@ -45,6 +45,11 @@ public interface LinearExpr { return newBuilder().addTerm(var, coeff).build(); } + /** Shortcut for newBuilder().addTerm(expr, coeff).build() */ + static LinearExpr term(LinearExpr expr, long coeff) { + return newBuilder().addTerm(expr, coeff).build(); + } + /** Shortcut for newBuilder().addTerm(literal, coeff).build() */ static LinearExpr term(Literal literal, long coeff) { return newBuilder().addTerm(literal, coeff).build(); @@ -55,26 +60,36 @@ public interface LinearExpr { return newBuilder().addSum(vars).build(); } + /** Shortcut for newBuilder().addSum(exprs).build() */ + static LinearExpr sum(LinearExpr[] exprs) { + return newBuilder().addSum(exprs).build(); + } + /** Shortcut for newBuilder().addSum(literals).build() */ static LinearExpr sum(Literal[] literals) { return newBuilder().addSum(literals).build(); } - /** Shortcut for newBuilder().addScalProd(vars, coeffs).build() */ - static LinearExpr scalProd(IntVar[] vars, long[] coeffs) { - return newBuilder().addScalProd(vars, coeffs).build(); + /** Shortcut for newBuilder().addWeightedSum(vars, coeffs).build() */ + static LinearExpr weightedSum(IntVar[] vars, long[] coeffs) { + return newBuilder().addWeightedSum(vars, coeffs).build(); } - /** Shortcut for newBuilder().addScalProd(literals, coeffs).build() */ - static LinearExpr scalProd(Literal[] literals, long[] coeffs) { - return newBuilder().addScalProd(literals, coeffs).build(); + /** Shortcut for newBuilder().addWeightedSum(literals, coeffs).build() */ + static LinearExpr weightedSum(Literal[] literals, long[] coeffs) { + return newBuilder().addWeightedSum(literals, coeffs).build(); + } + + /** Shortcut for newBuilder().addWeightedSum(exprs, coeffs).build() */ + static LinearExpr weightedSum(LinearExpr[] exprs, long[] coeffs) { + return newBuilder().addWeightedSum(exprs, coeffs).build(); } static LinearExpr rebuildFromLinearExpressionProto( LinearExpressionProto proto, CpModelProto.Builder builder) { int numElements = proto.getVarsCount(); if (numElements == 0) { - return new Constant(proto.getOffset()); + return new ConstantExpression(proto.getOffset()); } else if (numElements == 1) { return new AffineExpression( new IntVar(builder, proto.getVars(0)), proto.getCoeffs(0), proto.getOffset()); @@ -91,9 +106,9 @@ public interface LinearExpr { } } if (allOnes) { - return new SumOfVariables(vars, offset); + return new SumExpression(vars, offset); } else { - return new ScalProd(vars, coeffs, offset); + return new WeightedSumExpression(vars, coeffs, offset); } } } diff --git a/ortools/java/com/google/ortools/sat/LinearExprBuilder.java b/ortools/java/com/google/ortools/sat/LinearExprBuilder.java index c38dcb714c..85fcb9772b 100644 --- a/ortools/java/com/google/ortools/sat/LinearExprBuilder.java +++ b/ortools/java/com/google/ortools/sat/LinearExprBuilder.java @@ -28,19 +28,13 @@ public final class LinearExprBuilder { this.offset = 0; } - public LinearExprBuilder add(IntVar var) { - coefficients.merge(var, 1L, Long::sum); + public LinearExprBuilder add(LinearExpr expr) { + addTerm(expr, 1); return this; } public LinearExprBuilder add(Literal literal) { - final int index = literal.getIndex(); - if (index >= 0) { - coefficients.merge((IntVar) literal, 1L, Long::sum); - } else { - offset = offset + 1; - coefficients.merge((IntVar) literal.not(), -1L, Long::sum); - } + addTerm(literal, 1); return this; } @@ -49,79 +43,87 @@ public final class LinearExprBuilder { return this; } - public LinearExprBuilder addTerm(IntVar var, long coeff) { - coefficients.merge(var, coeff, Long::sum); + public LinearExprBuilder addTerm(LinearExpr expr, long coeff) { + final int numElements = expr.numElements(); + for (int i = 0; i < numElements; ++i) { + coefficients.merge(expr.getVariable(i), expr.getCoefficient(i) * coeff, Long::sum); + } + offset = offset + expr.getOffset() * coeff; return this; } public LinearExprBuilder addTerm(Literal literal, long coeff) { - final int index = literal.getIndex(); - if (index >= 0) { - coefficients.merge((IntVar) literal, coeff, Long::sum); - } else { + final BoolVar boolVar = literal.getBoolVar(); + if (literal.negated()) { + coefficients.merge(boolVar, -coeff, Long::sum); offset = offset + coeff; - coefficients.merge((IntVar) literal.not(), -coeff, Long::sum); + } else { + coefficients.merge(boolVar, coeff, Long::sum); } return this; } public LinearExprBuilder addSum(IntVar[] vars) { for (final IntVar var : vars) { - add(var); + addTerm(var, 1); } return this; } public LinearExprBuilder addSum(Literal[] literals) { for (final Literal literal : literals) { - add(literal); + addTerm(literal, 1); } return this; } - public LinearExprBuilder addScalProd(IntVar[] vars, long[] coeffs) { + public LinearExprBuilder addSum(LinearExpr[] exprs) { + for (final LinearExpr expr : exprs) { + addTerm(expr, 1); + } + return this; + } + + public LinearExprBuilder addWeightedSum(IntVar[] vars, long[] coeffs) { for (int i = 0; i < vars.length; ++i) { addTerm(vars[i], coeffs[i]); } - return this; } - public LinearExprBuilder addScalProd(IntVar[] vars, int[] coeffs) { + public LinearExprBuilder addWeightedSum(IntVar[] vars, int[] coeffs) { for (int i = 0; i < vars.length; ++i) { addTerm(vars[i], coeffs[i]); } - return this; } - public LinearExprBuilder addScalProd(Literal[] literals, long[] coeffs) { + public LinearExprBuilder addWeightedSum(Literal[] literals, long[] coeffs) { for (int i = 0; i < literals.length; ++i) { addTerm(literals[i], coeffs[i]); } - return this; } - public LinearExprBuilder addScalProd(Literal[] literals, int[] coeffs) { + public LinearExprBuilder addWeightedSum(Literal[] literals, int[] coeffs) { for (int i = 0; i < literals.length; ++i) { addTerm(literals[i], coeffs[i]); } - return this; } - public LinearExprBuilder addExpression(LinearExpr expr, long coeff) { - final int numElements = expr.numElements(); - for (int i = 0; i < numElements; ++i) { - addTerm(expr.getVariable(i), expr.getCoefficient(i) * coeff); + public LinearExprBuilder addWeightedSum(LinearExpr[] exprs, long[] coeffs) { + for (int i = 0; i < exprs.length; ++i) { + addTerm(exprs[i], coeffs[i]); } - add(expr.getOffset()); return this; } - public LinearExprBuilder addExpression(LinearExpr expr) { - return addExpression(expr, 1); + public LinearExprBuilder addWeightedSum(LinearExpr[] exprs, int[] coeffs) { + for (int i = 0; i < exprs.length; ++i) { + addTerm(exprs[i], coeffs[i]); + } + return this; } public LinearExpr build() { @@ -140,7 +142,7 @@ public final class LinearExprBuilder { } } if (numElements == 0) { - return new Constant(offset); + return new ConstantExpression(offset); } else if (numElements == 1) { return new AffineExpression(lastVar, lastCoeff, offset); } else if (allOnes) { @@ -152,7 +154,7 @@ public final class LinearExprBuilder { index++; } } - return new SumOfVariables(vars, offset); + return new SumExpression(vars, offset); } else { IntVar[] vars = new IntVar[numElements]; long[] coeffs = new long[numElements]; @@ -164,7 +166,7 @@ public final class LinearExprBuilder { index++; } } - return new ScalProd(vars, coeffs, offset); + return new WeightedSumExpression(vars, coeffs, offset); } } } diff --git a/ortools/java/com/google/ortools/sat/Literal.java b/ortools/java/com/google/ortools/sat/Literal.java index 1a0238c149..10a50d9c5f 100644 --- a/ortools/java/com/google/ortools/sat/Literal.java +++ b/ortools/java/com/google/ortools/sat/Literal.java @@ -14,7 +14,7 @@ package com.google.ortools.sat; /** Interface to describe a boolean variable or its negation. */ -public interface Literal { +public interface Literal extends LinearExpr { public int getIndex(); /** Returns the Boolean negation of the current literal. */ @@ -22,4 +22,10 @@ public interface Literal { /** Returns a short string to describe the literal. */ public String getShortString(); + + /** Returns the underlying BoolVar */ + public BoolVar getBoolVar(); + + /** Returns true if the literal is the negation of a Boolean variable */ + public boolean negated(); } diff --git a/ortools/java/com/google/ortools/sat/NotBooleanVariable.java b/ortools/java/com/google/ortools/sat/NotBooleanVariable.java index 5994db26e0..2ddcfe345f 100644 --- a/ortools/java/com/google/ortools/sat/NotBooleanVariable.java +++ b/ortools/java/com/google/ortools/sat/NotBooleanVariable.java @@ -18,7 +18,7 @@ package com.google.ortools.sat; * instead. */ public final class NotBooleanVariable implements Literal { - public NotBooleanVariable(IntVar boolVar) { + public NotBooleanVariable(BoolVar boolVar) { this.boolVar = boolVar; } @@ -34,11 +34,48 @@ public final class NotBooleanVariable implements Literal { return boolVar; } + @Override + public BoolVar getBoolVar() { + return boolVar; + } + + @Override + public boolean negated() { + return true; + } + + // LinearExpr interface. + @Override + public int numElements() { + return 1; + } + + @Override + public IntVar getVariable(int index) { + if (index != 0) { + throw new IllegalArgumentException("wrong index in LinearExpr.getVariable(): " + index); + } + return boolVar; + } + + @Override + public long getCoefficient(int index) { + if (index != 0) { + throw new IllegalArgumentException("wrong index in LinearExpr.getCoefficient(): " + index); + } + return -1; + } + + @Override + public long getOffset() { + return 1; + } + /** Returns a short string describing this literal. */ @Override public String getShortString() { return "not(" + boolVar.getShortString() + ")"; } - private final IntVar boolVar; + private final BoolVar boolVar; } diff --git a/ortools/java/com/google/ortools/sat/SumOfVariables.java b/ortools/java/com/google/ortools/sat/SumExpression.java similarity index 91% rename from ortools/java/com/google/ortools/sat/SumOfVariables.java rename to ortools/java/com/google/ortools/sat/SumExpression.java index 1a2fc434bc..99065bd983 100644 --- a/ortools/java/com/google/ortools/sat/SumOfVariables.java +++ b/ortools/java/com/google/ortools/sat/SumExpression.java @@ -14,11 +14,11 @@ package com.google.ortools.sat; /** A specialized linear expression: sum(xi) + b. */ -public final class SumOfVariables implements LinearExpr { +public final class SumExpression implements LinearExpr { private final IntVar[] variables; private final long offset; - public SumOfVariables(IntVar[] variables, long offset) { + public SumExpression(IntVar[] variables, long offset) { this.variables = variables; this.offset = offset; } diff --git a/ortools/java/com/google/ortools/sat/ScalProd.java b/ortools/java/com/google/ortools/sat/WeightedSumExpression.java similarity index 89% rename from ortools/java/com/google/ortools/sat/ScalProd.java rename to ortools/java/com/google/ortools/sat/WeightedSumExpression.java index ffdc99c465..d3d194033c 100644 --- a/ortools/java/com/google/ortools/sat/ScalProd.java +++ b/ortools/java/com/google/ortools/sat/WeightedSumExpression.java @@ -14,12 +14,12 @@ package com.google.ortools.sat; /** A specialized linear expression: sum(ai * xi) + b. */ -public final class ScalProd implements LinearExpr { +public final class WeightedSumExpression implements LinearExpr { private final IntVar[] variables; private final long[] coefficients; - private long offset; + private final long offset; - public ScalProd(IntVar[] variables, long[] coefficients, long offset) { + public WeightedSumExpression(IntVar[] variables, long[] coefficients, long offset) { this.variables = variables; this.coefficients = coefficients; this.offset = offset; diff --git a/ortools/sat/doc/README.md b/ortools/sat/doc/README.md index 75080baf10..8652c0a7ef 100644 --- a/ortools/sat/doc/README.md +++ b/ortools/sat/doc/README.md @@ -14,6 +14,8 @@ https://developers.google.com/optimization/cp/cp_solver * [C code samples](#c-code-samples) * [Java code samples](#java-code-samples) * [C# code samples](#c-code-samples-1) + + diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index 113d779765..fc975ab3cf 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -26,6 +26,8 @@ https://developers.google.com/optimization/ * [C# code](#c-code-5) * [Product of two Boolean Variables](#product-of-two-boolean-variables) * [Python code](#python-code-3) + + @@ -93,17 +95,17 @@ int main() { ```java package com.google.ortools.sat.samples; -import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; +import com.google.ortools.Loader; /** Code sample to demonstrate Boolean variable and literals. */ public class LiteralSampleSat { public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); + BoolVar x = model.newBoolVar("x"); Literal notX = x.not(); System.out.println(notX.getShortString()); } @@ -192,8 +194,8 @@ int main() { package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; /** Code sample to demonstrates a simple Boolean constraint. */ @@ -201,8 +203,8 @@ public class BoolOrSampleSat { public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); - IntVar y = model.newBoolVar("y"); + BoolVar x = model.newBoolVar("x"); + BoolVar y = model.newBoolVar("y"); model.addBoolOr(new Literal[] {x, y.not()}); } } @@ -319,8 +321,8 @@ int main() { package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; /** @@ -338,9 +340,9 @@ public class ReifiedSampleSat { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); - IntVar y = model.newBoolVar("y"); - IntVar b = model.newBoolVar("b"); + BoolVar x = model.newBoolVar("x"); + BoolVar y = model.newBoolVar("y"); + BoolVar b = model.newBoolVar("b"); // Version 1: a half-reified boolean and. model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b); diff --git a/ortools/sat/doc/channeling.md b/ortools/sat/doc/channeling.md index b6f8a5c2ae..d5d2906c94 100644 --- a/ortools/sat/doc/channeling.md +++ b/ortools/sat/doc/channeling.md @@ -17,6 +17,8 @@ https://developers.google.com/optimization/ * [C code](#c-code-2) * [Java code](#java-code-1) * [C# code](#c-code-3) + + @@ -178,6 +180,7 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; import com.google.ortools.sat.DecisionStrategyProto; import com.google.ortools.sat.SatParameters; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverSolutionCallback; @@ -195,7 +198,7 @@ public class ChannelingSampleSat { IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")}; // Declare our intermediate boolean variable. - IntVar b = model.newBoolVar("b"); + BoolVar b = model.newBoolVar("b"); // Implement b == (x >= 5). model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b); @@ -514,6 +517,7 @@ import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.LinearExpr; import com.google.ortools.sat.LinearExprBuilder; +import com.google.ortools.sat.Literal; /** Solves a bin packing problem with the CP-SAT solver. */ public class BinPackingProblemSat { @@ -546,7 +550,7 @@ public class BinPackingProblemSat { } // Slack variables. - IntVar[] slacks = new IntVar[numBins]; + Literal[] slacks = new Literal[numBins]; for (int b = 0; b < numBins; ++b) { slacks[b] = model.newBoolVar("slack_" + b); } diff --git a/ortools/sat/doc/integer_arithmetic.md b/ortools/sat/doc/integer_arithmetic.md index 412dcb8283..04d40a5c6b 100644 --- a/ortools/sat/doc/integer_arithmetic.md +++ b/ortools/sat/doc/integer_arithmetic.md @@ -33,6 +33,8 @@ https://developers.google.com/optimization/ * [C code](#c-code-4) * [Java code](#java-code-2) * [C# code](#c-code-5) + + diff --git a/ortools/sat/doc/model.md b/ortools/sat/doc/model.md index 48885ca274..a9d5a4d7d9 100644 --- a/ortools/sat/doc/model.md +++ b/ortools/sat/doc/model.md @@ -16,6 +16,8 @@ https://developers.google.com/optimization/ * [Model copy](#model-copy) * [Python code](#python-code-1) * [C code](#c-code-2) + + @@ -204,7 +206,7 @@ public class SolutionHintingSampleSat { // Create the constraints. model.addDifferent(x, y); - model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); + model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); // Solution hinting: x <- 1, y <- 2 model.addHint(x, 1); diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index 438873cd79..1eca60bedf 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -38,6 +38,8 @@ https://developers.google.com/optimization/ * [Precedences between intervals](#precedences-between-intervals) * [Convex hull of a set of intervals](#convex-hull-of-a-set-of-intervals) * [Reservoir constraint](#reservoir-constraint) + + @@ -991,6 +993,7 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; import com.google.ortools.sat.CpSolverStatus; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.IntVar; @@ -1006,9 +1009,10 @@ public class RankingSampleSat { /** * This code takes a list of interval variables in a noOverlap constraint, and a parallel list of * integer variables and enforces the following constraint + * *
    - *
  • rank[i] == -1 iff interval[i] is not active. - *
  • rank[i] == number of active intervals that precede interval[i]. + *
  • rank[i] == -1 iff interval[i] is not active. + *
  • rank[i] == number of active intervals that precede interval[i]. *
*/ static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) { @@ -1021,7 +1025,7 @@ public class RankingSampleSat { if (i == j) { precedences[i][i] = presences[i]; } else { - IntVar prec = model.newBoolVar(String.format("%d before %d", i, j)); + BoolVar prec = model.newBoolVar(String.format("%d before %d", i, j)); precedences[i][j] = prec; // Ensure that task i precedes task j if prec is true. model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec); @@ -1079,7 +1083,7 @@ public class RankingSampleSat { Literal[] presences = new Literal[numTasks]; IntVar[] ranks = new IntVar[numTasks]; - IntVar trueVar = model.newConstant(1); + Literal trueLiteral = model.trueLiteral(); // Creates intervals, half of them are optional. for (int t = 0; t < numTasks; ++t) { @@ -1090,7 +1094,7 @@ public class RankingSampleSat { intervals[t] = model.newIntervalVar( starts[t], LinearExpr.constant(duration), ends[t], "interval_" + t); - presences[t] = trueVar; + presences[t] = trueLiteral; } else { presences[t] = model.newBoolVar("presence_" + t); intervals[t] = diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index c1309e2225..3dc5b59b82 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -27,6 +27,8 @@ https://developers.google.com/optimization/ * [C code](#c-code-4) * [Java code](#java-code-2) * [C# code](#c-code-5) + + @@ -368,7 +370,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat { model.addDifferent(x, y); // Maximize a linear combination of variables. - model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); + model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); // Create a solver and solve the model. CpSolver solver = new CpSolver(); diff --git a/ortools/sat/samples/BinPackingProblemSat.java b/ortools/sat/samples/BinPackingProblemSat.java index 7877a32d2c..975143dbea 100644 --- a/ortools/sat/samples/BinPackingProblemSat.java +++ b/ortools/sat/samples/BinPackingProblemSat.java @@ -20,6 +20,7 @@ import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.LinearExpr; import com.google.ortools.sat.LinearExprBuilder; +import com.google.ortools.sat.Literal; /** Solves a bin packing problem with the CP-SAT solver. */ public class BinPackingProblemSat { @@ -52,7 +53,7 @@ public class BinPackingProblemSat { } // Slack variables. - IntVar[] slacks = new IntVar[numBins]; + Literal[] slacks = new Literal[numBins]; for (int b = 0; b < numBins; ++b) { slacks[b] = model.newBoolVar("slack_" + b); } diff --git a/ortools/sat/samples/BoolOrSampleSat.java b/ortools/sat/samples/BoolOrSampleSat.java index b3b1cec122..d1faa0b4b8 100644 --- a/ortools/sat/samples/BoolOrSampleSat.java +++ b/ortools/sat/samples/BoolOrSampleSat.java @@ -14,8 +14,8 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; /** Code sample to demonstrates a simple Boolean constraint. */ @@ -23,8 +23,8 @@ public class BoolOrSampleSat { public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); - IntVar y = model.newBoolVar("y"); + BoolVar x = model.newBoolVar("x"); + BoolVar y = model.newBoolVar("y"); model.addBoolOr(new Literal[] {x, y.not()}); } } diff --git a/ortools/sat/samples/ChannelingSampleSat.java b/ortools/sat/samples/ChannelingSampleSat.java index 0a3a8f45af..fa7e15303f 100644 --- a/ortools/sat/samples/ChannelingSampleSat.java +++ b/ortools/sat/samples/ChannelingSampleSat.java @@ -14,6 +14,7 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverSolutionCallback; @@ -33,7 +34,7 @@ public class ChannelingSampleSat { IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")}; // Declare our intermediate boolean variable. - IntVar b = model.newBoolVar("b"); + BoolVar b = model.newBoolVar("b"); // Implement b == (x >= 5). model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b); diff --git a/ortools/sat/samples/CpIsFunSat.java b/ortools/sat/samples/CpIsFunSat.java index 1422a91b78..d1bd3acfc1 100644 --- a/ortools/sat/samples/CpIsFunSat.java +++ b/ortools/sat/samples/CpIsFunSat.java @@ -77,7 +77,7 @@ public final class CpIsFunSat { model.addAllDifferent(letters); // CP + IS + FUN = TRUE - model.addEquality(LinearExpr.scalProd(new IntVar[] {c, p, i, s, f, u, n, t, r, u, e}, + model.addEquality(LinearExpr.weightedSum(new IntVar[] {c, p, i, s, f, u, n, t, r, u, e}, new long[] {base, 1, base, 1, base * base, base, 1, -base * base * base, -base * base, -base, -1}), 0); diff --git a/ortools/sat/samples/CpSatExample.java b/ortools/sat/samples/CpSatExample.java index 0224b46ae4..75ccd8730e 100644 --- a/ortools/sat/samples/CpSatExample.java +++ b/ortools/sat/samples/CpSatExample.java @@ -44,13 +44,13 @@ public final class CpSatExample { // Create the constraints. // [START constraints] - model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {2, 7, 3}), 50); - model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {3, -5, 7}), 45); - model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {5, 2, -6}), 37); + model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {2, 7, 3}), 50); + model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {3, -5, 7}), 45); + model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {5, 2, -6}), 37); // [END constraints] // [START objective] - model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {2, 2, 3})); + model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {2, 2, 3})); // [END objective] // Create a solver and solve the model. diff --git a/ortools/sat/samples/LiteralSampleSat.java b/ortools/sat/samples/LiteralSampleSat.java index 5b1bc26c0e..0d5e3d07c8 100644 --- a/ortools/sat/samples/LiteralSampleSat.java +++ b/ortools/sat/samples/LiteralSampleSat.java @@ -14,8 +14,8 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; /** Code sample to demonstrate Boolean variable and literals. */ @@ -23,7 +23,7 @@ public class LiteralSampleSat { public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); + BoolVar x = model.newBoolVar("x"); Literal notX = x.not(); System.out.println(notX.getShortString()); } diff --git a/ortools/sat/samples/RankingSampleSat.java b/ortools/sat/samples/RankingSampleSat.java index 3e3f2f7f0a..47076d56d8 100644 --- a/ortools/sat/samples/RankingSampleSat.java +++ b/ortools/sat/samples/RankingSampleSat.java @@ -14,6 +14,7 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverStatus; @@ -30,9 +31,10 @@ public class RankingSampleSat { /** * This code takes a list of interval variables in a noOverlap constraint, and a parallel list of * integer variables and enforces the following constraint + * *
    - *
  • rank[i] == -1 iff interval[i] is not active. - *
  • rank[i] == number of active intervals that precede interval[i]. + *
  • rank[i] == -1 iff interval[i] is not active. + *
  • rank[i] == number of active intervals that precede interval[i]. *
*/ static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) { @@ -45,7 +47,7 @@ public class RankingSampleSat { if (i == j) { precedences[i][i] = presences[i]; } else { - IntVar prec = model.newBoolVar(String.format("%d before %d", i, j)); + BoolVar prec = model.newBoolVar(String.format("%d before %d", i, j)); precedences[i][j] = prec; // Ensure that task i precedes task j if prec is true. model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec); @@ -103,7 +105,7 @@ public class RankingSampleSat { Literal[] presences = new Literal[numTasks]; IntVar[] ranks = new IntVar[numTasks]; - IntVar trueVar = model.newConstant(1); + Literal trueLiteral = model.trueLiteral(); // Creates intervals, half of them are optional. for (int t = 0; t < numTasks; ++t) { @@ -113,7 +115,7 @@ public class RankingSampleSat { if (t < numTasks / 2) { intervals[t] = model.newIntervalVar( starts[t], LinearExpr.constant(duration), ends[t], "interval_" + t); - presences[t] = trueVar; + presences[t] = trueLiteral; } else { presences[t] = model.newBoolVar("presence_" + t); intervals[t] = model.newOptionalIntervalVar( diff --git a/ortools/sat/samples/ReifiedSampleSat.java b/ortools/sat/samples/ReifiedSampleSat.java index 7eea4f34e4..c0690b0e14 100644 --- a/ortools/sat/samples/ReifiedSampleSat.java +++ b/ortools/sat/samples/ReifiedSampleSat.java @@ -14,8 +14,8 @@ package com.google.ortools.sat.samples; import com.google.ortools.Loader; +import com.google.ortools.sat.BoolVar; import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; /** @@ -33,9 +33,9 @@ public class ReifiedSampleSat { Loader.loadNativeLibraries(); CpModel model = new CpModel(); - IntVar x = model.newBoolVar("x"); - IntVar y = model.newBoolVar("y"); - IntVar b = model.newBoolVar("b"); + BoolVar x = model.newBoolVar("x"); + BoolVar y = model.newBoolVar("y"); + BoolVar b = model.newBoolVar("b"); // Version 1: a half-reified boolean and. model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b); diff --git a/ortools/sat/samples/SolutionHintingSampleSat.java b/ortools/sat/samples/SolutionHintingSampleSat.java index a6d2070bd8..16d409564b 100644 --- a/ortools/sat/samples/SolutionHintingSampleSat.java +++ b/ortools/sat/samples/SolutionHintingSampleSat.java @@ -45,7 +45,7 @@ public class SolutionHintingSampleSat { // [END constraints] // [START objective] - model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); + model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); // [END objective] // Solution hinting: x <- 1, y <- 2 diff --git a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java index e2a8619273..ea0f3c49ea 100644 --- a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java +++ b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java @@ -71,7 +71,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat { // Maximize a linear combination of variables. // [START objective] - model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); + model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3})); // [END objective] // Create a solver and solve the model.