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

polish sat samples

Browse Source
This commit is contained in:
Laurent Perron
2021-02-15 12:26:37 +01:00
parent 9d7acd602e
commit a7570d1ae6
8 changed files with 253 additions and 215 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -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() {}

20
ortools/sat/samples/AssumptionsSampleSat.java
View File

@@ -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]

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

@@ -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() {}

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

@@ -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
*
* <ul>
* <li>rank[i] == -1 iff interval[i] is not active.
* <li>rank[i] == number of active intervals that precede interval[i].
* <li>rank[i] == -1 iff interval[i] is not active.
* <li>rank[i] == number of active intervals that precede interval[i].
* </ul>
*/
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");
}
}
}

1
ortools/sat/samples/assignment_sat.cc
View File

@@ -108,3 +108,4 @@ int main(int argc, char** argv) {
operations_research::sat::IntegerProgrammingExample();
return EXIT_SUCCESS;
}
// [END program]

8
ortools/sat/samples/assignment_sat.py
View File

@@ -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]

22
ortools/sat/samples/assumptions_sample_sat.cc
View File

@@ -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]

17
ortools/sat/samples/assumptions_sample_sat.py
View File

@@ -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]