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

natural API for Cp_SAT C++

Browse Source
This commit is contained in:
Laurent Perron
2021-12-09 15:29:49 +01:00
parent 0bf387c3bc
commit 6ae332569b
40 changed files with 2423 additions and 2235 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
examples/cpp/costas_array_sat.cc
View File

@@ -110,8 +110,7 @@ void CostasHard(const int dim) {
for (int j = 0; j < dim - i; ++j) {
IntVar diff = cp_model.NewIntVar(difference_domain);
subset.push_back(diff);
cp_model.AddEquality(
diff, LinearExpr::ScalProd({vars[j + i], vars[j]}, {1, -1}));
cp_model.AddEquality(diff, vars[j + i] - vars[j]);
}
cp_model.AddAllDifferent(subset);
@@ -255,10 +254,8 @@ void CostasBoolSoft(const int dim) {
cp_model.NewIntVar(Domain(0, positive_diffs.size()));
const IntVar neg_var =
cp_model.NewIntVar(Domain(0, negative_diffs.size()));
cp_model.AddGreaterOrEqual(
pos_var, LinearExpr::Sum(positive_diffs).AddConstant(-1));
cp_model.AddGreaterOrEqual(
neg_var, LinearExpr::Sum(negative_diffs).AddConstant(-1));
cp_model.AddGreaterOrEqual(pos_var, LinearExpr::Sum(positive_diffs) - 1);
cp_model.AddGreaterOrEqual(neg_var, LinearExpr::Sum(negative_diffs) - 1);
all_violations.push_back(pos_var);
all_violations.push_back(neg_var);
}

22
examples/cpp/cryptarithm_sat.cc
View File

@@ -46,24 +46,20 @@ void SendMoreMoney() {
// Force all letters to take on different values.
cp_model.AddAllDifferent({s, e, n, d, m, o, r, y});
// Column 0: Force c0 == m.
// Column 0:
cp_model.AddEquality(c0, m);
// Column 1: Force c1 + s + m + o == 10*c0.
cp_model.AddEquality(LinearExpr::Sum({c1, s, m, o}),
LinearExpr::ScalProd({c0}, {10}));
// Column 1:
cp_model.AddEquality(c1 + s + m + o, 10 * c0);
// Column 2: Force c2 + e + o == n + 10*c1.
cp_model.AddEquality(LinearExpr::Sum({c2, e, o}),
LinearExpr::ScalProd({n, c1}, {1, 10}));
// Column 2:
cp_model.AddEquality(c2 + e + o, n + 10 * c1);
// Column 3: Force c3 + n + r == e + 10*c2.
cp_model.AddEquality(LinearExpr::Sum({c3, n, r}),
LinearExpr::ScalProd({e, c2}, {1, 10}));
// Column 3:
cp_model.AddEquality(c3 + n + r, e + 10 * c2);
// Column 4: Force d + e == y + 10*c3.
cp_model.AddEquality(LinearExpr::Sum({d, e}),
LinearExpr::ScalProd({y, c3}, {1, 10}));
// Column 4:
cp_model.AddEquality(d + e, y + 10 * c3);
// Declare the model, solve it, and display the results.
const CpSolverResponse response = Solve(cp_model.Build());

2
examples/cpp/golomb_sat.cc
View File

@@ -67,7 +67,7 @@ void GolombRuler(int size) {
for (int i = 0; i < size; ++i) {
for (int j = i + 1; j < size; ++j) {
const IntVar diff = cp_model.NewIntVar(domain);
cp_model.AddEquality(LinearExpr::Sum({diff, ticks[i]}), ticks[j]);
cp_model.AddEquality(diff, ticks[j] - ticks[i]);
diffs.push_back(diff);
}
}

38
examples/cpp/jobshop_sat.cc
View File

@@ -302,9 +302,10 @@ void AddAlternativeTaskDurationRelaxation(
// end == start + min_duration +
// sum(shifted_duration[i] * presence_literals[i])
cp_model.AddEquality(
LinearExpr::ScalProd({tasks[t].end, tasks[t].start}, {1, -1}),
LinearExpr::ScalProd(presence_literals, shifted_durations)
.AddConstant(min_duration));
tasks[t].end,
tasks[t].start +
LinearExpr::ScalProd(presence_literals, shifted_durations) +
min_duration);
}
}
}
@@ -432,18 +433,18 @@ void CreateMachines(
// Note that we use the start + duration + transition as this is more
// precise than the non-propagated end.
cp_model
.AddLessOrEqual(tail.interval.StartExpr().AddConstant(
tail.fixed_duration + transition),
head.interval.StartExpr())
.AddLessOrEqual(
tail.interval.StartExpr() + tail.fixed_duration + transition,
head.interval.StartExpr())
.OnlyEnforceIf(lit);
}
}
// Add a linear equation to define the size of the tail interval.
if (absl::GetFlag(FLAGS_use_variable_duration_to_encode_transition)) {
cp_model.AddEquality(tail.interval.SizeExpr(),
LinearExpr::ScalProd(literals, transitions)
.AddConstant(tail.fixed_duration));
cp_model.AddEquality(
tail.interval.SizeExpr(),
LinearExpr::ScalProd(literals, transitions) + tail.fixed_duration);
}
}
LOG(INFO) << "Machine " << m
@@ -493,8 +494,7 @@ void CreateObjective(
objective_coeffs.push_back(lateness_penalty);
} else {
const IntVar lateness_var = cp_model.NewIntVar(Domain(0, horizon));
cp_model.AddMaxEquality(lateness_var,
{0, job_end.AddConstant(-due_date)});
cp_model.AddMaxEquality(lateness_var, {0, job_end - due_date});
objective_vars.push_back(lateness_var);
objective_coeffs.push_back(lateness_penalty);
}
@@ -508,9 +508,7 @@ void CreateObjective(
if (due_date > 0) {
const IntVar earliness_var = cp_model.NewIntVar(Domain(0, horizon));
cp_model.AddMaxEquality(
earliness_var,
{0, LinearExpr::Term(job_end, -1).AddConstant(due_date)});
cp_model.AddMaxEquality(earliness_var, {0, due_date - job_end});
objective_vars.push_back(earliness_var);
objective_coeffs.push_back(earliness_penalty);
}
@@ -531,11 +529,11 @@ void CreateObjective(
problem.scaling_factor().value());
}
cp_model.Minimize(
DoubleLinearExpr::ScalProd(objective_vars, double_objective_coeffs)
.AddConstant(objective_offset));
DoubleLinearExpr::ScalProd(objective_vars, double_objective_coeffs) +
static_cast<double>(objective_offset));
} else {
cp_model.Minimize(LinearExpr::ScalProd(objective_vars, objective_coeffs)
.AddConstant(objective_offset));
cp_model.Minimize(LinearExpr::ScalProd(objective_vars, objective_coeffs) +
objective_offset);
}
}
@@ -627,7 +625,7 @@ void AddMakespanRedundantConstraints(
}
}
cp_model.AddLessOrEqual(LinearExpr::Sum(all_task_durations),
LinearExpr::Term(makespan, num_machines));
makespan * num_machines);
}
void DisplayJobStatistics(
@@ -749,7 +747,7 @@ void Solve(const JsspInputProblem& problem) {
const IntVar start =
job_to_tasks[precedence.second_job_index()].front().start;
const IntVar end = job_to_tasks[precedence.first_job_index()].back().end;
cp_model.AddLessOrEqual(end.AddConstant(precedence.min_delay()), start);
cp_model.AddLessOrEqual(end + precedence.min_delay(), start);
}
// Objective.

14
examples/cpp/network_routing_sat.cc
View File

@@ -601,8 +601,7 @@ class NetworkRoutingSolver {
LinearExpr traffic_expr;
for (int i = 0; i < path_vars.size(); ++i) {
sum_of_traffic += demands_array_[i].traffic;
traffic_expr.AddTerm(path_vars[i][arc_index],
demands_array_[i].traffic);
traffic_expr += path_vars[i][arc_index] * demands_array_[i].traffic;
}
const IntVar traffic_var = cp_model.NewIntVar(Domain(0, sum_of_traffic));
traffic_vars[arc_index] = traffic_var;
@@ -611,8 +610,7 @@ class NetworkRoutingSolver {
const int64_t capacity = arc_capacity_[arc_index];
IntVar scaled_traffic =
cp_model.NewIntVar(Domain(0, sum_of_traffic * 1000));
cp_model.AddEquality(LinearExpr::ScalProd({traffic_var}, {1000}),
scaled_traffic);
cp_model.AddEquality(traffic_var * 1000, scaled_traffic);
IntVar normalized_traffic =
cp_model.NewIntVar(Domain(0, sum_of_traffic * 1000 / capacity));
max_normalized_traffic =
@@ -634,12 +632,8 @@ class NetworkRoutingSolver {
cp_model.NewIntVar(Domain(0, max_normalized_traffic));
cp_model.AddMaxEquality(max_usage_cost, normalized_traffic_vars);
LinearExpr objective_expr;
objective_expr.AddVar(max_usage_cost);
for (const BoolVar var : comfortable_traffic_vars) {
objective_expr.AddVar(var);
}
cp_model.Minimize(objective_expr);
cp_model.Minimize(LinearExpr::Sum(comfortable_traffic_vars) +
max_usage_cost);
Model model;
if (!absl::GetFlag(FLAGS_params).empty()) {

5
examples/cpp/sports_scheduling_sat.cc
View File

@@ -97,8 +97,7 @@ void OpponentModel(int num_teams) {
// Link opponent, home_away, and signed_opponent.
builder.AddEquality(opp, signed_opp).OnlyEnforceIf(Not(home));
builder.AddEquality(LinearExpr(opp).AddConstant(num_teams), signed_opp)
.OnlyEnforceIf(home);
builder.AddEquality(opp + num_teams, signed_opp).OnlyEnforceIf(home);
}
}
@@ -118,7 +117,7 @@ void OpponentModel(int num_teams) {
IntVar second_home = builder.NewBoolVar();
builder.AddVariableElement(day_opponents[first_team], day_home_aways,
second_home);
builder.AddEquality(LinearExpr::Sum({first_home, second_home}), 1);
builder.AddEquality(first_home + second_home, 1);
}
builder.AddEquality(LinearExpr::Sum(day_home_aways), num_teams / 2);

2
examples/cpp/weighted_tardiness_sat.cc
View File

@@ -107,7 +107,7 @@ void Solve(const std::vector<int64_t>& durations,
// tardiness_vars >= end - due_date
cp_model.AddGreaterOrEqual(tardiness_vars[i],
task_ends[i].AddConstant(-due_dates[i]));
task_ends[i] - due_dates[i]);
}
}