always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] Add AtMostOne/AtLeastOne/ExactlyOne constraint in all languages; rewrite linear expressions in java

Browse Source
This commit is contained in:
Laurent Perron
2022-01-03 09:43:59 +01:00
parent ce02461741
commit 62d506143b
34 changed files with 754 additions and 525 deletions
Download Patch File Download Diff File Expand all files Collapse all files

34
ortools/java/com/google/ortools/sat/Difference.java → ortools/java/com/google/ortools/sat/AffineExpression.java
View File

@@ -13,41 +13,41 @@
package com.google.ortools.sat;
/** the substraction of two linear expressions. Used internally. */
final class Difference implements LinearExpr {
private final LinearExpr left;
private final LinearExpr right;
/** A linear expression interface that can be parsed. */
public final class AffineExpression implements LinearExpr {
private final IntVar var;
private final long coefficient;
private final long offset;
public Difference(LinearExpr left, LinearExpr right) {
this.left = left;
this.right = right;
public AffineExpression(IntVar var, long coefficient, long offset) {
this.var = var;
this.coefficient = coefficient;
this.offset = offset;
}
@Override
public int numElements() {
return left.numElements() + right.numElements();
return 1;
}
@Override
public IntVar getVariable(int index) {
if (index < left.numElements()) {
return left.getVariable(index);
} else {
return right.getVariable(index - left.numElements());
if (index != 0) {
throw new IllegalArgumentException("wrong index in LinearExpr.getVariable(): " + index);
}
return var;
}
@Override
public long getCoefficient(int index) {
if (index < left.numElements()) {
return left.getCoefficient(index);
} else {
return -right.getCoefficient(index - left.numElements());
if (index != 0) {
throw new IllegalArgumentException("wrong index in LinearExpr.getCoefficient(): " + index);
}
return coefficient;
}
@Override
public long getOffset() {
return left.getOffset() - right.getOffset();
return offset;
}
}

208
ortools/java/com/google/ortools/sat/CpModel.java
View File

@@ -121,6 +121,16 @@ public final class CpModel {
return ct;
}
/** Adds {@code Or(literals) == true}. */
public Constraint addBoolOr(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder boolOr = ct.getBuilder().getBoolOrBuilder();
for (Literal lit : literals) {
boolOr.addLiterals(lit.getIndex());
}
return ct;
}
/** Same as addBoolOr. {@code Sum(literals) >= 1}. */
public Constraint addAtLeastOne(Literal[] literals) {
Constraint ct = new Constraint(modelBuilder);
@@ -131,6 +141,16 @@ public final class CpModel {
return ct;
}
/** Same as addBoolOr. {@code Sum(literals) >= 1}. */
public Constraint addAtLeastOne(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder boolOr = ct.getBuilder().getBoolOrBuilder();
for (Literal lit : literals) {
boolOr.addLiterals(lit.getIndex());
}
return ct;
}
/** Adds {@code AtMostOne(literals): Sum(literals) <= 1}. */
public Constraint addAtMostOne(Literal[] literals) {
Constraint ct = new Constraint(modelBuilder);
@@ -141,6 +161,16 @@ public final class CpModel {
return ct;
}
/** Adds {@code AtMostOne(literals): Sum(literals) <= 1}. */
public Constraint addAtMostOne(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder atMostOne = ct.getBuilder().getAtMostOneBuilder();
for (Literal lit : literals) {
atMostOne.addLiterals(lit.getIndex());
}
return ct;
}
/** Adds {@code ExactlyOne(literals): Sum(literals) == 1}. */
public Constraint addExactlyOne(Literal[] literals) {
Constraint ct = new Constraint(modelBuilder);
@@ -151,6 +181,16 @@ public final class CpModel {
return ct;
}
/** Adds {@code ExactlyOne(literals): Sum(literals) == 1}. */
public Constraint addExactlyOne(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder exactlyOne = ct.getBuilder().getExactlyOneBuilder();
for (Literal lit : literals) {
exactlyOne.addLiterals(lit.getIndex());
}
return ct;
}
/** Adds {@code And(literals) == true}. */
public Constraint addBoolAnd(Literal[] literals) {
Constraint ct = new Constraint(modelBuilder);
@@ -161,6 +201,16 @@ public final class CpModel {
return ct;
}
/** Adds {@code And(literals) == true}. */
public Constraint addBoolAnd(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder boolAnd = ct.getBuilder().getBoolAndBuilder();
for (Literal lit : literals) {
boolAnd.addLiterals(lit.getIndex());
}
return ct;
}
/** Adds {@code XOr(literals) == true}. */
public Constraint addBoolXor(Literal[] literals) {
Constraint ct = new Constraint(modelBuilder);
@@ -171,6 +221,16 @@ public final class CpModel {
return ct;
}
/** Adds {@code XOr(literals) == true}. */
public Constraint addBoolXor(Iterable<Literal> literals) {
Constraint ct = new Constraint(modelBuilder);
BoolArgumentProto.Builder boolXOr = ct.getBuilder().getBoolXorBuilder();
for (Literal lit : literals) {
boolXOr.addLiterals(lit.getIndex());
}
return ct;
}
/** Adds {@code a => b}. */
public Constraint addImplication(Literal a, Literal b) {
return addBoolOr(new Literal[] {a.not(), b});
@@ -207,12 +267,10 @@ public final class CpModel {
/** Adds {@code left == right}. */
public Constraint addEquality(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(0));
}
/** Adds {@code left + offset == right}. */
public Constraint addEqualityWithOffset(LinearExpr left, LinearExpr right, long offset) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(-offset));
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(), new Domain(0));
}
/** Adds {@code expr <= value}. */
@@ -222,7 +280,10 @@ public final class CpModel {
/** Adds {@code left <= right}. */
public Constraint addLessOrEqual(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(Long.MIN_VALUE, 0));
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, 0));
}
/** Adds {@code expr < value}. */
@@ -232,13 +293,10 @@ public final class CpModel {
/** Adds {@code left < right}. */
public Constraint addLessThan(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(Long.MIN_VALUE, -1));
}
/** Adds {@code left + offset <= right}. */
public Constraint addLessOrEqualWithOffset(LinearExpr left, LinearExpr right, long offset) {
return addLinearExpressionInDomain(
new Difference(left, right), new Domain(Long.MIN_VALUE, -offset));
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, -1));
}
/** Adds {@code expr >= value}. */
@@ -248,7 +306,10 @@ public final class CpModel {
/** Adds {@code left >= right}. */
public Constraint addGreaterOrEqual(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(0, Long.MAX_VALUE));
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(), new Domain(0, Long.MAX_VALUE));
}
/** Adds {@code expr > value}. */
@@ -258,13 +319,10 @@ public final class CpModel {
/** Adds {@code left > right}. */
public Constraint addGreaterThan(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right), new Domain(1, Long.MAX_VALUE));
}
/** Adds {@code left + offset >= right}. */
public Constraint addGreaterOrEqualWithOffset(LinearExpr left, LinearExpr right, long offset) {
return addLinearExpressionInDomain(
new Difference(left, right), new Domain(-offset, Long.MAX_VALUE));
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(), new Domain(1, Long.MAX_VALUE));
}
/** Adds {@code expr != value}. */
@@ -276,17 +334,13 @@ public final class CpModel {
/** Adds {@code left != right}. */
public Constraint addDifferent(LinearExpr left, LinearExpr right) {
return addLinearExpressionInDomain(new Difference(left, right),
LinearExprBuilder difference = LinearExpr.newBuilder();
difference.addExpression(left, 1);
difference.addExpression(right, -1);
return addLinearExpressionInDomain(difference.build(),
Domain.fromFlatIntervals(new long[] {Long.MIN_VALUE, -1, 1, Long.MAX_VALUE}));
}
/** Adds {@code left + offset != right}. */
public Constraint addDifferentWithOffset(LinearExpr left, LinearExpr right, long offset) {
return addLinearExpressionInDomain(new Difference(left, right),
Domain.fromFlatIntervals(
new long[] {Long.MIN_VALUE, -offset - 1, -offset + 1, Long.MAX_VALUE}));
}
// Integer constraints.
/**
@@ -323,6 +377,20 @@ public final class CpModel {
return ct;
}
/**
* Adds {@code AllDifferent(expressions)}.
*
* @see addAllDifferent(LinearExpr[]).
*/
public Constraint addAllDifferent(Iterable<LinearExpr> expressions) {
Constraint ct = new Constraint(modelBuilder);
AllDifferentConstraintProto.Builder allDiff = ct.getBuilder().getAllDiffBuilder();
for (LinearExpr expr : expressions) {
allDiff.addExprs(getLinearExpressionProtoBuilderFromLinearExpr(expr, /*negate=*/false));
}
return ct;
}
/** Adds the element constraint: {@code variables[index] == target}. */
public Constraint addElement(IntVar index, IntVar[] variables, IntVar target) {
Constraint ct = new Constraint(modelBuilder);
@@ -407,6 +475,21 @@ public final class CpModel {
return ct;
}
/**
* Adds {@code AllowedAssignments(variables)}.
*
* @see addAllowedAssignments(IntVar[])
*/
public TableConstraint addAllowedAssignments(Iterable<IntVar> variables) {
TableConstraint ct = new TableConstraint(modelBuilder);
TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
for (IntVar var : variables) {
table.addVars(var.getIndex());
}
table.setNegated(false);
return ct;
}
/**
* Adds {@code ForbiddenAssignments(variables)}.
*
@@ -427,6 +510,21 @@ public final class CpModel {
return ct;
}
/**
* Adds {@code ForbiddenAssignments(variables)}.
*
* @see addForbiddenAssignments(IntVar[])
*/
public TableConstraint addForbiddenAssignments(Iterable<IntVar> variables) {
TableConstraint ct = new TableConstraint(modelBuilder);
TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
for (IntVar var : variables) {
table.addVars(var.getIndex());
}
table.setNegated(true);
return ct;
}
/**
* Adds an automaton constraint.
*
@@ -562,6 +660,17 @@ public final class CpModel {
return ct;
}
/** Adds {@code target == Min(exprs)}. */
public Constraint addMinEquality(LinearExpr target, Iterable<LinearExpr> exprs) {
Constraint ct = new Constraint(modelBuilder);
LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
linMax.setTarget(getLinearExpressionProtoBuilderFromLinearExpr(target, /*negate=*/true));
for (LinearExpr expr : exprs) {
linMax.addExprs(getLinearExpressionProtoBuilderFromLinearExpr(expr, /*negate=*/true));
}
return ct;
}
/** Adds {@code target == Max(vars)}. */
public Constraint addMaxEquality(LinearExpr target, IntVar[] vars) {
Constraint ct = new Constraint(modelBuilder);
@@ -584,6 +693,17 @@ public final class CpModel {
return ct;
}
/** Adds {@code target == Max(exprs)}. */
public Constraint addMaxEquality(LinearExpr target, Iterable<LinearExpr> exprs) {
Constraint ct = new Constraint(modelBuilder);
LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
linMax.setTarget(getLinearExpressionProtoBuilderFromLinearExpr(target, /*negate=*/false));
for (LinearExpr expr : exprs) {
linMax.addExprs(getLinearExpressionProtoBuilderFromLinearExpr(expr, /*negate=*/false));
}
return ct;
}
/** Adds {@code target == num / denom}, rounded towards 0. */
public Constraint addDivisionEquality(LinearExpr target, LinearExpr num, LinearExpr denom) {
Constraint ct = new Constraint(modelBuilder);
@@ -678,7 +798,10 @@ public final class CpModel {
*/
public IntervalVar newIntervalVar(
LinearExpr start, LinearExpr size, LinearExpr end, String name) {
addEquality(new Sum(start, size), end);
LinearExprBuilder expr = LinearExpr.newBuilder();
expr.addExpression(start);
expr.addExpression(size);
addEquality(expr.build(), end);
return new IntervalVar(modelBuilder,
getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false),
@@ -700,7 +823,8 @@ public final class CpModel {
return new IntervalVar(modelBuilder,
getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
getLinearExpressionProtoBuilderFromLong(size),
getLinearExpressionProtoBuilderFromLinearExpr(new Sum(start, size), /*negate=*/false),
getLinearExpressionProtoBuilderFromLinearExpr(
LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false),
name);
}
@@ -731,7 +855,8 @@ public final class CpModel {
*/
public IntervalVar newOptionalIntervalVar(
LinearExpr start, LinearExpr size, LinearExpr end, Literal isPresent, String name) {
addEquality(new Sum(start, size), end).onlyEnforceIf(isPresent);
addEquality(LinearExpr.newBuilder().addExpression(start).addExpression(size).build(), end)
.onlyEnforceIf(isPresent);
return new IntervalVar(modelBuilder,
getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false),
@@ -757,7 +882,8 @@ public final class CpModel {
return new IntervalVar(modelBuilder,
getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
getLinearExpressionProtoBuilderFromLong(size),
getLinearExpressionProtoBuilderFromLinearExpr(new Sum(start, size), /*negate=*/false),
getLinearExpressionProtoBuilderFromLinearExpr(
LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false),
isPresent.getIndex(), name);
}
@@ -786,6 +912,20 @@ public final class CpModel {
return ct;
}
/**
* Adds {@code NoOverlap(intervalVars)}.
*
* @see addNoOverlap(IntervalVar[]).
*/
public Constraint addNoOverlap(Iterable<IntervalVar> intervalVars) {
Constraint ct = new Constraint(modelBuilder);
NoOverlapConstraintProto.Builder noOverlap = ct.getBuilder().getNoOverlapBuilder();
for (IntervalVar var : intervalVars) {
noOverlap.addIntervals(var.getIndex());
}
return ct;
}
/**
* Adds {@code NoOverlap2D(xIntervals, yIntervals)}.
*

2
ortools/java/com/google/ortools/sat/IntervalVar.java
View File

@@ -77,7 +77,7 @@ public final class IntervalVar {
return LinearExpr.rebuildFromLinearExpressionProto(intervalBuilder.getSize(), modelBuilder);
}
/** Returns the size expression. */
/** Returns the end expression. */
public LinearExpr getEndExpr() {
return LinearExpr.rebuildFromLinearExpressionProto(intervalBuilder.getEnd(), modelBuilder);
}

112
ortools/java/com/google/ortools/sat/LinearExpr.java
View File

@@ -30,90 +30,54 @@ public interface LinearExpr {
/** Returns the constant part of the expression. */
long getOffset();
/** Creates a sum expression. */
static LinearExpr sum(IntVar[] variables) {
return new SumOfVariables(variables);
/** Returns a builder */
static LinearExprBuilder newBuilder() {
return new LinearExprBuilder();
}
/** Creates a sum expression. */
static LinearExpr booleanSum(Literal[] literals) {
// We need the scalar product for the negative coefficient of negated Boolean variables.
return new ScalProd(literals);
}
/** Creates a scalar product. */
static LinearExpr scalProd(IntVar[] variables, long[] coefficients) {
if (variables.length != coefficients.length) {
throw new CpModel.MismatchedArrayLengths("LinearExpr.scalProd", "variables", "coefficients");
}
return new ScalProd(variables, coefficients);
}
/** Creates a scalar product. */
static LinearExpr scalProd(IntVar[] variables, int[] coefficients) {
if (variables.length != coefficients.length) {
throw new CpModel.MismatchedArrayLengths("LinearExpr.scalProd", "variables", "coefficients");
}
long[] tmp = new long[coefficients.length];
for (int i = 0; i < coefficients.length; ++i) {
tmp[i] = coefficients[i];
}
return new ScalProd(variables, tmp);
}
/** Creates a scalar product. */
static LinearExpr booleanScalProd(Literal[] literals, long[] coefficients) {
if (literals.length != coefficients.length) {
throw new CpModel.MismatchedArrayLengths("LinearExpr.scalProd", "literals", "coefficients");
}
return new ScalProd(literals, coefficients);
}
/** Creates a scalar product. */
static LinearExpr booleanScalProd(Literal[] literals, int[] coefficients) {
if (literals.length != coefficients.length) {
throw new CpModel.MismatchedArrayLengths("LinearExpr.scalProd", "literals", "coefficients");
}
long[] tmp = new long[coefficients.length];
for (int i = 0; i < coefficients.length; ++i) {
tmp[i] = coefficients[i];
}
return new ScalProd(literals, tmp);
}
/** Creates a linear term (var * coefficient). */
static LinearExpr term(IntVar variable, long coefficient) {
return new ScalProd(variable, coefficient, 0);
}
/** Creates a linear term (lit * coefficient). */
static LinearExpr term(Literal lit, long coefficient) {
return new ScalProd(lit, coefficient, 0);
}
/** Creates an affine expression (var * coefficient + offset). */
static LinearExpr affine(IntVar variable, long coefficient, long offset) {
return new ScalProd(variable, coefficient, offset);
}
/** Creates an affine expression (lit * coefficient + offset). */
static LinearExpr affine(Literal lit, long coefficient, long offset) {
return new ScalProd(lit, coefficient, offset);
}
/** Creates an constant expression. */
/** Shortcut for newBuilder().add(value).build() */
static LinearExpr constant(long value) {
return new Constant(value);
return newBuilder().add(value).build();
}
/** Shortcut for newBuilder().addTerm(var, coeff).build() */
static LinearExpr term(IntVar var, long coeff) {
return newBuilder().addTerm(var, coeff).build();
}
/** Shortcut for newBuilder().addTerm(literal, coeff).build() */
static LinearExpr term(Literal literal, long coeff) {
return newBuilder().addTerm(literal, coeff).build();
}
/** Shortcut for newBuilder().addSum(vars).build() */
static LinearExpr sum(IntVar[] vars) {
return newBuilder().addSum(vars).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().addScalProd(literals, coeffs).build() */
static LinearExpr scalProd(Literal[] literals, long[] coeffs) {
return newBuilder().addScalProd(literals, coeffs).build();
}
static LinearExpr rebuildFromLinearExpressionProto(
LinearExpressionProto proto, CpModelProto.Builder builder) {
int numElements = proto.getVarsCount();
if (numElements == 0) {
return constant(proto.getOffset());
return new Constant(proto.getOffset());
} else if (numElements == 1) {
return affine(new IntVar(builder, proto.getVars(0)), proto.getCoeffs(0), proto.getOffset());
return new AffineExpression(
new IntVar(builder, proto.getVars(0)), proto.getCoeffs(0), proto.getOffset());
} else {
IntVar[] vars = new IntVar[numElements];
long[] coeffs = new long[numElements];

170
ortools/java/com/google/ortools/sat/LinearExprBuilder.java Normal file
View File

@@ -0,0 +1,170 @@
// 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 static java.util.Comparator.comparingInt;
import java.util.Map;
import java.util.TreeMap;
/** Builder class for the LinearExpr container. */
public final class LinearExprBuilder {
private final TreeMap<IntVar, Long> coefficients;
private long offset;
LinearExprBuilder() {
this.coefficients = new TreeMap<>(comparingInt(IntVar::getIndex));
this.offset = 0;
}
public LinearExprBuilder add(IntVar var) {
coefficients.merge(var, 1L, Long::sum);
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);
}
return this;
}
public LinearExprBuilder add(long constant) {
offset = offset + constant;
return this;
}
public LinearExprBuilder addTerm(IntVar var, long coeff) {
coefficients.merge(var, coeff, Long::sum);
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 {
offset = offset + coeff;
coefficients.merge((IntVar) literal.not(), -coeff, Long::sum);
}
return this;
}
public LinearExprBuilder addSum(IntVar[] vars) {
for (final IntVar var : vars) {
add(var);
}
return this;
}
public LinearExprBuilder addSum(Literal[] literals) {
for (final Literal literal : literals) {
add(literal);
}
return this;
}
public LinearExprBuilder addScalProd(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) {
for (int i = 0; i < vars.length; ++i) {
addTerm(vars[i], coeffs[i]);
}
return this;
}
public LinearExprBuilder addScalProd(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) {
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);
}
add(expr.getOffset());
return this;
}
public LinearExprBuilder addExpression(LinearExpr expr) {
return addExpression(expr, 1);
}
public LinearExpr build() {
boolean allOnes = true;
int numElements = 0;
IntVar lastVar = null;
long lastCoeff = 0;
for (Map.Entry<IntVar, Long> entry : coefficients.entrySet()) {
if (entry.getValue() != 0) {
numElements++;
lastVar = entry.getKey();
lastCoeff = entry.getValue();
if (lastCoeff != 1) {
allOnes = false;
}
}
}
if (numElements == 0) {
return new Constant(offset);
} else if (numElements == 1) {
return new AffineExpression(lastVar, lastCoeff, offset);
} else if (allOnes) {
IntVar[] vars = new IntVar[numElements];
int index = 0;
for (Map.Entry<IntVar, Long> entry : coefficients.entrySet()) {
if (entry.getValue() != 0) {
vars[index] = entry.getKey();
index++;
}
}
return new SumOfVariables(vars, offset);
} else {
IntVar[] vars = new IntVar[numElements];
long[] coeffs = new long[numElements];
int index = 0;
for (Map.Entry<IntVar, Long> entry : coefficients.entrySet()) {
if (entry.getValue() != 0) {
vars[index] = entry.getKey();
coeffs[index] = entry.getValue();
index++;
}
}
return new ScalProd(vars, coeffs, offset);
}
}
}

58
ortools/java/com/google/ortools/sat/Sum.java
View File

@@ -1,58 +0,0 @@
// 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;
/** the sum of two linear expressions. Used internally. */
final class Sum implements LinearExpr {
private final LinearExpr left;
private final LinearExpr right;
public Sum(LinearExpr left, LinearExpr right) {
this.left = left;
this.right = right;
}
public Sum(LinearExpr left, long right) {
this.left = left;
this.right = new Constant(right);
}
@Override
public int numElements() {
return left.numElements() + right.numElements();
}
@Override
public IntVar getVariable(int index) {
if (index < left.numElements()) {
return left.getVariable(index);
} else {
return right.getVariable(index - left.numElements());
}
}
@Override
public long getCoefficient(int index) {
if (index < left.numElements()) {
return left.getCoefficient(index);
} else {
return right.getCoefficient(index - left.numElements());
}
}
@Override
public long getOffset() {
return left.getOffset() + right.getOffset();
}
}

32
ortools/sat/doc/channeling.md
View File

@@ -194,25 +194,24 @@ public class ChannelingSampleSat {
CpModel model = new CpModel();
// Declare our two primary variables.
IntVar x = model.newIntVar(0, 10, "x");
IntVar y = model.newIntVar(0, 10, "y");
IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")};
// Declare our intermediate boolean variable.
IntVar b = model.newBoolVar("b");
// Implement b == (x >= 5).
model.addGreaterOrEqual(x, 5).onlyEnforceIf(b);
model.addLessOrEqual(x, 4).onlyEnforceIf(b.not());
model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b);
model.addLessOrEqual(vars[0], 4).onlyEnforceIf(b.not());
// Create our two half-reified constraints.
// First, b implies (y == 10 - x).
model.addEquality(LinearExpr.sum(new IntVar[] {x, y}), 10).onlyEnforceIf(b);
model.addEquality(LinearExpr.sum(vars), 10).onlyEnforceIf(b);
// Second, not(b) implies y == 0.
model.addEquality(y, 0).onlyEnforceIf(b.not());
model.addEquality(vars[1], 0).onlyEnforceIf(b.not());
// Search for x values in increasing order.
model.addDecisionStrategy(
new IntVar[] {x},
new IntVar[] {vars[0]},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
@@ -242,7 +241,7 @@ public class ChannelingSampleSat {
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, y, b}));
}.init(new IntVar[] {vars[0], vars[1], b}));
}
}
```
@@ -516,6 +515,7 @@ import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.LinearExpr;
import com.google.ortools.sat.LinearExprBuilder;
/** Solves a bin packing problem with the CP-SAT solver. */
public class BinPackingProblemSat {
@@ -554,25 +554,21 @@ public class BinPackingProblemSat {
}
// Links load and x.
int[] sizes = new int[numItems];
for (int i = 0; i < numItems; ++i) {
sizes[i] = items[i][0];
}
for (int b = 0; b < numBins; ++b) {
IntVar[] vars = new IntVar[numItems];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int i = 0; i < numItems; ++i) {
vars[i] = x[i][b];
expr.addTerm(x[i][b], items[i][0]);
}
model.addEquality(LinearExpr.scalProd(vars, sizes), load[b]);
model.addEquality(expr.build(), load[b]);
}
// Place all items.
for (int i = 0; i < numItems; ++i) {
IntVar[] vars = new IntVar[numBins];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int b = 0; b < numBins; ++b) {
vars[b] = x[i][b];
expr.add(x[i][b]);
}
model.addEquality(LinearExpr.sum(vars), items[i][1]);
model.addEquality(expr.build(), items[i][1]);
}
// Links load and slack.

35
ortools/sat/doc/integer_arithmetic.md
View File

@@ -238,9 +238,9 @@ public class RabbitsAndPheasantsSat {
IntVar r = model.newIntVar(0, 100, "r");
IntVar p = model.newIntVar(0, 100, "p");
// 20 heads.
model.addEquality(LinearExpr.sum(new IntVar[] {r, p}), 20);
model.addEquality(LinearExpr.newBuilder().add(r).add(p).build(), 20);
// 56 legs.
model.addEquality(LinearExpr.scalProd(new IntVar[] {r, p}, new long[] {4, 2}), 56);
model.addEquality(LinearExpr.newBuilder().addTerm(r, 4).addTerm(p, 2).build(), 56);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
@@ -505,23 +505,20 @@ public class EarlinessTardinessCostSampleSat {
long largeConstant = 1000;
IntVar expr = model.newIntVar(0, largeConstant, "expr");
// First segment: s1 == earlinessCost * (earlinessDate - x).
IntVar s1 = model.newIntVar(-largeConstant, largeConstant, "s1");
model.addEquality(
LinearExpr.scalProd(new IntVar[] {s1, x}, new long[] {1, earlinessCost}),
earlinessCost * earlinessDate);
// Second segment.
IntVar s2 = model.newConstant(0);
// Third segment: s3 == latenessCost * (x - latenessDate).
IntVar s3 = model.newIntVar(-largeConstant, largeConstant, "s3");
model.addEquality(
LinearExpr.scalProd(new IntVar[] {s3, x}, new long[] {1, -latenessCost}),
-latenessCost * latenessDate);
// Link together expr and x through s1, s2, and s3.
model.addMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Link together expr and the 3 segment.
// First segment: y == earlinessCost * (earlinessDate - x).
// Second segment: y = 0
// Third segment: y == latenessCost * (x - latenessDate).
model.addMaxEquality(
expr,
new LinearExpr[] {
LinearExpr.newBuilder()
.addTerm(x, -earlinessCost)
.add(earlinessCost * earlinessDate)
.build(),
LinearExpr.constant(0),
LinearExpr.newBuilder().addTerm(x, latenessCost).add(-latenessCost * latenessDate).build()
});
// Search for x values in increasing order.
model.addDecisionStrategy(

2
ortools/sat/doc/model.md
View File

@@ -206,7 +206,7 @@ public class SolutionHintingSampleSat {
// Create the constraints.
model.addDifferent(x, y);
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {1, 2, 3}));
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
// Solution hinting: x <- 1, y <- 2
model.addHint(x, 1);

57
ortools/sat/doc/scheduling.md
View File

@@ -175,7 +175,10 @@ public class IntervalSampleSat {
IntVar endVar = model.newIntVar(0, horizon, "end");
IntervalVar intervalVar =
model.newIntervalVar(
startVar, LinearExpr.constant(10), LinearExpr.affine(endVar, 1, 2), "interval");
startVar,
LinearExpr.constant(10),
LinearExpr.newBuilder().add(endVar).add(2).build(),
"interval");
System.out.println(intervalVar);
// If the size is fixed, a simpler version uses the start expression and the size.
@@ -344,7 +347,7 @@ public class OptionalIntervalSampleSat {
model.newOptionalIntervalVar(
startVar,
LinearExpr.constant(10),
LinearExpr.affine(endVar, 1, 2),
LinearExpr.newBuilder().add(endVar).add(2).build(),
presence,
"interval");
System.out.println(intervalVar);
@@ -568,20 +571,17 @@ public class NoOverlapSampleSat {
// Task 0, duration 2.
IntVar start0 = model.newIntVar(0, horizon, "start0");
int duration0 = 2;
IntVar end0 = model.newIntVar(0, horizon, "end0");
IntervalVar task0 = model.newIntervalVar(start0, LinearExpr.constant(duration0), end0, "task0");
IntervalVar task0 = model.newFixedSizeIntervalVar(start0, duration0, "task0");
// Task 1, duration 4.
IntVar start1 = model.newIntVar(0, horizon, "start1");
int duration1 = 4;
IntVar end1 = model.newIntVar(0, horizon, "end1");
IntervalVar task1 = model.newIntervalVar(start1, LinearExpr.constant(duration1), end1, "task1");
IntervalVar task1 = model.newFixedSizeIntervalVar(start1, duration1, "task1");
// Task 2, duration 3.
IntVar start2 = model.newIntVar(0, horizon, "start2");
int duration2 = 3;
IntVar end2 = model.newIntVar(0, horizon, "end2");
IntervalVar task2 = model.newIntervalVar(start2, LinearExpr.constant(duration2), end2, "task2");
IntervalVar task2 = model.newFixedSizeIntervalVar(start2, duration2, "task2");
// Weekends.
IntervalVar weekend0 = model.newFixedInterval(5, 2, "weekend0");
@@ -595,7 +595,13 @@ public class NoOverlapSampleSat {
// Makespan objective.
IntVar obj = model.newIntVar(0, horizon, "makespan");
model.addMaxEquality(obj, new IntVar[] {end0, end1, end2});
model.addMaxEquality(
obj,
new LinearExpr[] {
LinearExpr.newBuilder().add(start0).add(duration0).build(),
LinearExpr.newBuilder().add(start1).add(duration1).build(),
LinearExpr.newBuilder().add(start2).add(duration2).build()
});
model.minimize(obj);
// Creates a solver and solves the model.
@@ -992,6 +998,7 @@ import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.IntervalVar;
import com.google.ortools.sat.LinearExpr;
import com.google.ortools.sat.LinearExprBuilder;
import com.google.ortools.sat.Literal;
import java.util.ArrayList;
import java.util.List;
@@ -1019,7 +1026,7 @@ public class RankingSampleSat {
IntVar 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.addLessOrEqualWithOffset(starts[i], starts[j], 1).onlyEnforceIf(prec);
model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec);
}
}
}
@@ -1041,7 +1048,7 @@ public class RankingSampleSat {
// The following boolOr will enforce that for any two intervals:
// i precedes j or j precedes i or at least one interval is not
// performed.
model.addBoolOr(list.toArray(new Literal[0]));
model.addBoolOr(list);
// For efficiency, we add a redundant constraint declaring that only one of i precedes j and
// j precedes i are true. This will speed up the solve because the reason of this
// propagation is shorter that using interval bounds is true.
@@ -1052,16 +1059,13 @@ public class RankingSampleSat {
// Links precedences and ranks.
for (int i = 0; i < numTasks; ++i) {
IntVar[] vars = new IntVar[numTasks + 1];
int[] coefs = new int[numTasks + 1];
for (int j = 0; j < numTasks; ++j) {
vars[j] = (IntVar) precedences[j][i];
coefs[j] = 1;
}
vars[numTasks] = ranks[i];
coefs[numTasks] = -1;
// ranks == sum(precedences) - 1;
model.addEquality(LinearExpr.scalProd(vars, coefs), 1);
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int j = 0; j < numTasks; ++j) {
expr.add(precedences[j][i]);
}
expr.add(-1);
model.addEquality(ranks[i], expr.build());
}
}
@@ -1107,7 +1111,7 @@ public class RankingSampleSat {
rankTasks(model, starts, presences, ranks);
// Adds a constraint on ranks (ranks[0] < ranks[1]).
model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
model.addLessThan(ranks[0], ranks[1]);
// Creates makespan variable.
IntVar makespan = model.newIntVar(0, horizon, "makespan");
@@ -1121,15 +1125,12 @@ public class RankingSampleSat {
//
// On this problem, as the fixed cost is less that the duration of the last interval, the solver
// will not perform the last interval.
IntVar[] objectiveVars = new IntVar[numTasks + 1];
int[] objectiveCoefs = new int[numTasks + 1];
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int t = 0; t < numTasks; ++t) {
objectiveVars[t] = (IntVar) presences[t];
objectiveCoefs[t] = -7;
obj.addTerm(presences[t], -7);
}
objectiveVars[numTasks] = makespan;
objectiveCoefs[numTasks] = 2;
model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
obj.addTerm(makespan, 2);
model.minimize(obj.build());
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();

2
ortools/sat/doc/solver.md
View File

@@ -370,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 int[] {1, 2, 3}));
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
// Create a solver and solve the model.
CpSolver solver = new CpSolver();

98
ortools/sat/samples/AssignmentGroupsSat.java
View File

@@ -11,8 +11,8 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// CP-SAT example that solves an assignment problem.
// [START program]
// CP-SAT example that solves an assignment problem.
package com.google.ortools.sat.samples;
// [START import]
import com.google.ortools.Loader;
@@ -21,7 +21,11 @@ import com.google.ortools.sat.CpSolver;
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;
import com.google.ortools.sat.TableConstraint;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
@@ -32,10 +36,18 @@ public class AssignmentGroupsSat {
// Data
// [START data]
int[][] costs = {
{ 90, 76, 75, 70, 50, 74 }, { 35, 85, 55, 65, 48, 101 }, { 125, 95, 90, 105, 59, 120 },
{ 45, 110, 95, 115, 104, 83 }, { 60, 105, 80, 75, 59, 62 }, { 45, 65, 110, 95, 47, 31 },
{ 38, 51, 107, 41, 69, 99 }, { 47, 85, 57, 71, 92, 77 }, { 39, 63, 97, 49, 118, 56 },
{ 47, 101, 71, 60, 88, 109 }, { 17, 39, 103, 64, 61, 92 }, { 101, 45, 83, 59, 92, 27 },
{90, 76, 75, 70, 50, 74},
{35, 85, 55, 65, 48, 101},
{125, 95, 90, 105, 59, 120},
{45, 110, 95, 115, 104, 83},
{60, 105, 80, 75, 59, 62},
{45, 65, 110, 95, 47, 31},
{38, 51, 107, 41, 69, 99},
{47, 85, 57, 71, 92, 77},
{39, 63, 97, 49, 118, 56},
{47, 101, 71, 60, 88, 109},
{17, 39, 103, 64, 61, 92},
{101, 45, 83, 59, 92, 27},
};
final int numWorkers = costs.length;
final int numTasks = costs[0].length;
@@ -47,27 +59,27 @@ public class AssignmentGroupsSat {
// Allowed groups of workers:
// [START allowed_groups]
int[][] group1 = {
{ 0, 0, 1, 1 }, // Workers 2, 3
{ 0, 1, 0, 1 }, // Workers 1, 3
{ 0, 1, 1, 0 }, // Workers 1, 2
{ 1, 1, 0, 0 }, // Workers 0, 1
{ 1, 0, 1, 0 }, // Workers 0, 2
{0, 0, 1, 1}, // Workers 2, 3
{0, 1, 0, 1}, // Workers 1, 3
{0, 1, 1, 0}, // Workers 1, 2
{1, 1, 0, 0}, // Workers 0, 1
{1, 0, 1, 0}, // Workers 0, 2
};
int[][] group2 = {
{ 0, 0, 1, 1 }, // Workers 6, 7
{ 0, 1, 0, 1 }, // Workers 5, 7
{ 0, 1, 1, 0 }, // Workers 5, 6
{ 1, 1, 0, 0 }, // Workers 4, 5
{ 1, 0, 0, 1 }, // Workers 4, 7
{0, 0, 1, 1}, // Workers 6, 7
{0, 1, 0, 1}, // Workers 5, 7
{0, 1, 1, 0}, // Workers 5, 6
{1, 1, 0, 0}, // Workers 4, 5
{1, 0, 0, 1}, // Workers 4, 7
};
int[][] group3 = {
{ 0, 0, 1, 1 }, // Workers 10, 11
{ 0, 1, 0, 1 }, // Workers 9, 11
{ 0, 1, 1, 0 }, // Workers 9, 10
{ 1, 0, 1, 0 }, // Workers 8, 10
{ 1, 0, 0, 1 }, // Workers 8, 11
{0, 0, 1, 1}, // Workers 10, 11
{0, 1, 0, 1}, // Workers 9, 11
{0, 1, 1, 0}, // Workers 9, 10
{1, 0, 1, 0}, // Workers 8, 10
{1, 0, 0, 1}, // Workers 8, 11
};
// [END allowed_groups]
@@ -78,16 +90,10 @@ public class AssignmentGroupsSat {
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
Literal[][] x = new Literal[numWorkers][numTasks];
for (int worker : allWorkers) {
for (int task : allTasks) {
x[worker][task] = model.newBoolVar("x["+worker+","+task+"]");
int k = worker * numTasks + task;
xFlat[k] = x[worker][task];
costsFlat[k] = costs[worker][task];
x[worker][task] = model.newBoolVar("x[" + worker + "," + task + "]");
}
}
// [END variables]
@@ -96,20 +102,20 @@ public class AssignmentGroupsSat {
// [START constraints]
// Each worker is assigned to at most one task.
for (int worker : allWorkers) {
IntVar[] vars = new IntVar[numTasks];
List<Literal> tasks = new ArrayList<>();
for (int task : allTasks) {
vars[task] = x[worker][task];
tasks.add(x[worker][task]);
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
model.addAtMostOne(tasks);
}
// Each task is assigned to exactly one worker.
for (int task : allTasks) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
List<Literal> workers = new ArrayList<>();
for (int worker : allWorkers) {
vars[worker] = x[worker][task];
workers.add(x[worker][task]);
}
model.addEquality(LinearExpr.sum(vars), 1);
model.addExactlyOne(workers);
}
// [END constraints]
@@ -117,15 +123,15 @@ public class AssignmentGroupsSat {
// Create variables for each worker, indicating whether they work on some task.
IntVar[] work = new IntVar[numWorkers];
for (int worker : allWorkers) {
work[worker] = model.newBoolVar("work["+worker+"]");
work[worker] = model.newBoolVar("work[" + worker + "]");
}
for (int worker : allWorkers) {
IntVar[] vars = new IntVar[numTasks];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int task : allTasks) {
vars[task] = x[worker][task];
expr.add(x[worker][task]);
}
model.addEquality(work[worker], LinearExpr.sum(vars));
model.addEquality(work[worker], expr.build());
}
// Define the allowed groups of worders
@@ -148,7 +154,13 @@ public class AssignmentGroupsSat {
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int worker : allWorkers) {
for (int task : allTasks) {
obj.addTerm(x[worker][task], costs[worker][task]);
}
}
model.minimize(obj.build());
// [END objective]
// Solve
@@ -164,9 +176,9 @@ public class AssignmentGroupsSat {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int worker : allWorkers) {
for (int task : allTasks) {
if (solver.value(x[worker][task]) == 1) {
System.out.println(
"Worker " + worker + " assigned to task " + task + ". Cost: " + costs[worker][task]);
if (solver.booleanValue(x[worker][task])) {
System.out.println("Worker " + worker + " assigned to task " + task
+ ". Cost: " + costs[worker][task]);
}
}
}

55
ortools/sat/samples/AssignmentSat.java
View File

@@ -19,8 +19,12 @@ import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
/** Assignment problem. */
@@ -38,6 +42,9 @@ public class AssignmentSat {
};
final int numWorkers = costs.length;
final int numTasks = costs[0].length;
final int[] allWorkers = IntStream.range(0, numWorkers).toArray();
final int[] allTasks = IntStream.range(0, numTasks).toArray();
// [END data_model]
// Model
@@ -47,16 +54,10 @@ public class AssignmentSat {
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
x[i][j] = model.newIntVar(0, 1, "");
int k = i * numTasks + j;
xFlat[k] = x[i][j];
costsFlat[k] = costs[i][j];
Literal[][] x = new Literal[numWorkers][numTasks];
for (int worker : allWorkers) {
for (int task : allTasks) {
x[worker][task] = model.newBoolVar("x[" + worker + "," + task + "]");
}
}
// [END variables]
@@ -64,27 +65,33 @@ public class AssignmentSat {
// Constraints
// [START constraints]
// Each worker is assigned to at most one task.
for (int i = 0; i < numWorkers; ++i) {
IntVar[] vars = new IntVar[numTasks];
for (int j = 0; j < numTasks; ++j) {
vars[j] = x[i][j];
for (int worker : allWorkers) {
List<Literal> tasks = new ArrayList<>();
for (int task : allTasks) {
tasks.add(x[worker][task]);
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
model.addAtMostOne(tasks);
}
// Each task is assigned to exactly one worker.
for (int j = 0; j < numTasks; ++j) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
for (int i = 0; i < numWorkers; ++i) {
vars[i] = x[i][j];
for (int task : allTasks) {
List<Literal> workers = new ArrayList<>();
for (int worker : allWorkers) {
workers.add(x[worker][task]);
}
model.addEquality(LinearExpr.sum(vars), 1);
model.addExactlyOne(workers);
}
// [END constraints]
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int worker : allWorkers) {
for (int task : allTasks) {
obj.addTerm(x[worker][task], costs[worker][task]);
}
}
model.minimize(obj.build());
// [END objective]
// Solve
@@ -100,7 +107,7 @@ public class AssignmentSat {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
if (solver.value(x[i][j]) == 1) {
if (solver.booleanValue(x[i][j])) {
System.out.println(
"Worker " + i + " assigned to task " + j + ". Cost: " + costs[i][j]);
}

41
ortools/sat/samples/AssignmentTaskSizesSat.java
View File

@@ -11,16 +11,19 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// CP-SAT example that solves an assignment problem.
// [START program]
// CP-SAT example that solves an assignment problem.
package com.google.ortools.sat.samples;
// [START import]
import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
@@ -60,44 +63,44 @@ public class AssignmentTaskSizesSat {
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
Literal[][] x = new Literal[numWorkers][numTasks];
for (int worker : allWorkers) {
for (int task : allTasks) {
x[worker][task] = model.newBoolVar("x[" + worker + "," + task + "]");
int k = worker * numTasks + task;
xFlat[k] = x[worker][task];
costsFlat[k] = costs[worker][task];
}
}
// [END variables]
// Constraints
// [START constraints]
// Each worker is assigned to at most one task.
// Each worker has a maximum capacity.
for (int worker : allWorkers) {
IntVar[] vars = new IntVar[numTasks];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int task : allTasks) {
vars[task] = x[worker][task];
expr.addTerm(x[worker][task], taskSizes[task]);
}
model.addLessOrEqual(LinearExpr.scalProd(vars, taskSizes), totalSizeMax);
model.addLessOrEqual(expr.build(), totalSizeMax);
}
// Each task is assigned to exactly one worker.
for (int task : allTasks) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
List<Literal> workers = new ArrayList<>();
for (int worker : allWorkers) {
vars[worker] = x[worker][task];
workers.add(x[worker][task]);
}
model.addEquality(LinearExpr.sum(vars), 1);
model.addExactlyOne(workers);
}
// [END constraints]
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int worker : allWorkers) {
for (int task : allTasks) {
obj.addTerm(x[worker][task], costs[worker][task]);
}
}
model.minimize(obj.build());
// [END objective]
// Solve
@@ -113,7 +116,7 @@ public class AssignmentTaskSizesSat {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int worker : allWorkers) {
for (int task : allTasks) {
if (solver.value(x[worker][task]) == 1) {
if (solver.booleanValue(x[worker][task])) {
System.out.println("Worker " + worker + " assigned to task " + task
+ ". Cost: " + costs[worker][task]);
}

44
ortools/sat/samples/AssignmentTeamsSat.java
View File

@@ -11,16 +11,17 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// CP-SAT example that solves an assignment problem.
// [START program]
// CP-SAT example that solves an assignment problem.
package com.google.ortools.sat.samples;
// [START import]
import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
@@ -59,16 +60,11 @@ public class AssignmentTeamsSat {
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
Literal[][] x = new Literal[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
for (int worker : allWorkers) {
for (int task : allTasks) {
x[worker][task] = model.newBoolVar("x[" + worker + "," + task + "]");
int k = worker * numTasks + task;
xFlat[k] = x[worker][task];
costsFlat[k] = costs[worker][task];
}
}
// [END variables]
@@ -77,43 +73,49 @@ public class AssignmentTeamsSat {
// [START constraints]
// Each worker is assigned to at most one task.
for (int worker : allWorkers) {
IntVar[] vars = new IntVar[numTasks];
List<Literal> tasks = new ArrayList<>();
for (int task : allTasks) {
vars[task] = x[worker][task];
tasks.add(x[worker][task]);
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
model.addAtMostOne(tasks);
}
// Each task is assigned to exactly one worker.
for (int task : allTasks) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
List<Literal> workers = new ArrayList<>();
for (int worker : allWorkers) {
vars[worker] = x[worker][task];
workers.add(x[worker][task]);
}
model.addEquality(LinearExpr.sum(vars), 1);
model.addExactlyOne(workers);
}
// Each team takes at most two tasks.
List<IntVar> team1Tasks = new ArrayList<>();
LinearExprBuilder team1Tasks = LinearExpr.newBuilder();
for (int worker : team1) {
for (int task : allTasks) {
team1Tasks.add(x[worker][task]);
}
}
model.addLessOrEqual(LinearExpr.sum(team1Tasks.toArray(new IntVar[0])), teamMax);
model.addLessOrEqual(team1Tasks.build(), teamMax);
List<IntVar> team2Tasks = new ArrayList<>();
LinearExprBuilder team2Tasks = LinearExpr.newBuilder();
for (int worker : team2) {
for (int task : allTasks) {
team2Tasks.add(x[worker][task]);
}
}
model.addLessOrEqual(LinearExpr.sum(team2Tasks.toArray(new IntVar[0])), teamMax);
model.addLessOrEqual(team2Tasks.build(), teamMax);
// [END constraints]
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int worker : allWorkers) {
for (int task : allTasks) {
obj.addTerm(x[worker][task], costs[worker][task]);
}
}
model.minimize(obj.build());
// [END objective]
// Solve
@@ -129,7 +131,7 @@ public class AssignmentTeamsSat {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int worker : allWorkers) {
for (int task : allTasks) {
if (solver.value(x[worker][task]) == 1) {
if (solver.booleanValue(x[worker][task])) {
System.out.println("Worker " + worker + " assigned to task " + task
+ ". Cost: " + costs[worker][task]);
}

17
ortools/sat/samples/BinPackingProblemSat.java
View File

@@ -19,6 +19,7 @@ import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.LinearExpr;
import com.google.ortools.sat.LinearExprBuilder;
/** Solves a bin packing problem with the CP-SAT solver. */
public class BinPackingProblemSat {
@@ -57,25 +58,21 @@ public class BinPackingProblemSat {
}
// Links load and x.
int[] sizes = new int[numItems];
for (int i = 0; i < numItems; ++i) {
sizes[i] = items[i][0];
}
for (int b = 0; b < numBins; ++b) {
IntVar[] vars = new IntVar[numItems];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int i = 0; i < numItems; ++i) {
vars[i] = x[i][b];
expr.addTerm(x[i][b], items[i][0]);
}
model.addEquality(LinearExpr.scalProd(vars, sizes), load[b]);
model.addEquality(expr.build(), load[b]);
}
// Place all items.
for (int i = 0; i < numItems; ++i) {
IntVar[] vars = new IntVar[numBins];
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int b = 0; b < numBins; ++b) {
vars[b] = x[i][b];
expr.add(x[i][b]);
}
model.addEquality(LinearExpr.sum(vars), items[i][1]);
model.addEquality(expr.build(), items[i][1]);
}
// Links load and slack.

15
ortools/sat/samples/ChannelingSampleSat.java
View File

@@ -30,24 +30,23 @@ public class ChannelingSampleSat {
CpModel model = new CpModel();
// Declare our two primary variables.
IntVar x = model.newIntVar(0, 10, "x");
IntVar y = model.newIntVar(0, 10, "y");
IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")};
// Declare our intermediate boolean variable.
IntVar b = model.newBoolVar("b");
// Implement b == (x >= 5).
model.addGreaterOrEqual(x, 5).onlyEnforceIf(b);
model.addLessOrEqual(x, 4).onlyEnforceIf(b.not());
model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b);
model.addLessOrEqual(vars[0], 4).onlyEnforceIf(b.not());
// Create our two half-reified constraints.
// First, b implies (y == 10 - x).
model.addEquality(LinearExpr.sum(new IntVar[] {x, y}), 10).onlyEnforceIf(b);
model.addEquality(LinearExpr.sum(vars), 10).onlyEnforceIf(b);
// Second, not(b) implies y == 0.
model.addEquality(y, 0).onlyEnforceIf(b.not());
model.addEquality(vars[1], 0).onlyEnforceIf(b.not());
// Search for x values in increasing order.
model.addDecisionStrategy(new IntVar[] {x},
model.addDecisionStrategy(new IntVar[] {vars[0]},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
@@ -75,6 +74,6 @@ public class ChannelingSampleSat {
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, y, b}));
}.init(new IntVar[] {vars[0], vars[1], b}));
}
}

8
ortools/sat/samples/CpSatExample.java
View File

@@ -44,13 +44,13 @@ public final class CpSatExample {
// Create the constraints.
// [START constraints]
model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {2, 7, 3}), 50);
model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {3, -5, 7}), 45);
model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {5, 2, -6}), 37);
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);
// [END constraints]
// [START objective]
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {2, 2, 3}));
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {2, 2, 3}));
// [END objective]
// Create a solver and solve the model.

29
ortools/sat/samples/EarlinessTardinessCostSampleSat.java
View File

@@ -46,21 +46,20 @@ public class EarlinessTardinessCostSampleSat {
long largeConstant = 1000;
IntVar expr = model.newIntVar(0, largeConstant, "expr");
// First segment: s1 == earlinessCost * (earlinessDate - x).
IntVar s1 = model.newIntVar(-largeConstant, largeConstant, "s1");
model.addEquality(LinearExpr.scalProd(new IntVar[] {s1, x}, new long[] {1, earlinessCost}),
earlinessCost * earlinessDate);
// Second segment.
IntVar s2 = model.newConstant(0);
// Third segment: s3 == latenessCost * (x - latenessDate).
IntVar s3 = model.newIntVar(-largeConstant, largeConstant, "s3");
model.addEquality(LinearExpr.scalProd(new IntVar[] {s3, x}, new long[] {1, -latenessCost}),
-latenessCost * latenessDate);
// Link together expr and x through s1, s2, and s3.
model.addMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Link together expr and the 3 segment.
// First segment: y == earlinessCost * (earlinessDate - x).
// Second segment: y = 0
// Third segment: y == latenessCost * (x - latenessDate).
model.addMaxEquality(expr,
new LinearExpr[] {LinearExpr.newBuilder()
.addTerm(x, -earlinessCost)
.add(earlinessCost * earlinessDate)
.build(),
LinearExpr.constant(0),
LinearExpr.newBuilder()
.addTerm(x, latenessCost)
.add(-latenessCost * latenessDate)
.build()});
// Search for x values in increasing order.
model.addDecisionStrategy(new IntVar[] {x},

4
ortools/sat/samples/IntervalSampleSat.java
View File

@@ -29,8 +29,8 @@ public class IntervalSampleSat {
// An interval can be created from three affine expressions.
IntVar startVar = model.newIntVar(0, horizon, "start");
IntVar endVar = model.newIntVar(0, horizon, "end");
IntervalVar intervalVar = model.newIntervalVar(
startVar, LinearExpr.constant(10), LinearExpr.affine(endVar, 1, 2), "interval");
IntervalVar intervalVar = model.newIntervalVar(startVar, LinearExpr.constant(10),
LinearExpr.newBuilder().add(endVar).add(2).build(), "interval");
System.out.println(intervalVar);
// If the size is fixed, a simpler version uses the start expression and the size.

6
ortools/sat/samples/MinimalJobshopSat.java
View File

@@ -108,7 +108,7 @@ public class MinimalJobshopSat {
// Create and add disjunctive constraints.
for (int machine : allMachines) {
List<IntervalVar> list = machineToIntervals.get(machine);
model.addNoOverlap(list.toArray(new IntervalVar[0]));
model.addNoOverlap(list);
}
// Precedences inside a job.
@@ -125,13 +125,13 @@ public class MinimalJobshopSat {
// [START objective]
// Makespan objective.
IntVar objVar = model.newIntVar(0, horizon, "makespan");
List<IntVar> ends = new ArrayList<>();
List<LinearExpr> ends = new ArrayList<>();
for (int jobID = 0; jobID < allJobs.size(); ++jobID) {
List<Task> job = allJobs.get(jobID);
List<Integer> key = Arrays.asList(jobID, job.size() - 1);
ends.add(allTasks.get(key).end);
}
model.addMaxEquality(objVar, ends.toArray(new IntVar[0]));
model.addMaxEquality(objVar, ends);
model.minimize(objVar);
// [END objective]

30
ortools/sat/samples/MultipleKnapsackSat.java
View File

@@ -19,8 +19,11 @@ import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
@@ -46,7 +49,7 @@ public class MultipleKnapsackSat {
// Variables.
// [START variables]
IntVar[][] x = new IntVar[numItems][numBins];
Literal[][] x = new Literal[numItems][numBins];
for (int i : allItems) {
for (int b : allBins) {
x[i][b] = model.newBoolVar("x_" + i + "_" + b);
@@ -58,36 +61,33 @@ public class MultipleKnapsackSat {
// [START constraints]
// Each item is assigned to at most one bin.
for (int i : allItems) {
IntVar[] vars = new IntVar[numBins];
List<Literal> bins = new ArrayList<>();
for (int b : allBins) {
vars[b] = x[i][b];
bins.add(x[i][b]);
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
model.addAtMostOne(bins);
}
// The amount packed in each bin cannot exceed its capacity.
for (int b : allBins) {
IntVar[] vars = new IntVar[numItems];
LinearExprBuilder load = LinearExpr.newBuilder();
for (int i : allItems) {
vars[i] = x[i][b];
load.addTerm(x[i][b], weights[i]);
}
model.addLessOrEqual(LinearExpr.scalProd(vars, weights), binCapacities[b]);
model.addLessOrEqual(load.build(), binCapacities[b]);
}
// [END constraints]
// Objective.
// [START objective]
// Maximize total value of packed items.
IntVar[] objectiveVars = new IntVar[numItems * numBins];
int[] objectiveValues = new int[numItems * numBins];
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int i : allItems) {
for (int b : allBins) {
int k = i * numBins + b;
objectiveVars[k] = x[i][b];
objectiveValues[k] = values[i];
obj.addTerm(x[i][b], values[i]);
}
}
model.maximize(LinearExpr.scalProd(objectiveVars, objectiveValues));
model.maximize(obj.build());
// [END objective]
// [START solve]
@@ -105,7 +105,7 @@ public class MultipleKnapsackSat {
long binValue = 0;
System.out.println("Bin " + b);
for (int i : allItems) {
if (solver.value(x[i][b]) > 0) {
if (solver.booleanValue(x[i][b])) {
System.out.println("Item " + i + " weight: " + weights[i] + " value: " + values[i]);
binWeight += weights[i];
binValue += values[i];

4
ortools/sat/samples/NQueensSat.java
View File

@@ -84,8 +84,8 @@ public final class NQueensSat {
LinearExpr[] diag1 = new LinearExpr[boardSize];
LinearExpr[] diag2 = new LinearExpr[boardSize];
for (int i = 0; i < boardSize; ++i) {
diag1[i] = LinearExpr.affine(queens[i], /*coefficient=*/1, /*offset=*/i);
diag2[i] = LinearExpr.affine(queens[i], /*coefficient=*/1, /*offset=*/-i);
diag1[i] = LinearExpr.newBuilder().add(queens[i]).add(i).build();
diag2[i] = LinearExpr.newBuilder().add(queens[i]).add(-i).build();
}
model.addAllDifferent(diag1);
model.addAllDifferent(diag2);

14
ortools/sat/samples/NoOverlapSampleSat.java
View File

@@ -35,20 +35,17 @@ public class NoOverlapSampleSat {
// Task 0, duration 2.
IntVar start0 = model.newIntVar(0, horizon, "start0");
int duration0 = 2;
IntVar end0 = model.newIntVar(0, horizon, "end0");
IntervalVar task0 = model.newIntervalVar(start0, LinearExpr.constant(duration0), end0, "task0");
IntervalVar task0 = model.newFixedSizeIntervalVar(start0, duration0, "task0");
// Task 1, duration 4.
IntVar start1 = model.newIntVar(0, horizon, "start1");
int duration1 = 4;
IntVar end1 = model.newIntVar(0, horizon, "end1");
IntervalVar task1 = model.newIntervalVar(start1, LinearExpr.constant(duration1), end1, "task1");
IntervalVar task1 = model.newFixedSizeIntervalVar(start1, duration1, "task1");
// Task 2, duration 3.
IntVar start2 = model.newIntVar(0, horizon, "start2");
int duration2 = 3;
IntVar end2 = model.newIntVar(0, horizon, "end2");
IntervalVar task2 = model.newIntervalVar(start2, LinearExpr.constant(duration2), end2, "task2");
IntervalVar task2 = model.newFixedSizeIntervalVar(start2, duration2, "task2");
// Weekends.
IntervalVar weekend0 = model.newFixedInterval(5, 2, "weekend0");
@@ -62,7 +59,10 @@ public class NoOverlapSampleSat {
// Makespan objective.
IntVar obj = model.newIntVar(0, horizon, "makespan");
model.addMaxEquality(obj, new IntVar[] {end0, end1, end2});
model.addMaxEquality(obj,
new LinearExpr[] {LinearExpr.newBuilder().add(start0).add(duration0).build(),
LinearExpr.newBuilder().add(start1).add(duration1).build(),
LinearExpr.newBuilder().add(start2).add(duration2).build()});
model.minimize(obj);
// Creates a solver and solves the model.

32
ortools/sat/samples/NursesSat.java
View File

@@ -19,8 +19,11 @@ import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
@@ -46,7 +49,7 @@ public class NursesSat {
// Creates shift variables.
// shifts[(n, d, s)]: nurse 'n' works shift 's' on day 'd'.
// [START variables]
IntVar[][][] shifts = new IntVar[numNurses][numDays][numShifts];
Literal[][][] shifts = new Literal[numNurses][numDays][numShifts];
for (int n : allNurses) {
for (int d : allDays) {
for (int s : allShifts) {
@@ -60,11 +63,11 @@ public class NursesSat {
// [START exactly_one_nurse]
for (int d : allDays) {
for (int s : allShifts) {
IntVar[] x = new IntVar[numNurses];
List<Literal> nurses = new ArrayList<>();
for (int n : allNurses) {
x[n] = shifts[n][d][s];
nurses.add(shifts[n][d][s]);
}
model.addEquality(LinearExpr.sum(x), 1);
model.addExactlyOne(nurses);
}
}
// [END exactly_one_nurse]
@@ -73,11 +76,11 @@ public class NursesSat {
// [START at_most_one_shift]
for (int n : allNurses) {
for (int d : allDays) {
IntVar[] x = new IntVar[numShifts];
List<Literal> work = new ArrayList<>();
for (int s : allShifts) {
x[s] = shifts[n][d][s];
work.add(shifts[n][d][s]);
}
model.addLessOrEqual(LinearExpr.sum(x), 1);
model.addAtMostOne(work);
}
}
// [END at_most_one_shift]
@@ -95,14 +98,13 @@ public class NursesSat {
maxShiftsPerNurse = minShiftsPerNurse + 1;
}
for (int n : allNurses) {
IntVar[] numShiftsWorked = new IntVar[numDays * numShifts];
LinearExprBuilder numShiftsWorked = LinearExpr.newBuilder();
for (int d : allDays) {
for (int s : allShifts) {
numShiftsWorked[d * numShifts + s] = shifts[n][d][s];
numShiftsWorked.add(shifts[n][d][s]);
}
}
model.addLinearConstraint(
LinearExpr.sum(numShiftsWorked), minShiftsPerNurse, maxShiftsPerNurse);
model.addLinearConstraint(numShiftsWorked.build(), minShiftsPerNurse, maxShiftsPerNurse);
}
// [END assign_nurses_evenly]
@@ -118,7 +120,7 @@ public class NursesSat {
final int solutionLimit = 5;
class VarArraySolutionPrinterWithLimit extends CpSolverSolutionCallback {
public VarArraySolutionPrinterWithLimit(
int[] allNurses, int[] allDays, int[] allShifts, IntVar[][][] shifts, int limit) {
int[] allNurses, int[] allDays, int[] allShifts, Literal[][][] shifts, int limit) {
solutionCount = 0;
this.allNurses = allNurses;
this.allDays = allDays;
@@ -135,7 +137,7 @@ public class NursesSat {
for (int n : allNurses) {
boolean isWorking = false;
for (int s : allShifts) {
if (value(shifts[n][d][s]) == 1L) {
if (booleanValue(shifts[n][d][s])) {
isWorking = true;
System.out.printf(" Nurse %d work shift %d%n", n, s);
}
@@ -160,7 +162,7 @@ public class NursesSat {
private final int[] allNurses;
private final int[] allDays;
private final int[] allShifts;
private final IntVar[][][] shifts;
private final Literal[][][] shifts;
private final int solutionLimit;
}

4
ortools/sat/samples/OptionalIntervalSampleSat.java
View File

@@ -31,8 +31,8 @@ public class OptionalIntervalSampleSat {
IntVar startVar = model.newIntVar(0, horizon, "start");
IntVar endVar = model.newIntVar(0, horizon, "end");
Literal presence = model.newBoolVar("presence");
IntervalVar intervalVar = model.newOptionalIntervalVar(
startVar, LinearExpr.constant(10), LinearExpr.affine(endVar, 1, 2), presence, "interval");
IntervalVar intervalVar = model.newOptionalIntervalVar(startVar, LinearExpr.constant(10),
LinearExpr.newBuilder().add(endVar).add(2).build(), presence, "interval");
System.out.println(intervalVar);
// If the size is fixed, a simpler version uses the start expression, the size and the literal.

4
ortools/sat/samples/RabbitsAndPheasantsSat.java
View File

@@ -33,9 +33,9 @@ public class RabbitsAndPheasantsSat {
IntVar r = model.newIntVar(0, 100, "r");
IntVar p = model.newIntVar(0, 100, "p");
// 20 heads.
model.addEquality(LinearExpr.sum(new IntVar[] {r, p}), 20);
model.addEquality(LinearExpr.newBuilder().add(r).add(p).build(), 20);
// 56 legs.
model.addEquality(LinearExpr.scalProd(new IntVar[] {r, p}, new long[] {4, 2}), 56);
model.addEquality(LinearExpr.newBuilder().addTerm(r, 4).addTerm(p, 2).build(), 56);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();

33
ortools/sat/samples/RankingSampleSat.java
View File

@@ -20,6 +20,7 @@ import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.IntervalVar;
import com.google.ortools.sat.LinearExpr;
import com.google.ortools.sat.LinearExprBuilder;
import com.google.ortools.sat.Literal;
import java.util.ArrayList;
import java.util.List;
@@ -47,7 +48,7 @@ public class RankingSampleSat {
IntVar 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.addLessOrEqualWithOffset(starts[i], starts[j], 1).onlyEnforceIf(prec);
model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec);
}
}
}
@@ -69,7 +70,7 @@ public class RankingSampleSat {
// The following boolOr will enforce that for any two intervals:
// i precedes j or j precedes i or at least one interval is not
// performed.
model.addBoolOr(list.toArray(new Literal[0]));
model.addBoolOr(list);
// For efficiency, we add a redundant constraint declaring that only one of i precedes j and
// j precedes i are true. This will speed up the solve because the reason of this
// propagation is shorter that using interval bounds is true.
@@ -80,16 +81,13 @@ public class RankingSampleSat {
// Links precedences and ranks.
for (int i = 0; i < numTasks; ++i) {
IntVar[] vars = new IntVar[numTasks + 1];
int[] coefs = new int[numTasks + 1];
for (int j = 0; j < numTasks; ++j) {
vars[j] = (IntVar) precedences[j][i];
coefs[j] = 1;
}
vars[numTasks] = ranks[i];
coefs[numTasks] = -1;
// ranks == sum(precedences) - 1;
model.addEquality(LinearExpr.scalProd(vars, coefs), 1);
LinearExprBuilder expr = LinearExpr.newBuilder();
for (int j = 0; j < numTasks; ++j) {
expr.add(precedences[j][i]);
}
expr.add(-1);
model.addEquality(ranks[i], expr.build());
}
}
@@ -133,7 +131,7 @@ public class RankingSampleSat {
rankTasks(model, starts, presences, ranks);
// Adds a constraint on ranks (ranks[0] < ranks[1]).
model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
model.addLessThan(ranks[0], ranks[1]);
// Creates makespan variable.
IntVar makespan = model.newIntVar(0, horizon, "makespan");
@@ -147,15 +145,12 @@ public class RankingSampleSat {
//
// On this problem, as the fixed cost is less that the duration of the last interval, the solver
// will not perform the last interval.
IntVar[] objectiveVars = new IntVar[numTasks + 1];
int[] objectiveCoefs = new int[numTasks + 1];
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int t = 0; t < numTasks; ++t) {
objectiveVars[t] = (IntVar) presences[t];
objectiveCoefs[t] = -7;
obj.addTerm(presences[t], -7);
}
objectiveVars[numTasks] = makespan;
objectiveCoefs[numTasks] = 2;
model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
obj.addTerm(makespan, 2);
model.minimize(obj.build());
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();

36
ortools/sat/samples/ScheduleRequestsSat.java
View File

@@ -18,8 +18,11 @@ import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
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;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.IntStream;
// [END import]
@@ -93,7 +96,7 @@ public class ScheduleRequestsSat {
// Creates shift variables.
// shifts[(n, d, s)]: nurse 'n' works shift 's' on day 'd'.
// [START variables]
IntVar[][][] shifts = new IntVar[numNurses][numDays][numShifts];
Literal[][][] shifts = new Literal[numNurses][numDays][numShifts];
for (int n : allNurses) {
for (int d : allDays) {
for (int s : allShifts) {
@@ -107,11 +110,11 @@ public class ScheduleRequestsSat {
// [START exactly_one_nurse]
for (int d : allDays) {
for (int s : allShifts) {
IntVar[] x = new IntVar[numNurses];
List<Literal> nurses = new ArrayList<>();
for (int n : allNurses) {
x[n] = shifts[n][d][s];
nurses.add(shifts[n][d][s]);
}
model.addEquality(LinearExpr.sum(x), 1);
model.addExactlyOne(nurses);
}
}
// [END exactly_one_nurse]
@@ -120,11 +123,11 @@ public class ScheduleRequestsSat {
// [START at_most_one_shift]
for (int n : allNurses) {
for (int d : allDays) {
IntVar[] x = new IntVar[numShifts];
List<Literal> work = new ArrayList<>();
for (int s : allShifts) {
x[s] = shifts[n][d][s];
work.add(shifts[n][d][s]);
}
model.addLessOrEqual(LinearExpr.sum(x), 1);
model.addAtMostOne(work);
}
}
// [END at_most_one_shift]
@@ -142,29 +145,26 @@ public class ScheduleRequestsSat {
maxShiftsPerNurse = minShiftsPerNurse + 1;
}
for (int n : allNurses) {
IntVar[] numShiftsWorked = new IntVar[numDays * numShifts];
LinearExprBuilder numShiftsWorked = LinearExpr.newBuilder();
for (int d : allDays) {
for (int s : allShifts) {
numShiftsWorked[d * numShifts + s] = shifts[n][d][s];
numShiftsWorked.add(shifts[n][d][s]);
}
}
model.addLinearConstraint(
LinearExpr.sum(numShiftsWorked), minShiftsPerNurse, maxShiftsPerNurse);
model.addLinearConstraint(numShiftsWorked.build(), minShiftsPerNurse, maxShiftsPerNurse);
}
// [END assign_nurses_evenly]
// [START objective]
IntVar[] flatShifts = new IntVar[numNurses * numDays * numShifts];
int[] flatShiftRequests = new int[numNurses * numDays * numShifts];
LinearExprBuilder obj = LinearExpr.newBuilder();
for (int n : allNurses) {
for (int d : allDays) {
for (int s : allShifts) {
flatShifts[n * numDays * numShifts + d * numShifts + s] = shifts[n][d][s];
flatShiftRequests[n * numDays * numShifts + d * numShifts + s] = shiftRequests[n][d][s];
obj.addTerm(shifts[n][d][s], shiftRequests[n][d][s]);
}
}
}
model.maximize(LinearExpr.scalProd(flatShifts, flatShiftRequests));
model.maximize(obj.build());
// [END objective]
// Creates a solver and solves the model.
@@ -180,7 +180,7 @@ public class ScheduleRequestsSat {
System.out.printf("Day %d%n", d);
for (int n : allNurses) {
for (int s : allShifts) {
if (solver.value(shifts[n][d][s]) == 1L) {
if (solver.booleanValue(shifts[n][d][s])) {
if (shiftRequests[n][d][s] == 1) {
System.out.printf(" Nurse %d works shift %d (requested).%n", n, s);
} else {

2
ortools/sat/samples/SolutionHintingSampleSat.java
View File

@@ -45,7 +45,7 @@ public class SolutionHintingSampleSat {
// [END constraints]
// [START objective]
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new int[] {1, 2, 3}));
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
// [END objective]
// Solution hinting: x <- 1, y <- 2

2
ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java
View File

@@ -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 int[] {1, 2, 3}));
model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
// [END objective]
// Create a solver and solve the model.

15
ortools/sat/samples/assignment_groups_sat.cc
View File

@@ -10,6 +10,7 @@
// 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.
// [START program]
// Solve assignment problem for given group of workers.
// [START import]
@@ -39,11 +40,11 @@ void AssignmentGroups() {
{{17, 39, 103, 64, 61, 92}},
{{101, 45, 83, 59, 92, 27}},
}};
const int num_workers = costs.size();
const int num_workers = static_cast<int>(costs.size());
std::vector<int> all_workers(num_workers);
std::iota(all_workers.begin(), all_workers.end(), 0);
const int num_tasks = costs[0].size();
const int num_tasks = static_cast<int>(costs[0].size());
std::vector<int> all_tasks(num_tasks);
std::iota(all_tasks.begin(), all_tasks.end(), 0);
// [END data]
@@ -98,15 +99,15 @@ void AssignmentGroups() {
// [START constraints]
// Each worker is assigned to at most one task.
for (int worker : all_workers) {
cp_model.AddLessOrEqual(LinearExpr::Sum(x[worker]), 1);
cp_model.AddAtMostOne(x[worker]);
}
// Each task is assigned to exactly one worker.
for (int task : all_tasks) {
LinearExpr task_sum;
std::vector<BoolVar> tasks;
for (int worker : all_workers) {
task_sum.AddTerm(x[worker][task], 1);
tasks.push_back(x[worker][task]);
}
cp_model.AddEquality(task_sum, 1);
cp_model.AddExactlyOne(tasks);
}
// [END constraints]
@@ -122,7 +123,7 @@ void AssignmentGroups() {
for (int worker : all_workers) {
LinearExpr task_sum;
for (int task : all_tasks) {
task_sum.AddTerm(x[worker][task], 1);
task_sum += x[worker][task];
}
cp_model.AddEquality(work[worker], task_sum);
}

33
ortools/sat/samples/assignment_task_sizes_sat.cc
View File

@@ -10,6 +10,7 @@
// 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.
// [START program]
// Solve assignment problem.
// [START import]
@@ -26,22 +27,22 @@ void AssignmentTaskSizes() {
// Data
// [START data]
const std::vector<std::vector<int>> costs = {{
{{90, 76, 75, 70, 50, 74, 12, 68}},
{{35, 85, 55, 65, 48, 101, 70, 83}},
{{125, 95, 90, 105, 59, 120, 36, 73}},
{{45, 110, 95, 115, 104, 83, 37, 71}},
{{60, 105, 80, 75, 59, 62, 93, 88}},
{{45, 65, 110, 95, 47, 31, 81, 34}},
{{38, 51, 107, 41, 69, 99, 115, 48}},
{{47, 85, 57, 71, 92, 77, 109, 36}},
{{39, 63, 97, 49, 118, 56, 92, 61}},
{{47, 101, 71, 60, 88, 109, 52, 90}},
{{90, 76, 75, 70, 50, 74, 12, 68}},
{{35, 85, 55, 65, 48, 101, 70, 83}},
{{125, 95, 90, 105, 59, 120, 36, 73}},
{{45, 110, 95, 115, 104, 83, 37, 71}},
{{60, 105, 80, 75, 59, 62, 93, 88}},
{{45, 65, 110, 95, 47, 31, 81, 34}},
{{38, 51, 107, 41, 69, 99, 115, 48}},
{{47, 85, 57, 71, 92, 77, 109, 36}},
{{39, 63, 97, 49, 118, 56, 92, 61}},
{{47, 101, 71, 60, 88, 109, 52, 90}},
}};
const int num_workers = costs.size();
const int num_workers = static_cast<int>(costs.size());
std::vector<int> all_workers(num_workers);
std::iota(all_workers.begin(), all_workers.end(), 0);
const int num_tasks = costs[0].size();
const int num_tasks = static_cast<int>(costs[0].size());
std::vector<int> all_tasks(num_tasks);
std::iota(all_tasks.begin(), all_tasks.end(), 0);
@@ -75,17 +76,17 @@ void AssignmentTaskSizes() {
for (int worker : all_workers) {
LinearExpr task_sum;
for (int task : all_tasks) {
task_sum.AddTerm(x[worker][task], task_sizes[task]);
task_sum += x[worker][task] * task_sizes[task];
}
cp_model.AddLessOrEqual(task_sum, total_size_max);
}
// Each task is assigned to exactly one worker.
for (int task : all_tasks) {
LinearExpr task_sum;
std::vector<BoolVar> tasks;
for (int worker : all_workers) {
task_sum.AddTerm(x[worker][task], 1);
tasks.push_back(x[worker][task]);
}
cp_model.AddEquality(task_sum, 1);
cp_model.AddExactlyOne(tasks);
}
// [END constraints]

41
ortools/sat/samples/assignment_teams_sat.cc
View File

@@ -10,6 +10,7 @@
// 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.
// [START program]
// Solve a simple assignment problem.
// [START import]
@@ -27,23 +28,23 @@ void AssignmentTeamsSat() {
// Data
// [START data]
const std::vector<std::vector<int>> costs = {{
{{90, 76, 75, 70}},
{{35, 85, 55, 65}},
{{125, 95, 90, 105}},
{{45, 110, 95, 115}},
{{60, 105, 80, 75}},
{{45, 65, 110, 95}},
{{90, 76, 75, 70}},
{{35, 85, 55, 65}},
{{125, 95, 90, 105}},
{{45, 110, 95, 115}},
{{60, 105, 80, 75}},
{{45, 65, 110, 95}},
}};
const int num_workers = costs.size();
const int num_workers = static_cast<int>(costs.size());
std::vector<int> all_workers(num_workers);
std::iota(all_workers.begin(), all_workers.end(), 0);
const int num_tasks = costs[0].size();
const int num_tasks = static_cast<int>(costs[0].size());
std::vector<int> all_tasks(num_tasks);
std::iota(all_tasks.begin(), all_tasks.end(), 0);
const std::vector<int64_t> team1 = {{ 0, 2, 4 }};
const std::vector<int64_t> team2 = {{ 1, 3, 5 }};
const std::vector<int> team1 = {{0, 2, 4}};
const std::vector<int> team2 = {{1, 3, 5}};
// Maximum total of tasks for any team
const int team_max = 2;
// [END data]
@@ -71,31 +72,31 @@ void AssignmentTeamsSat() {
// [START constraints]
// Each worker is assigned to at most one task.
for (int worker : all_workers) {
cp_model.AddLessOrEqual(LinearExpr::Sum(x[worker]), 1);
cp_model.AddAtMostOne(x[worker]);
}
// Each task is assigned to exactly one worker.
for (int task : all_tasks) {
LinearExpr task_sum;
std::vector<BoolVar> tasks;
for (int worker : all_workers) {
task_sum.AddTerm(x[worker][task], 1);
tasks.push_back(x[worker][task]);
}
cp_model.AddEquality(task_sum, 1);
cp_model.AddExactlyOne(tasks);
}
// Each team takes at most two tasks.
LinearExpr team1_tasks;
for (int worker : team1) {
for (int task : all_tasks) {
team1_tasks.AddTerm(x[worker][task], 1);
}
for (int task : all_tasks) {
team1_tasks += x[worker][task];
}
}
cp_model.AddLessOrEqual(team1_tasks, team_max);
LinearExpr team2_tasks;
for (int worker : team2) {
for (int task : all_tasks) {
team2_tasks.AddTerm(x[worker][task], 1);
}
for (int task : all_tasks) {
team2_tasks += x[worker][task];
}
}
cp_model.AddLessOrEqual(team2_tasks, team_max);
// [END constraints]