diff --git a/ortools/sat/samples/AssignmentSat.java b/ortools/sat/samples/AssignmentSat.java
index 18b6b63a02..22aff14cbc 100644
--- a/ortools/sat/samples/AssignmentSat.java
+++ b/ortools/sat/samples/AssignmentSat.java
@@ -41,75 +41,79 @@ public class AssignmentSat {
// [END data_model]
// Model
- // [START model]
- CpModel model = new CpModel();
- // [END model]
+ try {
+ // [START model]
+ CpModel model = new CpModel();
+ // [END model]
- // 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];
- }
- }
- // [END variables]
-
- // 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];
- }
- model.addLessOrEqual(LinearExpr.sum(vars), 1);
- }
- // 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];
- }
- model.addEquality(LinearExpr.sum(vars), 1);
- }
- // [END constraints]
-
- // Objective
- // [START objective]
- model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
- // [END objective]
-
- // Solve
- // [START solve]
- CpSolver solver = new CpSolver();
- CpSolverStatus status = solver.solve(model);
- // [END solve]
-
- // Print solution.
- // [START print_solution]
- // Check that the problem has a feasible solution.
- if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
- System.out.println("Total cost: " + solver.objectiveValue() + "\n");
+ // 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) {
- if (solver.value(x[i][j]) == 1) {
- System.out.println(
- "Worker " + i + " assigned to task " + j + ". Cost: " + costs[i][j]);
- }
+ x[i][j] = model.newIntVar(0, 1, "");
+ int k = i * numTasks + j;
+ xFlat[k] = x[i][j];
+ costsFlat[k] = costs[i][j];
}
}
- } else {
- System.err.println("No solution found.");
+ // [END variables]
+
+ // 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];
+ }
+ model.addLessOrEqual(LinearExpr.sum(vars), 1);
+ }
+ // 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];
+ }
+ model.addEquality(LinearExpr.sum(vars), 1);
+ }
+ // [END constraints]
+
+ // Objective
+ // [START objective]
+ model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
+ // [END objective]
+
+ // Solve
+ // [START solve]
+ CpSolver solver = new CpSolver();
+ CpSolverStatus status = solver.solve(model);
+ // [END solve]
+
+ // Print solution.
+ // [START print_solution]
+ // Check that the problem has a feasible solution.
+ if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
+ 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) {
+ System.out.println(
+ "Worker " + i + " assigned to task " + j + ". Cost: " + costs[i][j]);
+ }
+ }
+ }
+ } else {
+ System.err.println("No solution found.");
+ }
+ // [END print_solution]
+ } catch (Exception e) {
+ System.err.println("Caught " + e + " while building the model");
}
- // [END print_solution]
}
private AssignmentSat() {}
diff --git a/ortools/sat/samples/AssumptionsSampleSat.java b/ortools/sat/samples/AssumptionsSampleSat.java
index 4e06632b95..9e9d7a9ce5 100644
--- a/ortools/sat/samples/AssumptionsSampleSat.java
+++ b/ortools/sat/samples/AssumptionsSampleSat.java
@@ -13,18 +13,18 @@
// [START program]
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.CpSolverSolutionCallback;
+import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
-import com.google.ortools.sat.LinearExpr;
import com.google.ortools.sat.Literal;
+// [END import]
/** Minimal CP-SAT example to showcase assumptions. */
public class AssumptionsSampleSat {
- public static void main(String[] args) throws Exception {
+ public static void main(String[] args) {
Loader.loadNativeLibraries();
// Create the model.
// [START model]
@@ -54,10 +54,18 @@ public class AssumptionsSampleSat {
// Create a solver and solve the model.
// [START solve]
CpSolver solver = new CpSolver();
- solver.solve(model);
- System.out.println(solver.sufficientAssumptionsForInfeasibility());
+ CpSolverStatus status = solver.solve(model);
// [END solve]
+
+ // Print solution.
+ // [START print_solution]
+ // Check that the problem is infeasible.
+ if (status == CpSolverStatus.INFEASIBLE) {
+ System.out.println(solver.sufficientAssumptionsForInfeasibility());
+ }
+ // [END print_solution]
}
+ private AssumptionsSampleSat() {}
}
// [END program]
diff --git a/ortools/sat/samples/MultipleKnapsackSat.java b/ortools/sat/samples/MultipleKnapsackSat.java
index 88ed0bdba3..0a86748b79 100644
--- a/ortools/sat/samples/MultipleKnapsackSat.java
+++ b/ortools/sat/samples/MultipleKnapsackSat.java
@@ -69,68 +69,72 @@ public class MultipleKnapsackSat {
totalValue = totalValue + data.values[i];
}
- // [START model]
- CpModel model = new CpModel();
- // [END model]
+ try {
+ // [START model]
+ CpModel model = new CpModel();
+ // [END model]
- // [START variables]
- IntVar[][] x = new IntVar[data.numItems][data.numBins];
- for (int i = 0; i < data.numItems; ++i) {
- for (int b = 0; b < data.numBins; ++b) {
- x[i][b] = model.newIntVar(0, 1, "x_" + i + "_" + b);
- }
- }
- // Main variables.
- // Load and value variables.
- IntVar[] load = new IntVar[data.numBins];
- IntVar[] value = new IntVar[data.numBins];
- for (int b = 0; b < data.numBins; ++b) {
- load[b] = model.newIntVar(0, data.binCapacities[b], "load_" + b);
- value[b] = model.newIntVar(0, totalValue, "value_" + b);
- }
-
- // Links load and value with x.
- int[] sizes = new int[data.numItems];
- for (int i = 0; i < data.numItems; ++i) {
- sizes[i] = data.items[i];
- }
- for (int b = 0; b < data.numBins; ++b) {
- IntVar[] vars = new IntVar[data.numItems];
+ // [START variables]
+ IntVar[][] x = new IntVar[data.numItems][data.numBins];
for (int i = 0; i < data.numItems; ++i) {
- vars[i] = x[i][b];
+ for (int b = 0; b < data.numBins; ++b) {
+ x[i][b] = model.newIntVar(0, 1, "x_" + i + "_" + b);
+ }
}
- model.addEquality(LinearExpr.scalProd(vars, data.items), load[b]);
- model.addEquality(LinearExpr.scalProd(vars, data.values), value[b]);
- }
- // [END variables]
-
- // [START constraints]
- // Each item can be in at most one bin.
- // Place all items.
- for (int i = 0; i < data.numItems; ++i) {
- IntVar[] vars = new IntVar[data.numBins];
+ // Main variables.
+ // Load and value variables.
+ IntVar[] load = new IntVar[data.numBins];
+ IntVar[] value = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
- vars[b] = x[i][b];
+ load[b] = model.newIntVar(0, data.binCapacities[b], "load_" + b);
+ value[b] = model.newIntVar(0, totalValue, "value_" + b);
}
- model.addLessOrEqual(LinearExpr.sum(vars), 1);
- }
- // [END constraints]
- // Maximize sum of load.
- // [START objective]
- model.maximize(LinearExpr.sum(value));
- // [END objective]
- // [START solve]
- CpSolver solver = new CpSolver();
- CpSolverStatus status = solver.solve(model);
- // [END solve]
+ // Links load and value with x.
+ int[] sizes = new int[data.numItems];
+ for (int i = 0; i < data.numItems; ++i) {
+ sizes[i] = data.items[i];
+ }
+ for (int b = 0; b < data.numBins; ++b) {
+ IntVar[] vars = new IntVar[data.numItems];
+ for (int i = 0; i < data.numItems; ++i) {
+ vars[i] = x[i][b];
+ }
+ model.addEquality(LinearExpr.scalProd(vars, data.items), load[b]);
+ model.addEquality(LinearExpr.scalProd(vars, data.values), value[b]);
+ }
+ // [END variables]
- // [START print_solution]
- System.out.println("Solve status: " + status);
- if (status == CpSolverStatus.OPTIMAL) {
- printSolution(data, solver, x, load, value);
+ // [START constraints]
+ // Each item can be in at most one bin.
+ // Place all items.
+ for (int i = 0; i < data.numItems; ++i) {
+ IntVar[] vars = new IntVar[data.numBins];
+ for (int b = 0; b < data.numBins; ++b) {
+ vars[b] = x[i][b];
+ }
+ model.addLessOrEqual(LinearExpr.sum(vars), 1);
+ }
+ // [END constraints]
+ // Maximize sum of load.
+ // [START objective]
+ model.maximize(LinearExpr.sum(value));
+ // [END objective]
+
+ // [START solve]
+ CpSolver solver = new CpSolver();
+ CpSolverStatus status = solver.solve(model);
+ // [END solve]
+
+ // [START print_solution]
+ System.out.println("Solve status: " + status);
+ if (status == CpSolverStatus.OPTIMAL) {
+ printSolution(data, solver, x, load, value);
+ }
+ // [END print_solution]
+ } catch (Exception e) {
+ System.err.println("Caught " + e + " while building the model");
}
- // [END print_solution]
}
private MultipleKnapsackSat() {}
diff --git a/ortools/sat/samples/RankingSampleSat.java b/ortools/sat/samples/RankingSampleSat.java
index 0ed88a86fb..9a948db43e 100644
--- a/ortools/sat/samples/RankingSampleSat.java
+++ b/ortools/sat/samples/RankingSampleSat.java
@@ -29,12 +29,14 @@ 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) {
+ static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks)
+ throws Exception {
int numTasks = starts.length;
// Creates precedence variables between pairs of intervals.
@@ -95,85 +97,91 @@ public class RankingSampleSat {
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
- CpModel model = new CpModel();
- int horizon = 100;
- int numTasks = 4;
+ try {
+ CpModel model = new CpModel();
+ int horizon = 100;
+ int numTasks = 4;
- IntVar[] starts = new IntVar[numTasks];
- IntVar[] ends = new IntVar[numTasks];
- IntervalVar[] intervals = new IntervalVar[numTasks];
- Literal[] presences = new Literal[numTasks];
- IntVar[] ranks = new IntVar[numTasks];
+ IntVar[] starts = new IntVar[numTasks];
+ IntVar[] ends = new IntVar[numTasks];
+ IntervalVar[] intervals = new IntervalVar[numTasks];
+ Literal[] presences = new Literal[numTasks];
+ IntVar[] ranks = new IntVar[numTasks];
- IntVar trueVar = model.newConstant(1);
+ IntVar trueVar = model.newConstant(1);
- // Creates intervals, half of them are optional.
- for (int t = 0; t < numTasks; ++t) {
- starts[t] = model.newIntVar(0, horizon, "start_" + t);
- int duration = t + 1;
- ends[t] = model.newIntVar(0, horizon, "end_" + t);
- if (t < numTasks / 2) {
- intervals[t] = model.newIntervalVar(starts[t], duration, ends[t], "interval_" + t);
- presences[t] = trueVar;
- } else {
- presences[t] = model.newBoolVar("presence_" + t);
- intervals[t] = model.newOptionalIntervalVar(
- starts[t], duration, ends[t], presences[t], "o_interval_" + t);
- }
-
- // The rank will be -1 iff the task is not performed.
- ranks[t] = model.newIntVar(-1, numTasks - 1, "rank_" + t);
- }
-
- // Adds NoOverlap constraint.
- model.addNoOverlap(intervals);
-
- // Adds ranking constraint.
- rankTasks(model, starts, presences, ranks);
-
- // Adds a constraint on ranks (ranks[0] < ranks[1]).
- model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
-
- // Creates makespan variable.
- IntVar makespan = model.newIntVar(0, horizon, "makespan");
- for (int t = 0; t < numTasks; ++t) {
- model.addLessOrEqual(ends[t], makespan).onlyEnforceIf(presences[t]);
- }
- // The objective function is a mix of a fixed gain per task performed, and a fixed cost for each
- // additional day of activity.
- // The solver will balance both cost and gain and minimize makespan * per-day-penalty - number
- // of tasks performed * per-task-gain.
- //
- // 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];
- for (int t = 0; t < numTasks; ++t) {
- objectiveVars[t] = (IntVar) presences[t];
- objectiveCoefs[t] = -7;
- }
- objectiveVars[numTasks] = makespan;
- objectiveCoefs[numTasks] = 2;
- model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
-
- // Creates a solver and solves the model.
- CpSolver solver = new CpSolver();
- CpSolverStatus status = solver.solve(model);
-
- if (status == CpSolverStatus.OPTIMAL) {
- System.out.println("Optimal cost: " + solver.objectiveValue());
- System.out.println("Makespan: " + solver.value(makespan));
+ // Creates intervals, half of them are optional.
for (int t = 0; t < numTasks; ++t) {
- if (solver.booleanValue(presences[t])) {
- System.out.printf("Task %d starts at %d with rank %d%n", t, solver.value(starts[t]),
- solver.value(ranks[t]));
+ starts[t] = model.newIntVar(0, horizon, "start_" + t);
+ int duration = t + 1;
+ ends[t] = model.newIntVar(0, horizon, "end_" + t);
+ if (t < numTasks / 2) {
+ intervals[t] = model.newIntervalVar(starts[t], duration, ends[t], "interval_" + t);
+ presences[t] = trueVar;
} else {
- System.out.printf(
- "Task %d in not performed and ranked at %d%n", t, solver.value(ranks[t]));
+ presences[t] = model.newBoolVar("presence_" + t);
+ intervals[t] = model.newOptionalIntervalVar(
+ starts[t], duration, ends[t], presences[t], "o_interval_" + t);
}
+
+ // The rank will be -1 iff the task is not performed.
+ ranks[t] = model.newIntVar(-1, numTasks - 1, "rank_" + t);
}
- } else {
- System.out.println("Solver exited with nonoptimal status: " + status);
+
+ // Adds NoOverlap constraint.
+ model.addNoOverlap(intervals);
+
+ // Adds ranking constraint.
+ rankTasks(model, starts, presences, ranks);
+
+ // Adds a constraint on ranks (ranks[0] < ranks[1]).
+ model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
+
+ // Creates makespan variable.
+ IntVar makespan = model.newIntVar(0, horizon, "makespan");
+ for (int t = 0; t < numTasks; ++t) {
+ model.addLessOrEqual(ends[t], makespan).onlyEnforceIf(presences[t]);
+ }
+ // The objective function is a mix of a fixed gain per task performed, and a fixed cost for
+ // each
+ // additional day of activity.
+ // The solver will balance both cost and gain and minimize makespan * per-day-penalty - number
+ // of tasks performed * per-task-gain.
+ //
+ // 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];
+ for (int t = 0; t < numTasks; ++t) {
+ objectiveVars[t] = (IntVar) presences[t];
+ objectiveCoefs[t] = -7;
+ }
+ objectiveVars[numTasks] = makespan;
+ objectiveCoefs[numTasks] = 2;
+ model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
+
+ // Creates a solver and solves the model.
+ CpSolver solver = new CpSolver();
+ CpSolverStatus status = solver.solve(model);
+
+ if (status == CpSolverStatus.OPTIMAL) {
+ System.out.println("Optimal cost: " + solver.objectiveValue());
+ System.out.println("Makespan: " + solver.value(makespan));
+ for (int t = 0; t < numTasks; ++t) {
+ if (solver.booleanValue(presences[t])) {
+ System.out.printf("Task %d starts at %d with rank %d%n", t, solver.value(starts[t]),
+ solver.value(ranks[t]));
+ } else {
+ System.out.printf(
+ "Task %d in not performed and ranked at %d%n", t, solver.value(ranks[t]));
+ }
+ }
+ } else {
+ System.out.println("Solver exited with nonoptimal status: " + status);
+ }
+ } catch (Exception e) {
+ System.err.println("Caught " + e + " while building the model");
}
}
}
diff --git a/ortools/sat/samples/assignment_sat.cc b/ortools/sat/samples/assignment_sat.cc
index e5c640b8ec..dca9ca4b19 100644
--- a/ortools/sat/samples/assignment_sat.cc
+++ b/ortools/sat/samples/assignment_sat.cc
@@ -108,3 +108,4 @@ int main(int argc, char** argv) {
operations_research::sat::IntegerProgrammingExample();
return EXIT_SUCCESS;
}
+// [END program]
diff --git a/ortools/sat/samples/assignment_sat.py b/ortools/sat/samples/assignment_sat.py
index 5b3290d3f2..533b0d4638 100644
--- a/ortools/sat/samples/assignment_sat.py
+++ b/ortools/sat/samples/assignment_sat.py
@@ -42,7 +42,7 @@ def main():
for i in range(num_workers):
t = []
for j in range(num_tasks):
- t.append(model.NewBoolVar('x[%i,%i]' % (i, j)))
+ t.append(model.NewBoolVar(f'x[{i},{j}]'))
x.append(t)
# [END variables]
@@ -75,13 +75,13 @@ def main():
# Print solution.
# [START print_solution]
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
- print('Total cost = %i' % solver.ObjectiveValue())
+ print(f'Total cost = {solver.ObjectiveValue()}')
print()
for i in range(num_workers):
for j in range(num_tasks):
if solver.BooleanValue(x[i][j]):
- print('Worker ', i, ' assigned to task ', j, ' Cost = ',
- costs[i][j])
+ print(
+ f'Worker {i} assigned to task {j} Cost = {costs[i][j]}')
else:
print('No solution found.')
# [END print_solution]
diff --git a/ortools/sat/samples/assumptions_sample_sat.cc b/ortools/sat/samples/assumptions_sample_sat.cc
index dd4bdec211..2527213d06 100644
--- a/ortools/sat/samples/assumptions_sample_sat.cc
+++ b/ortools/sat/samples/assumptions_sample_sat.cc
@@ -12,9 +12,10 @@
// limitations under the License.
// [START program]
+// [START import]
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
-
+// [END import]
namespace operations_research {
namespace sat {
@@ -45,19 +46,24 @@ void AssumptionsSampleSat() {
// Solving part.
// [START solve]
const CpSolverResponse response = Solve(cp_model.Build());
- LOG(INFO) << CpSolverResponseStats(response);
- for (const int index : response.sufficient_assumptions_for_infeasibility()) {
- LOG(INFO) << index;
- }
// [END solve]
-}
+ // Print solution.
+ // [START print_solution]
+ LOG(INFO) << CpSolverResponseStats(response);
+ if (response.status() == CpSolverStatus::INFEASIBLE) {
+ for (const int index :
+ response.sufficient_assumptions_for_infeasibility()) {
+ LOG(INFO) << index;
+ }
+ }
+ // [END print_solution]
+}
} // namespace sat
} // namespace operations_research
-int main() {
+int main(int argc, char** argv) {
operations_research::sat::AssumptionsSampleSat();
-
return EXIT_SUCCESS;
}
// [END program]
diff --git a/ortools/sat/samples/assumptions_sample_sat.py b/ortools/sat/samples/assumptions_sample_sat.py
index 95b6cb8c97..fb4b378e43 100644
--- a/ortools/sat/samples/assumptions_sample_sat.py
+++ b/ortools/sat/samples/assumptions_sample_sat.py
@@ -11,12 +11,13 @@
# See the License for the specific language governing permissions and
# limitations under the License.
"""Code sample that solves a model and gets the infeasibility assumptions."""
-
# [START program]
+# [START import]
from ortools.sat.python import cp_model
+# [END import]
-def AssumptionsSampleSat():
+def main():
"""Showcases assumptions."""
# Creates the model.
# [START model]
@@ -49,9 +50,15 @@ def AssumptionsSampleSat():
status = solver.Solve(model)
# [END solve]
- print('Status = %s' % solver.StatusName(status))
- print('SufficientAssumptionsForInfeasibility = %s' % solver.SufficientAssumptionsForInfeasibility())
+ # Print solution.
+ # [START print_solution]
+ print(f'Status = {solver.StatusName(status)}')
+ if status == cp_model.INFEASIBLE:
+ print('SufficientAssumptionsForInfeasibility = '
+ f'{solver.SufficientAssumptionsForInfeasibility()}')
+ # [END print_solution]
-AssumptionsSampleSat()
+if __name__ == '__main__':
+ main()
# [END program]