From a7570d1ae64eef2e69b952cb8a8b82e85fcf390f Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 15 Feb 2021 12:26:37 +0100 Subject: [PATCH] polish sat samples --- ortools/sat/samples/AssignmentSat.java | 130 +++++++------- ortools/sat/samples/AssumptionsSampleSat.java | 20 ++- ortools/sat/samples/MultipleKnapsackSat.java | 112 +++++++------ ortools/sat/samples/RankingSampleSat.java | 158 +++++++++--------- ortools/sat/samples/assignment_sat.cc | 1 + ortools/sat/samples/assignment_sat.py | 8 +- ortools/sat/samples/assumptions_sample_sat.cc | 22 ++- ortools/sat/samples/assumptions_sample_sat.py | 17 +- 8 files changed, 253 insertions(+), 215 deletions(-) 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 + * * */ - 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]