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

sat based scheduling: no_cycle, disjunctive, precedences + 2 examples: jobshop_sat and weighted_tardiness_sat

Browse Source
This commit is contained in:
Laurent Perron
2016-07-19 14:19:21 -07:00
parent 476c490176
commit 3e158e7656
17 changed files with 7218 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

189
examples/cpp/jobshop_sat.cc Normal file
View File

@@ -0,0 +1,189 @@
// Copyright 2010-2014 Google
// 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.
#include <math.h>
#include <vector>
#include "base/commandlineflags.h"
#include "base/commandlineflags.h"
#include "base/logging.h"
#include "base/timer.h"
#include "google/protobuf/text_format.h"
#include "base/join.h"
#include "base/strutil.h"
#include "cpp/flexible_jobshop.h"
#include "cpp/jobshop.h"
#include "sat/disjunctive.h"
#include "sat/intervals.h"
#include "sat/model.h"
#include "sat/optimization.h"
#include "sat/precedences.h"
#include "sat/sat_solver.h"
DEFINE_string(input, "", "Jobshop data file name.");
DEFINE_string(params, "", "Sat parameters in text proto format.");
namespace {
struct Task {
int id; // dense unique id in [1, num_tasks + 1)
int job; // dense unique id in [0, num_jobs)
// The possible alternative to run this task.
std::vector<int> machines;
std::vector<int> durations;
};
struct MachineTask {
int id; // The task id (note that it is shared between alternative tasks).
int job;
int duration;
// -1 if no alternative or the index of the Boolean variable indicating if
// this alternative was taken.
int alternative_var;
};
} // namespace
namespace operations_research {
namespace sat {
// Solve a flexible/normal JobShop scheduling problem using SAT.
void Solve(const std::vector<std::vector<Task>>& tasks_per_job, int horizon) {
int num_machines = 0;
for (const std::vector<Task>& tasks : tasks_per_job) {
for (const Task& task : tasks) {
for (const int machine : task.machines) {
num_machines = std::max(num_machines, machine + 1);
}
}
}
Model model;
model.Add(NewSatParameters(FLAGS_params));
const IntegerVariable makespan = model.Add(NewIntegerVariable(0, horizon));
std::vector<std::vector<IntervalVariable>> machine_to_intervals(num_machines);
for (const std::vector<Task>& tasks : tasks_per_job) {
IntervalVariable previous_interval = kNoIntervalVariable;
for (const Task& task : tasks) {
const int num_alternatives = task.machines.size();
CHECK_EQ(num_alternatives, task.durations.size());
// Add the "main" task interval. It will englobe all the alternative ones
// if there is many, or be a normal task otherwise.
int min_duration = task.durations[0];
int max_duration = task.durations[0];
for (int i = 0; i < num_alternatives; ++i) {
min_duration = std::min(min_duration, task.durations[i]);
max_duration = std::max(max_duration, task.durations[i]);
}
const IntervalVariable interval =
model.Add(NewIntervalWithVariableSize(min_duration, max_duration));
// Chain the task belonging to the same job.
if (previous_interval != kNoIntervalVariable) {
model.Add(EndBeforeStart(previous_interval, interval));
}
previous_interval = interval;
if (num_alternatives == 1) {
machine_to_intervals[task.machines[0]].push_back(interval);
} else {
std::vector<IntervalVariable> alternatives;
for (int i = 0; i < num_alternatives; ++i) {
const Literal is_present(model.Add(NewBooleanVariable()), true);
const IntervalVariable alternative =
model.Add(NewOptionalInterval(task.durations[i], is_present));
alternatives.push_back(alternative);
machine_to_intervals[task.machines[i]].push_back(alternative);
}
model.Add(IntervalWithAlternatives(interval, alternatives));
}
}
// The makespan will be greater than the end of each job.
model.Add(EndBefore(previous_interval, makespan));
}
// Add all the potential precedences between tasks on the same machine.
for (int m = 0; m < num_machines; ++m) {
model.Add(DisjunctiveWithBooleanPrecedences(machine_to_intervals[m]));
}
LOG(INFO) << "#machines:" << num_machines;
LOG(INFO) << "#jobs:" << tasks_per_job.size();
LOG(INFO) << "#tasks:" << model.Get<IntervalsRepository>()->NumIntervals();
MinimizeIntegerVariableWithLinearScan(
makespan,
/*feasible_solution_observer=*/
[makespan](const Model& model) {
const IntegerTrail* integer_trail = model.Get<IntegerTrail>();
LOG(INFO) << "Makespan " << integer_trail->LowerBound(makespan);
},
&model);
}
} // namespace sat
void LoadAndSolve() {
// Read a flexible/normal job shop problem based on the file extension.
int new_task_id = 0;
int horizon = 0;
std::vector<std::vector<Task>> data;
if (HasSuffixString(FLAGS_input, ".fjs")) {
LOG(INFO) << "Reading flexible jobshop instance '" << FLAGS_input << "'.";
operations_research::FlexibleJobShopData fjs;
fjs.Load(FLAGS_input);
horizon = fjs.horizon();
data.resize(fjs.job_count());
if (fjs.job_count() == 0) {
LOG(FATAL) << "No jobs in '" << FLAGS_input << "'.";
}
for (int i = 0; i < fjs.job_count(); ++i) {
for (const operations_research::FlexibleJobShopData::Task& task :
fjs.TasksOfJob(i)) {
CHECK_EQ(task.machines.size(), task.durations.size());
data[i].push_back(
{new_task_id++, task.job_id, task.machines, task.durations});
}
}
} else {
operations_research::JobShopData jssp;
jssp.Load(FLAGS_input);
horizon = jssp.horizon();
data.resize(jssp.job_count());
if (jssp.job_count() == 0) {
LOG(FATAL) << "No jobs in '" << FLAGS_input << "'.";
}
for (int i = 0; i < jssp.job_count(); ++i) {
for (const operations_research::JobShopData::Task& task :
jssp.TasksOfJob(i)) {
data[i].push_back(
{new_task_id++, task.job_id, {task.machine_id}, {task.duration}});
}
}
}
// Solve it.
operations_research::sat::Solve(data, horizon);
}
} // namespace operations_research
int main(int argc, char** argv) {
gflags::ParseCommandLineFlags( &argc, &argv, true);
if (FLAGS_input.empty()) {
LOG(FATAL) << "Please supply a data file with --input=";
}
operations_research::LoadAndSolve();
return EXIT_SUCCESS;
}

207
examples/cpp/weighted_tardiness_sat.cc Normal file
View File

@@ -0,0 +1,207 @@
// Copyright 2010-2014 Google
// 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.
#include <math.h>
#include <vector>
#include "base/commandlineflags.h"
#include "base/commandlineflags.h"
#include "base/logging.h"
#include "base/timer.h"
#include "google/protobuf/text_format.h"
#include "base/join.h"
#include "base/split.h"
#include "base/strutil.h"
#include "base/strtoint.h"
#include "sat/disjunctive.h"
#include "sat/integer_sum.h"
#include "sat/intervals.h"
#include "sat/model.h"
#include "sat/optimization.h"
#include "sat/precedences.h"
#include "util/filelineiter.h"
DEFINE_string(input, "examples/data/weighted_tardiness/wt40.txt",
"wt data file name.");
DEFINE_int32(size, 40, "Size of the problem in the wt file.");
DEFINE_int32(n, 28, "1-based instance number in the wt file.");
DEFINE_string(params, "", "Sat parameters in text proto format.");
namespace operations_research {
namespace sat {
// Solve a single machine problem with weighted tardiness cost.
void Solve(const std::vector<int>& durations, const std::vector<int>& due_dates,
const std::vector<int>& weights) {
const int num_tasks = durations.size();
CHECK_EQ(due_dates.size(), num_tasks);
CHECK_EQ(weights.size(), num_tasks);
// Display some statistics.
int horizon = 0;
for (int i = 0; i < num_tasks; ++i) {
horizon += durations[i];
LOG(INFO) << "#" << i << " duration:" << durations[i]
<< " due_date:" << due_dates[i] << " weight:" << weights[i];
}
int trivial_bound = 0;
for (int i = 0; i < num_tasks; ++i) {
trivial_bound += weights[i] * std::max(0, horizon - due_dates[i]);
}
LOG(INFO) << "num_tasks: " << num_tasks;
LOG(INFO) << "The time horizon is " << horizon;
LOG(INFO) << "Trival cost bound = " << trivial_bound;
// Create the model.
Model model;
std::vector<IntervalVariable> tasks(num_tasks);
std::vector<IntegerVariable> tardiness_vars(num_tasks);
for (int i = 0; i < num_tasks; ++i) {
tasks[i] = model.Add(NewInterval(durations[i]));
model.Add(LowerOrEqual(model.Get(EndVar(tasks[i])), horizon));
if (due_dates[i] == 0) {
tardiness_vars[i] = model.Get(EndVar(tasks[i]));
} else {
tardiness_vars[i] =
model.Add(NewIntegerVariable(0, horizon - due_dates[i]));
model.Add(
EndBeforeWithOffset(tasks[i], tardiness_vars[i], -due_dates[i]));
}
}
model.Add(DisjunctiveWithBooleanPrecedences(tasks));
const IntegerVariable objective_var =
model.Add(NewWeightedSum(weights, tardiness_vars));
// Optional preprocessing: add precedences that don't change the optimal
// solution value.
//
// Proof: in any schedule, if such precendece between task A and B is not
// satisfied, then it is always better (or the same) to swap A and B. This is
// because the tasks between A and B will be completed earlier (because the
// duration of A is smaller), and the cost of the swap itself is also smaller.
int num_added_precedences = 0;
for (int i = 0; i < num_tasks; ++i) {
for (int j = 0; j < num_tasks; ++j) {
if (i == j) continue;
if (due_dates[i] <= due_dates[j] && durations[i] <= durations[j] &&
weights[i] >= weights[j]) {
++num_added_precedences;
model.Add(EndBeforeStart(tasks[i], tasks[j]));
}
}
}
LOG(INFO) << "Added " << num_added_precedences
<< " precedences that will not affect the optimal solution value.";
// Solve it.
model.Add(NewSatParameters(FLAGS_params));
MinimizeIntegerVariableWithLinearScan(
objective_var,
/*feasible_solution_observer=*/
[&](const Model& model) {
const IntegerTrail* integer_trail = model.Get<IntegerTrail>();
const IntervalsRepository* intervals = model.Get<IntervalsRepository>();
const int objective = integer_trail->LowerBound(objective_var);
LOG(INFO) << "Cost " << objective;
// Debug code.
{
int tardiness_objective = 0;
for (int i = 0; i < num_tasks; ++i) {
tardiness_objective +=
weights[i] * std::max(0, integer_trail->LowerBound(
intervals->EndVar(tasks[i])) -
due_dates[i]);
}
CHECK_EQ(objective, tardiness_objective);
tardiness_objective = 0;
for (int i = 0; i < num_tasks; ++i) {
tardiness_objective +=
weights[i] * integer_trail->LowerBound(tardiness_vars[i]);
}
CHECK_EQ(objective, tardiness_objective);
}
// Print the current solution.
std::vector<IntervalVariable> sorted_tasks = tasks;
std::sort(sorted_tasks.begin(), sorted_tasks.end(),
[integer_trail, &intervals](IntervalVariable v1,
IntervalVariable v2) {
return integer_trail->LowerBound(intervals->StartVar(v1)) <
integer_trail->LowerBound(intervals->StartVar(v2));
});
std::string solution = "0";
int end = 0;
for (const IntervalVariable v : sorted_tasks) {
const int cost = weights[v.value()] *
integer_trail->LowerBound(tardiness_vars[v.value()]);
solution += StringPrintf("| #%d ", v.value());
if (cost > 0) {
// Display the cost in red.
solution += StringPrintf("\033[1;31m(+%d) \033[0m", cost);
}
solution += StringPrintf(
"|%d", integer_trail->LowerBound(intervals->EndVar(v)));
CHECK_EQ(end, integer_trail->LowerBound(intervals->StartVar(v)));
end += durations[v.value()];
CHECK_EQ(end, integer_trail->LowerBound(intervals->EndVar(v)));
}
LOG(INFO) << "solution: " << solution;
},
&model);
}
} // namespace sat
void LoadAndSolve() {
std::vector<int> numbers;
std::vector<std::string> entries;
for (const std::string& line : operations_research::FileLines(FLAGS_input)) {
entries = strings::Split(line, " ", strings::SkipEmpty());
for (const std::string& entry : entries) {
numbers.push_back(atoi32(entry));
}
}
const int instance_size = FLAGS_size * 3;
LOG(INFO) << numbers.size() << " numbers in '" << FLAGS_input << "'.";
LOG(INFO) << "This correspond to " << numbers.size() / instance_size
<< " instances of size " << FLAGS_size;
LOG(INFO) << "Loading instance #" << FLAGS_n;
CHECK_GE(FLAGS_n, 0);
CHECK_LE(FLAGS_n * instance_size, numbers.size());
// The order in a wt file is: duration, tardiness weights and then due_dates.
int index = (FLAGS_n - 1) * instance_size;
std::vector<int> durations;
for (int j = 0; j < FLAGS_size; ++j) durations.push_back(numbers[index++]);
std::vector<int> weights;
for (int j = 0; j < FLAGS_size; ++j) weights.push_back(numbers[index++]);
std::vector<int> due_dates;
for (int j = 0; j < FLAGS_size; ++j) due_dates.push_back(numbers[index++]);
sat::Solve(durations, due_dates, weights);
}
} // namespace operations_research
int main(int argc, char** argv) {
gflags::ParseCommandLineFlags( &argc, &argv, true);
if (FLAGS_input.empty()) {
LOG(FATAL) << "Please supply a data file with --input=";
}
operations_research::LoadAndSolve();
return EXIT_SUCCESS;
}

1877
examples/data/weighted_tardiness/wt100.txt Normal file
View File

File diff suppressed because it is too large Load Diff

751
examples/data/weighted_tardiness/wt40.txt Normal file
View File

@@ -0,0 +1,751 @@
26 24 79 46 32 35 73 74 14 67 86 46 78 40 29 94 64 27 90 55
35 52 36 69 85 95 14 78 37 86 44 28 39 12 30 68 70 9 49 50
1 10 9 10 10 4 3 2 10 3 7 3 1 3 10 4 7 7 4 7
5 3 5 4 9 5 2 8 10 4 7 4 9 5 7 7 5 10 1 3
1588 1620 1731 1773 1694 1487 1566 1844 1727 1636 1599 1539 1855 1645 1709 1660 1582 1836 1484 1559
1772 1510 1512 1795 1522 1509 1598 1658 1826 1628 1650 1833 1627 1528 1541 1497 1481 1446 1579 1814
56 25 76 35 28 52 21 32 64 67 48 100 94 87 39 18 78 80 56 72
4 70 36 46 85 31 96 30 66 92 33 18 19 34 18 4 42 94 4 89
1 9 9 9 5 1 4 3 2 8 2 3 7 5 3 5 2 2 2 4
9 9 6 8 9 7 5 2 1 6 4 6 1 2 10 10 6 5 4 3
1687 1738 1663 1480 1504 1826 1722 1660 1594 1445 1704 1660 1715 1701 1679 1516 1658 1611 1502 1685
1614 1647 1689 1615 1524 1800 1654 1752 1456 1452 1801 1713 1761 1513 1759 1484 1821 1448 1666 1611
1 49 35 83 75 64 20 84 31 88 27 88 21 32 12 20 26 64 6 11
54 2 21 94 44 19 45 6 61 41 45 86 98 45 66 77 76 64 31 25
10 4 7 3 6 7 5 10 5 10 2 1 7 7 2 8 3 8 8 8
10 1 1 3 6 7 2 4 6 5 7 4 4 9 5 6 1 9 9 4
1452 1565 1588 1319 1436 1434 1573 1427 1593 1432 1428 1549 1565 1312 1614 1362 1643 1536 1372 1490
1631 1338 1336 1487 1361 1363 1583 1652 1396 1376 1319 1369 1341 1434 1319 1296 1644 1418 1421 1338
71 58 89 62 8 31 74 52 71 85 1 77 35 30 96 12 4 29 64 34
8 98 86 22 6 6 24 61 86 76 17 36 63 83 81 37 80 56 11 57
6 3 9 3 8 8 3 8 10 4 7 8 10 5 5 6 5 10 3 6
9 4 3 2 7 10 6 10 9 3 2 6 6 9 10 9 7 5 5 6
1419 1682 1683 1617 1703 1549 1741 1634 1580 1588 1694 1574 1548 1730 1535 1438 1501 1504 1587 1687
1472 1507 1389 1454 1404 1522 1526 1681 1506 1584 1720 1767 1621 1677 1487 1513 1591 1620 1771 1712
7 70 52 52 86 66 70 60 65 70 27 41 42 88 21 15 40 80 28 7
13 58 4 43 41 89 80 54 34 92 66 72 29 40 53 35 91 58 6 82
5 10 1 2 2 8 8 5 6 4 8 4 1 1 6 5 10 7 2 7
5 8 7 7 6 2 6 6 1 8 8 5 7 6 6 4 8 6 5 7
1471 1794 1514 1473 1702 1583 1640 1683 1491 1519 1702 1527 1701 1675 1421 1718 1639 1742 1749 1653
1441 1722 1691 1612 1424 1615 1809 1533 1648 1702 1450 1614 1675 1435 1441 1485 1746 1732 1727 1612
76 54 14 32 100 37 69 36 27 7 39 52 74 67 93 49 89 73 79 98
45 36 24 71 47 19 32 47 25 37 86 5 37 60 46 28 72 11 52 4
1 7 6 3 10 7 2 8 1 8 8 10 4 3 1 10 10 8 2 10
6 7 3 3 8 10 1 2 3 2 8 2 3 5 6 9 10 6 4 9
1145 1091 1222 1290 1047 1011 1058 1313 1351 1076 1163 1004 1141 1061 1259 1306 985 1173 1154 1325
1352 1169 1189 1241 1210 1209 1331 1128 1102 983 1232 1131 1358 1339 1260 1074 1283 1068 1008 1023
73 32 44 87 67 63 13 10 94 11 50 90 93 79 96 39 33 20 72 77
11 40 75 24 52 100 83 4 7 12 49 45 59 42 6 75 16 10 65 29
8 8 10 1 2 9 3 6 1 10 7 10 2 3 10 9 2 3 4 8
6 4 3 4 6 4 7 5 4 7 7 10 10 5 9 8 3 3 1 1
1034 1260 1317 1095 1026 1187 1138 1281 1063 1006 982 1169 1051 1310 1189 1125 1097 1212 1091 1063
1084 1336 1016 1025 1219 1186 990 1167 1216 977 1184 1155 1235 1335 1008 1329 1064 1242 1108 1328
22 83 90 4 33 16 21 17 34 54 51 33 88 93 94 13 85 84 41 21
43 30 64 25 10 89 10 96 59 70 5 8 93 37 54 37 44 4 39 65
7 7 10 1 5 7 1 8 10 1 6 7 6 1 6 8 6 2 4 1
1 6 6 6 10 10 2 6 2 7 6 3 3 9 5 1 8 9 9 5
1192 1284 1086 1269 1008 1002 1202 943 1153 960 1201 1204 1074 983 1115 1066 1034 981 1199 1174
965 1222 1242 1020 993 1298 1186 1148 1032 1132 1182 1115 1299 1062 1094 949 1175 993 1293 959
75 33 77 73 71 24 90 94 44 57 11 67 77 27 27 100 83 81 1 5
3 20 75 97 4 98 70 92 84 20 83 12 67 48 90 80 5 94 47 24
8 2 8 1 7 6 8 5 3 7 10 6 7 3 5 7 7 9 9 2
3 6 9 6 10 10 6 5 2 5 7 6 3 8 9 7 4 5 4 6
1472 1343 1218 1338 1495 1463 1444 1249 1121 1325 1366 1368 1186 1545 1396 1517 1141 1538 1405 1508
1238 1175 1238 1351 1376 1324 1450 1237 1504 1498 1148 1307 1353 1291 1404 1188 1292 1140 1315 1540
12 67 9 86 83 64 94 80 46 97 77 78 5 54 14 36 96 82 41 12
79 77 71 68 47 89 97 67 16 22 89 78 34 34 94 72 75 33 39 22
10 6 10 6 2 1 3 7 10 10 8 1 1 10 9 4 1 4 1 4
4 4 6 1 3 4 5 5 9 7 6 5 2 10 8 5 10 6 5 7
1366 1541 1552 1418 1301 1363 1194 1349 1480 1311 1631 1335 1378 1443 1181 1258 1205 1521 1412 1251
1398 1347 1620 1449 1410 1327 1466 1510 1539 1412 1515 1297 1239 1201 1213 1332 1416 1205 1285 1614
41 18 66 42 100 71 89 19 92 3 75 57 46 2 53 57 17 9 30 25
90 19 93 69 76 79 5 100 16 89 7 32 78 4 21 85 60 29 43 77
9 10 5 5 3 1 5 9 1 8 1 10 5 8 9 1 9 4 6 3
2 5 4 1 5 6 7 7 5 7 3 6 8 6 4 6 9 4 6 2
928 623 690 630 796 811 728 670 618 788 609 629 984 841 918 809 613 644 724 764
667 713 797 663 951 920 716 892 677 774 894 652 988 696 872 713 971 719 956 836
98 77 8 38 79 28 4 57 63 57 7 96 2 48 18 3 72 39 17 31
80 21 60 33 60 38 84 69 73 88 2 1 11 22 6 92 92 42 66 10
10 9 5 9 3 10 8 2 5 5 6 10 5 2 4 9 4 1 2 4
7 1 3 4 2 6 3 5 2 5 2 8 10 5 2 2 8 7 2 8
754 682 557 827 647 880 631 783 875 806 619 648 631 540 590 658 876 696 739 570
738 886 724 548 870 882 619 789 553 860 606 622 709 771 861 640 646 598 890 722
48 83 74 78 6 75 51 45 67 95 57 93 3 25 64 18 13 100 25 19
25 8 69 99 94 90 3 61 6 40 13 15 72 5 62 72 32 86 93 46
7 6 5 6 1 9 10 1 8 2 10 9 4 9 3 9 5 2 1 3
4 8 6 1 6 10 8 5 9 6 8 8 4 1 10 5 8 7 3 10
832 907 759 997 708 929 831 1001 763 891 871 686 838 624 690 635 630 997 724 707
870 961 874 637 648 881 777 836 620 803 680 955 739 945 892 687 624 774 636 765
82 33 79 67 96 3 16 33 40 6 82 46 7 19 22 48 18 76 59 84
24 59 96 5 2 9 10 61 59 15 59 8 28 23 80 5 71 29 85 12
3 8 6 8 7 6 1 1 6 4 7 6 3 6 1 7 1 3 7 7
9 10 1 3 8 10 2 1 4 1 3 7 4 6 10 9 1 5 3 8
756 774 770 620 720 667 808 562 728 743 794 657 817 611 562 599 799 748 517 673
567 749 691 590 554 724 634 790 716 540 780 627 664 556 691 660 622 541 752 503
23 75 17 14 92 58 65 79 46 30 21 58 100 68 1 42 97 100 1 22
9 8 93 95 36 26 29 60 6 42 38 18 74 98 29 75 25 88 85 39
8 9 9 7 7 3 6 8 2 3 1 2 3 3 5 5 8 2 1 6
5 6 8 4 9 5 6 9 5 7 9 4 3 4 6 9 7 5 8 9
872 724 826 789 878 974 680 847 796 662 639 800 717 952 742 884 735 900 987 680
919 909 609 884 674 830 710 924 688 649 760 724 712 966 836 689 719 905 893 712
17 8 61 32 63 36 43 41 77 64 90 36 96 65 89 53 85 63 9 32
38 38 93 16 76 22 65 51 49 99 26 84 35 7 56 70 40 38 11 62
10 9 10 6 7 9 2 10 9 7 3 7 2 7 5 9 2 7 5 7
3 1 10 5 7 9 5 8 4 7 4 1 4 8 8 1 3 9 9 3
602 476 347 346 321 320 277 473 492 244 595 307 293 221 208 249 406 521 497 259
539 384 509 450 415 541 472 269 532 264 235 304 306 288 345 244 465 270 486 290
44 88 60 35 10 90 72 81 55 54 83 87 38 52 53 37 47 6 21 17
96 90 4 17 30 34 98 30 19 19 75 51 63 80 86 78 91 5 61 16
8 4 9 8 1 8 9 4 6 10 4 4 8 1 6 4 7 8 3 1
5 5 6 2 9 1 8 6 7 1 8 1 5 7 7 9 6 4 8 1
442 276 351 442 237 620 484 503 402 408 473 293 252 381 379 331 506 370 377 507
354 422 414 276 511 480 475 293 301 259 237 545 286 582 578 338 590 371 335 556
6 22 44 42 58 22 52 64 28 3 72 24 97 30 36 53 75 23 54 83
99 54 16 51 33 49 89 97 72 86 16 63 37 97 23 95 78 67 9 42
6 4 9 10 1 1 3 9 4 1 10 6 6 3 5 9 5 4 5 10
8 7 5 10 10 8 8 1 5 4 5 7 5 3 8 3 10 3 3 3
498 605 344 361 429 599 436 351 308 263 570 415 274 225 586 311 501 237 518 217
334 289 245 523 513 292 587 581 255 371 487 538 303 541 575 510 415 600 346 355
37 71 18 74 62 92 61 59 73 63 7 63 72 48 60 62 90 62 2 38
88 75 94 73 51 9 74 54 96 39 61 71 65 95 48 15 31 57 9 84
1 7 6 6 8 6 2 5 9 6 2 6 10 9 3 1 6 9 5 5
10 7 1 4 4 2 10 4 8 6 2 3 1 9 1 10 10 5 5 3
655 263 510 495 668 392 574 325 588 554 666 634 397 356 649 241 429 290 687 533
410 686 402 633 562 431 548 601 643 521 332 267 586 482 466 600 468 541 489 247
100 47 68 56 6 8 57 36 94 43 17 20 88 11 25 30 41 25 36 95
34 52 81 43 76 10 71 8 5 71 96 27 85 62 22 39 10 61 93 87
3 8 10 3 2 3 6 3 7 7 2 9 2 8 5 8 8 1 7 9
6 6 4 1 2 10 4 6 5 4 10 4 9 8 8 9 8 6 6 3
197 314 578 420 325 474 260 200 227 456 435 438 369 504 493 483 234 469 535 520
219 481 275 206 242 252 454 202 484 517 202 420 383 415 367 405 529 469 500 281
82 18 55 14 1 36 73 72 26 3 8 18 2 77 11 26 5 66 7 68
37 35 100 21 29 98 73 67 41 26 87 87 59 41 81 69 99 17 71 2
5 5 4 9 10 2 1 5 3 1 6 2 4 8 8 2 1 7 1 7
10 8 2 1 6 6 1 9 2 2 3 7 1 4 4 10 2 5 5 7
0 0 123 0 5 168 104 41 0 0 0 62 170 61 163 59 0 113 76 0
30 55 0 136 68 179 0 0 54 0 0 0 0 0 154 33 0 28 130 0
1 3 22 81 86 90 22 42 28 57 66 82 96 55 73 20 86 92 43 76
22 28 52 75 58 76 53 43 75 2 79 11 81 25 42 11 14 17 29 81
5 3 5 3 9 8 5 3 10 2 4 1 5 1 4 1 9 9 1 2
5 3 1 1 4 10 9 6 6 8 8 7 10 4 8 6 2 1 2 2
0 103 0 44 0 0 38 166 0 0 57 1 0 0 159 0 71 0 0 87
193 0 0 0 0 0 146 148 0 159 165 36 11 19 83 0 0 0 54 0
4 75 87 90 29 42 96 27 92 70 52 38 81 9 47 87 17 64 52 41
45 90 14 71 40 97 60 51 5 50 94 59 71 62 98 74 97 5 34 80
3 4 3 3 2 10 9 1 8 8 9 3 2 5 8 10 7 3 2 2
2 9 10 1 4 7 6 1 1 6 7 4 7 1 4 7 6 5 10 3
88 167 228 0 0 0 56 205 0 66 0 0 0 0 0 0 0 117 0 146
0 0 0 77 69 185 0 105 0 0 159 0 52 66 0 0 113 20 0 179
63 61 47 77 25 14 63 13 33 64 7 18 98 57 45 4 60 94 17 86
89 30 43 81 80 69 23 10 59 73 31 97 78 55 23 70 18 80 31 57
4 6 1 1 4 4 8 3 7 6 9 7 2 5 8 9 7 4 4 2
9 7 8 3 2 9 5 9 9 7 4 7 1 7 7 6 8 7 9 7
154 159 70 34 60 142 172 127 0 0 163 2 0 144 0 0 189 123 95 0
0 0 34 0 177 0 187 0 0 13 85 0 0 0 161 81 0 0 188 47
81 39 78 84 99 82 71 85 98 10 52 56 12 67 58 53 5 51 1 40
65 11 75 80 11 52 48 41 91 31 70 94 78 57 66 13 76 92 40 75
4 10 6 8 5 4 1 5 5 6 2 3 9 2 6 2 2 10 1 10
5 7 1 7 2 4 3 5 10 8 7 4 8 5 7 9 3 2 9 2
0 179 19 2 119 0 40 99 24 0 0 69 0 0 0 0 151 128 171 0
12 147 0 0 0 0 29 145 0 110 227 45 189 0 0 0 0 10 0 0
87 43 33 53 1 76 44 34 60 36 82 88 21 63 54 18 68 53 46 33
12 52 21 45 95 60 21 69 85 32 66 21 78 75 55 23 99 47 64 98
5 7 10 7 6 6 1 3 9 6 4 2 6 10 6 5 9 7 9 5
6 2 8 8 6 4 10 6 4 2 8 8 6 8 6 8 3 9 3 6
1267 1914 1785 1385 1653 1344 1888 2075 1804 1297 1990 1709 1561 1719 1947 2024 2095 2021 1591 1836
1616 1683 1703 1655 1612 1285 2041 1964 1720 1424 1465 1940 1747 2059 1868 1946 1597 1424 1564 1404
41 56 43 30 12 77 87 53 22 19 74 54 47 21 82 84 95 73 70 99
99 21 72 58 21 60 4 20 51 41 55 52 9 69 98 20 40 100 79 96
1 1 5 9 5 6 2 5 4 9 9 4 6 4 7 2 8 7 8 7
7 2 9 7 6 10 8 1 9 6 10 9 7 3 1 1 9 6 1 1
1494 1558 1707 1373 1538 1603 1783 2142 1765 1811 1878 1852 1675 1785 1921 1456 1879 1505 1979 1990
1387 1958 1519 1470 1475 1815 1739 1907 2090 1578 2190 1797 2202 2017 1352 1372 1485 2162 2054 2134
27 19 18 66 40 22 81 39 12 94 80 99 43 70 67 44 60 39 70 76
20 41 99 1 6 70 37 26 30 75 50 64 33 54 78 29 84 63 42 38
10 3 8 1 9 2 2 9 2 4 10 1 6 10 2 10 5 6 2 5
10 5 10 10 2 7 5 7 2 6 3 10 6 3 2 4 10 5 3 6
1829 1980 1263 1532 1527 1377 1304 1295 1535 1844 1586 1958 1596 1809 1815 1897 1413 1694 1977 1622
1381 1288 1656 1747 1310 1524 1365 1364 1946 1848 1869 1620 1300 2001 1507 1693 1773 1790 1920 1566
60 22 47 13 21 98 85 91 90 44 32 68 89 93 11 88 66 28 23 3
99 88 47 62 95 65 41 21 88 2 40 40 40 97 59 78 41 100 89 1
1 10 2 7 2 2 6 4 7 6 9 9 7 2 5 6 4 7 8 2
7 2 9 2 2 6 10 4 6 1 7 5 2 9 1 5 4 5 5 3
1442 1639 1483 2221 2264 1743 2047 1442 2193 2139 2239 1543 1725 1378 2034 1385 1939 2135 1892 1846
1690 1896 1993 1711 1610 2215 1922 2179 2199 2115 1718 1850 1487 1917 1566 2132 2188 2070 1935 2228
83 11 94 26 20 48 38 11 42 9 40 10 92 24 97 15 41 73 80 23
89 93 42 31 64 70 12 42 22 46 96 62 47 16 82 98 51 26 32 61
3 6 9 3 9 7 7 10 7 6 5 9 5 2 5 9 10 10 6 10
8 2 8 10 1 3 7 3 4 8 9 9 7 5 7 2 8 9 4 6
1756 1615 1772 1197 1866 1894 1703 1596 1847 1700 1347 1676 1734 1532 1441 1741 1818 1588 1715 1927
1794 1548 1811 1788 1861 1520 1781 1838 1863 1825 1437 1566 1608 1607 1644 1763 1581 1734 1313 1758
66 83 4 64 29 66 54 6 82 80 92 79 88 52 84 24 44 60 75 83
68 36 88 2 13 64 25 29 54 84 65 17 99 85 65 22 81 11 62 100
9 8 7 5 2 4 6 8 3 1 7 9 5 4 5 8 4 10 10 1
1 7 4 1 6 3 3 4 9 9 6 6 7 3 7 5 5 9 2 7
1480 1684 1474 1438 1532 931 1041 1110 1219 1826 1694 998 1607 1400 1174 1018 1033 961 1708 1405
1424 1264 1014 1314 1350 1797 1122 1531 1424 1441 1208 1252 1022 1410 938 1703 933 1338 1518 1090
9 90 99 90 69 100 29 84 51 3 53 30 43 20 10 17 61 27 16 32
46 54 66 70 72 81 34 25 37 43 71 97 70 29 6 87 27 80 47 1
5 1 8 3 2 8 5 1 10 3 10 3 1 1 10 3 6 7 7 1
3 10 4 4 9 4 8 2 10 2 1 4 9 9 7 3 9 10 5 1
1503 881 1491 888 1415 1099 1158 1567 1376 1157 824 1580 1318 850 1077 1164 936 1348 1000 1277
1198 1023 1454 811 1510 1152 861 1300 1213 955 851 978 1493 931 1252 1068 1350 1048 1010 1416
37 35 80 69 88 52 35 57 22 74 68 23 49 21 90 100 6 66 91 24
59 35 36 35 100 4 71 76 51 8 18 93 63 29 80 34 12 7 36 51
2 6 5 5 6 9 10 2 5 1 2 8 5 1 10 5 5 9 8 4
10 5 10 7 2 2 6 7 5 1 9 10 9 8 3 10 2 4 10 4
833 940 1046 1433 1128 829 1582 1431 1398 1217 1180 1109 1076 994 1096 921 1488 1278 1226 903
1028 1217 1018 1047 1027 1341 1586 1273 920 958 1066 1013 953 1499 1494 1561 1308 1536 984 894
7 77 25 68 63 75 21 41 93 45 59 18 26 5 20 81 23 22 66 13
70 20 35 1 82 74 44 33 4 12 88 2 6 16 41 5 89 22 53 40
2 10 8 1 4 1 10 4 1 1 3 4 8 6 7 6 8 8 7 6
4 4 10 10 6 7 5 6 2 6 8 2 9 7 6 7 3 1 10 2
1137 1078 737 846 972 844 691 1087 852 955 895 1209 955 994 746 1032 873 1092 1208 1034
824 1117 1104 743 643 811 708 1259 985 880 1203 1109 1052 1234 666 667 1068 803 1135 1180
100 25 90 60 100 77 16 53 90 21 25 82 23 71 71 74 81 93 85 60
72 5 80 72 34 81 42 47 32 45 41 25 59 77 19 48 37 7 2 62
4 5 6 1 10 6 8 2 10 2 8 8 8 8 8 10 1 3 2 5
9 5 1 5 9 6 5 2 5 4 2 8 1 3 9 7 10 3 10 2
1009 1009 1062 897 1643 1700 1012 1627 1509 1341 1380 1530 1392 1639 1415 1246 1002 1617 940 1067
1506 1738 1359 1345 1528 1473 999 1593 1422 1677 1351 891 1015 1285 1535 1349 1262 1433 1055 1542
29 43 10 19 31 18 27 15 68 59 46 82 17 75 93 93 80 29 71 25
87 38 64 57 97 70 32 75 99 48 13 63 7 48 26 11 65 98 64 13
5 10 5 8 9 3 1 2 5 2 5 1 2 1 10 9 7 9 4 8
5 3 6 5 8 2 10 3 8 5 5 10 6 5 9 4 1 1 9 3
747 1111 1041 1032 401 1148 906 789 747 893 629 996 1100 700 893 556 1138 918 656 906
832 858 478 780 766 577 649 999 461 649 505 832 1106 740 563 1186 673 983 1040 963
32 47 97 22 17 12 39 52 12 68 78 90 13 23 14 56 45 35 23 73
62 19 60 69 43 40 56 75 98 17 22 22 65 23 47 48 8 84 99 92
2 9 3 4 3 4 9 1 4 2 5 4 8 7 9 9 10 7 7 5
10 5 1 10 8 4 9 5 4 8 7 9 3 1 8 4 1 1 9 3
538 436 960 472 537 888 1115 1066 574 817 643 599 663 834 448 886 923 831 701 509
755 531 960 464 660 401 665 1115 657 693 772 1029 587 843 467 745 803 780 1062 851
77 9 44 50 48 26 13 92 31 13 56 81 44 75 42 85 33 68 21 74
74 3 17 23 70 41 37 9 50 99 61 11 75 46 50 14 32 5 45 3
10 1 2 3 5 8 4 6 4 2 4 7 9 4 9 6 9 2 9 5
2 10 7 7 5 6 1 6 2 7 10 6 8 4 10 3 3 5 6 4
591 869 702 434 766 972 820 735 547 426 436 623 989 657 358 824 935 380 850 873
440 989 1044 831 357 422 792 566 874 645 777 778 404 827 876 887 403 632 968 751
60 49 18 87 42 79 92 64 65 11 92 31 71 47 62 4 27 40 20 99
29 96 66 37 4 77 75 43 3 94 2 43 8 15 79 68 28 57 17 50
1 5 7 8 3 2 3 6 2 5 8 4 8 5 10 6 4 8 1 9
7 6 5 9 10 9 1 5 3 1 1 5 7 3 1 8 10 10 9 6
1159 986 1117 761 428 909 599 1123 1070 960 780 891 464 484 683 507 1064 521 431 1069
981 473 585 811 530 612 1098 526 601 1077 660 817 634 495 1104 516 890 426 512 939
5 46 67 20 44 44 93 3 82 31 78 23 83 3 34 40 36 12 55 21
60 61 11 32 1 7 49 44 35 59 95 32 63 80 55 71 17 88 11 43
7 1 6 7 5 6 7 1 3 3 1 8 5 9 7 7 4 3 8 9
10 4 2 3 4 10 8 2 3 7 9 9 4 1 3 7 1 10 1 1
732 933 691 670 499 629 561 816 810 910 964 509 546 494 490 412 802 1034 911 780
677 691 363 404 1008 520 728 736 854 812 819 684 539 553 983 733 895 691 446 515
63 27 17 40 27 48 15 46 78 96 81 39 99 65 2 26 2 3 40 19
28 10 38 33 44 39 15 85 49 99 70 96 66 47 79 90 48 98 97 94
7 8 1 4 9 8 9 1 10 10 6 4 2 3 5 8 3 1 9 7
3 5 8 5 6 2 2 8 8 4 7 3 1 1 2 9 7 6 7 3
625 448 143 797 452 717 316 387 491 464 203 778 536 518 462 512 296 316 756 578
131 129 691 685 575 431 369 57 607 17 505 289 453 292 509 382 690 111 254 425
14 75 70 39 94 69 32 33 75 82 51 66 63 4 83 94 91 81 64 74
21 9 9 67 45 39 8 39 80 75 32 58 72 73 30 93 98 43 26 18
1 10 8 8 8 10 5 7 3 10 3 8 5 6 4 9 8 2 5 7
7 9 6 2 4 1 9 4 2 2 1 4 9 7 3 3 4 2 8 4
513 228 419 398 232 147 101 102 756 38 39 135 116 555 465 823 347 49 714 338
411 440 230 354 50 419 16 773 580 437 149 139 874 291 353 852 773 606 132 835
66 26 8 14 75 40 99 7 27 18 11 96 49 48 75 81 99 70 98 68
58 79 65 66 41 22 41 85 88 1 67 40 65 67 63 50 72 29 28 33
5 6 5 7 7 3 7 2 4 10 4 5 1 6 9 9 10 4 2 4
1 1 2 4 5 4 6 3 9 3 1 7 9 4 9 10 9 10 5 1
259 201 384 841 310 629 132 431 815 125 254 707 381 705 201 296 405 481 414 469
722 251 748 425 813 273 177 672 570 21 348 17 650 81 159 661 683 206 166 59
56 68 92 64 27 47 46 15 12 88 66 21 60 74 53 28 49 46 87 91
85 93 26 63 2 59 4 3 62 43 36 72 56 94 14 36 2 17 7 61
5 4 6 9 7 10 8 9 10 5 3 4 5 7 6 10 1 7 6 3
5 4 8 10 3 10 6 9 9 7 1 10 6 9 5 3 5 8 6 8
355 429 511 168 486 286 141 481 493 478 421 411 77 117 635 178 447 236 337 512
394 488 233 703 456 83 383 120 534 657 320 108 205 276 322 115 193 149 768 364
48 43 58 92 38 28 83 7 39 25 96 37 25 17 71 78 94 38 59 30
75 76 88 95 22 72 67 76 21 21 82 84 84 70 95 29 51 20 49 26
3 4 4 6 8 2 5 2 9 5 10 2 1 8 5 4 2 1 2 10
4 3 5 10 1 6 3 7 2 9 6 3 8 6 9 3 6 9 1 2
786 140 199 360 561 183 810 489 856 46 765 378 333 798 428 72 870 468 631 702
416 854 171 480 411 655 793 850 408 521 278 722 195 597 71 861 595 276 134 768
34 46 22 4 20 74 98 34 45 19 62 44 2 60 60 78 14 28 15 81
29 8 27 2 26 38 77 93 10 9 22 10 16 65 97 10 7 5 17 55
2 5 1 8 10 7 10 7 4 5 7 8 1 2 10 6 10 9 3 3
4 2 2 6 10 3 5 1 6 10 7 4 9 7 2 5 2 3 1 2
119 181 156 0 129 127 0 0 0 215 211 0 0 125 0 0 0 0 228 56
2 0 0 0 0 271 265 156 0 0 0 0 62 0 105 129 0 114 0 0
36 24 79 9 17 31 57 52 93 12 2 45 78 43 30 76 16 52 37 38
78 21 97 27 65 85 59 43 3 32 54 86 49 3 90 62 87 92 51 80
3 1 7 7 8 8 5 9 1 8 9 4 3 3 9 8 3 2 10 10
7 1 8 10 10 1 6 8 8 8 7 5 2 6 10 3 4 4 5 6
0 0 0 93 0 179 6 99 0 0 129 0 270 46 311 0 0 81 0 0
0 0 0 0 0 0 184 180 0 327 0 0 156 333 0 0 0 231 0 338
1 79 1 18 100 96 4 21 76 98 30 45 67 57 68 25 37 99 86 2
80 1 28 18 18 96 17 19 1 69 54 53 6 58 20 73 39 54 71 35
5 10 10 7 9 3 10 6 2 1 6 9 9 5 2 6 5 5 3 1
5 4 8 6 1 2 10 6 3 6 4 6 9 8 1 2 9 5 2 2
0 61 361 0 0 0 327 0 25 76 323 152 1 190 0 126 278 0 277 227
248 35 93 0 45 0 248 68 0 0 0 49 0 0 0 231 297 0 0 0
7 64 38 47 67 21 61 3 15 25 42 53 11 47 41 82 41 9 99 75
22 86 30 23 96 7 31 17 34 54 75 54 38 61 13 33 34 16 74 55
4 9 8 10 7 7 4 6 6 7 1 6 3 3 4 7 1 9 10 5
10 1 9 7 8 7 6 2 3 3 8 9 10 9 6 9 3 2 5 3
195 0 74 0 103 0 0 0 41 69 271 202 159 329 29 0 192 68 0 6
80 0 7 0 242 0 0 144 153 125 0 0 0 0 0 0 0 83 0 165
58 88 19 14 45 9 28 62 58 95 9 82 81 12 93 5 21 79 91 64
17 68 92 95 32 6 63 38 62 70 48 36 26 93 72 35 76 59 35 83
8 9 6 3 5 10 3 7 3 8 9 8 2 4 2 7 2 4 8 3
8 1 1 9 7 3 6 6 1 3 2 9 3 3 2 1 3 8 2 9
325 384 0 0 0 0 0 139 168 0 0 226 195 0 0 0 37 0 103 0
0 0 70 134 0 0 0 0 0 0 47 23 0 84 0 0 0 399 369 377
89 11 49 41 88 19 85 67 83 61 82 46 76 1 45 56 97 55 57 76
7 92 79 90 93 34 49 84 68 58 84 48 78 90 79 75 94 14 7 60
10 8 8 1 2 9 3 9 10 8 1 9 1 4 6 4 9 3 1 9
9 6 9 8 1 10 6 9 7 9 5 9 4 1 8 7 10 3 3 2
1445 1249 2181 1877 1517 1516 1253 1762 2246 2550 1652 1729 1912 2530 1272 1847 1408 2483 1939 1595
2624 1437 2244 2031 1653 2654 1478 1312 1962 1388 1334 1298 1683 1477 2448 1596 2347 1610 1669 1726
59 46 15 51 81 59 86 89 94 31 89 64 22 20 98 100 19 39 70 24
65 55 35 67 69 87 5 61 69 8 69 43 30 41 93 53 46 68 22 33
3 9 5 10 8 7 8 4 3 9 8 4 10 3 3 8 1 5 5 3
6 4 10 1 3 6 6 1 9 5 6 5 9 9 5 6 7 1 2 6
1567 1721 1314 1352 2126 1136 1462 1138 1789 1507 2085 2152 1967 1862 2260 1711 2058 1220 2164 1254
1929 2127 1977 1741 1146 1824 1435 2305 1458 2306 1332 2166 2106 1478 1777 1899 2321 1919 2390 1435
58 59 77 73 34 95 68 3 24 65 36 57 75 25 31 6 62 86 78 23
88 10 82 87 83 13 26 77 7 65 70 76 47 88 52 71 18 57 90 52
8 2 9 8 2 2 10 3 7 8 7 8 2 8 8 7 6 6 9 2
5 10 5 6 4 7 7 4 6 7 9 2 3 8 9 7 5 4 6 5
1934 1175 1115 1502 2129 1792 1230 1803 1832 2123 1134 1253 2297 1666 1659 2101 2335 1304 2360 2293
2138 1620 1730 1340 1179 1868 2003 1600 2038 2238 1471 2313 1730 1505 1920 2194 2097 1926 2265 1361
4 72 79 38 86 43 42 86 34 77 9 49 17 28 100 44 32 2 12 92
3 59 22 16 82 12 84 44 52 27 30 7 20 24 72 36 25 75 99 69
5 2 9 4 9 9 10 8 4 10 8 9 5 2 5 4 9 7 5 9
7 5 9 2 1 10 6 2 1 2 4 8 6 7 10 2 1 8 6 5
1241 1177 952 1274 1716 1866 1388 1739 1257 1384 1903 1703 1428 1738 980 1550 1451 1819 1662 1977
1347 1417 915 1253 1283 1459 1145 1672 1486 1548 1721 1418 1591 1275 1845 1007 1624 994 1800 1640
43 56 37 79 6 72 1 20 15 34 71 69 61 91 39 90 62 48 77 51
65 60 31 23 44 39 28 79 3 46 73 96 72 99 48 56 10 66 13 40
1 10 3 7 3 7 7 3 5 2 4 3 8 2 6 8 4 7 2 10
3 6 9 8 3 2 3 8 10 4 9 1 9 9 9 3 3 7 6 10
1056 1538 1837 1610 1103 1848 1441 1934 1860 1421 2026 1948 1602 1425 1406 1502 1642 2039 1501 1472
1393 2113 1295 1910 1267 1838 1246 2010 1360 1208 1058 1876 1937 1486 1682 1281 2119 1245 1888 1436
48 38 51 33 88 6 12 88 83 55 61 47 44 32 62 21 13 37 57 25
57 24 67 77 73 1 88 98 86 26 98 11 49 13 51 43 42 27 79 25
4 3 5 8 9 3 8 3 10 1 2 10 6 3 2 5 5 8 7 2
4 5 7 7 6 4 9 7 5 5 1 9 2 3 4 4 7 8 4 9
1443 1541 1612 1229 1652 1580 1612 1310 1555 975 1395 1652 1522 837 1425 1406 997 1398 1699 1366
715 1681 763 1024 852 917 1117 860 914 1693 1277 1722 1370 934 1176 1311 1226 1169 1181 1686
20 97 94 40 57 20 23 77 84 13 99 16 36 19 59 18 75 36 17 43
91 15 64 55 3 58 70 23 58 23 84 18 29 20 31 12 21 11 17 84
9 5 2 9 7 10 10 3 7 8 2 9 4 6 3 6 3 1 4 2
5 10 9 8 3 4 2 4 6 2 6 3 1 6 3 7 6 7 10 10
1171 1010 649 1448 751 1185 648 1100 676 672 1499 988 622 1362 1373 636 1191 1309 1333 577
701 666 1341 768 797 871 937 554 1163 1245 1482 1234 984 1293 607 837 920 1451 682 835
91 65 21 44 64 45 59 76 91 35 83 15 30 77 100 64 64 66 96 34
6 48 35 34 95 25 58 80 100 49 87 89 18 28 17 82 73 21 27 83
7 4 5 1 8 4 6 9 3 1 7 10 6 6 4 6 6 9 1 10
5 6 1 5 8 6 2 8 3 6 6 3 4 9 9 8 3 4 9 10
930 1059 1244 1337 1643 1557 941 1854 1158 1123 1435 1016 1771 1883 960 1119 1116 1010 1800 1102
1580 1245 959 1274 1313 1648 1962 1911 917 1313 1434 1166 1276 1021 904 1845 695 1499 1562 1137
17 28 62 91 89 61 24 81 8 99 87 82 52 81 31 48 28 98 14 32
69 94 71 94 38 67 16 95 24 67 41 99 48 97 16 74 54 14 90 91
3 6 8 8 9 2 2 10 2 1 4 6 2 6 5 1 4 5 6 4
6 3 5 2 2 8 1 4 4 6 7 1 3 10 9 2 9 6 9 1
957 2105 1120 1956 1943 1859 1043 2018 1305 1088 763 1805 895 1461 1409 896 1531 990 1491 1856
1429 736 1391 948 1056 863 1444 886 1564 1650 751 1549 1117 964 942 1360 1852 968 720 790
86 25 28 31 40 5 99 86 63 38 65 62 53 61 78 58 39 60 68 75
76 76 41 19 49 5 84 99 70 93 61 25 80 41 13 12 46 2 60 78
5 2 7 4 8 1 5 3 8 8 5 7 2 4 6 8 3 6 4 6
3 7 7 3 4 6 6 3 4 7 5 9 2 1 3 7 3 6 1 3
1484 864 1710 954 1928 1196 1211 933 1452 924 1210 759 768 901 1076 1204 1819 1324 1910 1314
1208 1369 1594 1594 1047 763 793 1387 1089 713 1866 771 1836 1608 686 1804 1837 1362 1029 1395
12 46 7 16 55 65 44 92 14 38 49 100 12 98 44 88 99 30 33 2
51 70 93 97 75 12 82 26 5 98 36 48 4 26 69 25 61 47 72 20
2 8 3 4 9 9 9 7 3 8 2 8 5 5 4 3 7 5 2 6
7 1 6 3 2 1 7 3 9 8 3 2 2 3 3 10 3 1 10 7
1309 524 939 577 378 358 220 611 813 508 587 1209 762 1001 688 452 299 1344 972 211
1322 1359 349 824 973 269 486 1054 933 1070 1286 993 849 209 492 851 569 1356 914 332
37 37 64 2 96 82 96 1 49 37 47 47 39 29 12 34 38 40 62 58
45 5 51 17 89 13 6 13 25 4 36 52 37 72 26 42 38 66 40 94
2 7 2 5 7 7 9 3 7 1 2 3 9 7 7 5 10 1 10 7
7 3 2 10 4 1 8 4 2 7 6 3 2 10 7 9 4 6 5 7
846 751 1016 643 363 1089 392 1154 1120 512 995 509 1025 290 627 731 328 302 831 616
521 763 1016 216 727 431 1126 820 624 347 793 391 841 1044 1005 572 873 243 232 1130
31 96 43 48 56 53 73 18 80 26 49 55 69 41 39 97 14 76 88 88
39 63 18 73 92 88 32 1 53 87 7 24 25 53 3 98 45 29 54 80
10 8 9 3 4 4 3 1 8 4 8 7 7 8 7 3 4 9 1 2
3 6 2 10 3 8 6 10 3 5 2 9 1 5 4 5 3 2 7 5
1126 453 366 995 1142 312 616 1308 212 487 895 670 909 1450 454 1011 783 749 944 922
1070 213 320 1287 902 1188 1227 1457 970 394 1109 1109 253 296 607 1465 941 1175 1230 834
94 74 66 15 57 24 66 53 52 51 20 79 66 76 65 78 14 77 20 41
40 81 78 61 16 69 13 32 40 78 76 54 42 94 97 30 77 59 83 63
10 6 6 6 10 2 6 5 4 10 2 6 3 8 1 8 9 9 4 6
10 2 5 1 3 2 1 10 3 10 4 5 5 3 8 7 1 5 1 7
604 331 1144 648 499 636 1080 1434 342 930 1131 741 1202 353 779 1191 1026 406 996 1204
1313 498 376 1079 866 956 1469 230 1104 1291 1471 544 1176 486 1280 900 551 703 265 520
52 75 35 70 47 97 50 18 34 9 4 78 23 30 5 84 52 34 45 71
86 45 88 80 17 42 81 53 69 57 45 36 89 75 84 77 57 33 75 30
4 1 8 4 4 2 2 6 10 8 2 7 1 7 7 10 4 9 8 4
5 5 2 3 6 7 7 10 1 7 6 10 9 9 6 7 10 6 5 8
1213 263 497 1051 1192 956 820 1466 1323 1104 1339 737 529 998 1364 392 789 680 564 1290
631 854 449 381 763 619 1372 893 1394 932 1453 1431 1481 1067 1252 1044 1159 802 1409 1105
61 57 26 79 2 26 74 27 25 52 22 15 61 51 54 23 70 92 29 33
39 99 87 34 83 45 45 14 45 61 97 65 97 27 16 84 39 78 55 70
4 10 3 6 3 9 2 8 10 2 10 9 10 6 8 1 6 2 8 1
10 8 9 6 3 5 1 3 3 5 8 10 7 1 8 7 1 5 2 4
1005 694 0 268 301 136 86 41 179 0 319 0 826 0 433 269 64 0 917 376
629 506 560 78 810 704 973 0 497 177 606 0 448 752 495 791 946 0 753 554
3 29 97 16 27 17 66 100 52 83 76 55 29 38 83 7 40 50 18 87
93 36 92 28 27 70 93 66 6 77 90 41 23 36 26 96 1 79 26 77
9 6 1 3 4 4 8 8 7 3 10 9 9 7 9 5 10 7 2 5
9 8 6 1 2 3 4 4 4 10 2 6 10 4 8 1 10 5 6 3
892 585 889 788 887 0 182 643 596 743 0 571 975 136 0 1015 225 0 40 694
0 330 728 874 197 113 729 404 399 28 763 0 48 574 666 912 344 431 815 702
89 55 83 53 57 33 33 57 69 60 44 65 2 47 42 51 59 57 32 93
69 5 95 70 92 62 92 66 15 49 63 68 54 42 23 64 53 69 69 47
6 6 8 7 1 6 6 9 1 8 9 8 6 5 1 5 1 7 10 4
1 9 5 1 9 3 10 10 8 5 3 8 8 10 4 3 7 6 8 3
867 0 0 892 753 0 0 690 318 858 0 922 935 401 623 580 552 0 319 229
296 346 1073 0 978 25 506 559 281 729 32 384 33 43 350 419 698 380 309 1011
60 53 96 70 51 86 60 23 61 94 83 18 87 85 61 75 54 19 72 18
14 8 69 74 49 18 85 74 66 70 31 50 5 34 95 39 29 38 45 81
1 6 2 10 6 8 6 10 3 9 9 7 6 2 7 6 10 4 7 7
5 2 2 7 2 4 7 7 8 8 1 7 10 5 6 8 4 4 8 3
204 197 546 1039 103 484 11 443 266 0 147 0 549 0 1044 1024 997 426 195 581
399 100 625 0 784 661 0 445 700 729 761 542 1027 149 382 632 893 941 862 0
82 92 27 46 100 42 10 26 38 48 26 87 17 12 46 98 81 92 16 29
7 97 64 54 96 90 94 49 79 88 88 96 16 60 8 78 95 27 91 80
10 5 4 6 10 9 2 7 8 4 6 7 5 4 2 5 9 5 1 3
10 1 7 5 2 1 6 4 3 1 9 4 4 2 9 2 7 2 3 3
173 171 697 157 534 174 1070 590 659 0 0 547 1098 126 0 979 737 722 130 401
934 1089 80 0 404 758 666 0 773 361 257 11 53 513 0 0 1032 0 433 297
51 95 45 65 20 23 23 96 40 39 87 51 52 42 80 46 23 88 21 98
51 81 9 28 60 83 20 59 3 5 8 19 61 15 5 38 42 32 23 50
4 10 10 9 4 4 10 10 5 9 6 1 4 6 7 7 7 1 4 4
10 8 2 8 4 4 1 9 2 4 1 3 4 9 9 2 7 6 2 5
374 413 0 0 0 0 422 0 51 0 0 134 25 500 511 0 0 337 0 0
281 399 0 0 276 0 0 211 0 0 461 509 518 0 0 0 89 528 265 364
91 37 97 15 58 100 18 67 34 36 57 90 81 42 28 46 91 69 23 99
80 20 11 17 96 52 41 71 14 75 39 34 36 52 9 84 93 99 35 100
7 3 8 6 6 5 10 7 7 2 2 3 5 6 4 10 2 1 9 10
10 10 4 3 8 10 10 2 4 4 9 8 5 2 8 6 5 10 8 1
0 444 471 485 348 0 219 221 359 185 0 96 291 505 260 0 0 589 0 0
0 400 651 0 361 135 258 0 299 0 0 424 122 0 237 551 0 0 0 334
53 49 10 85 87 100 93 76 15 63 5 88 24 31 30 29 23 52 32 11
55 27 53 47 88 9 13 56 17 5 10 59 68 75 21 79 94 31 100 43
7 2 10 1 1 8 5 10 8 2 8 7 7 1 10 4 10 1 6 5
3 2 3 7 3 1 4 4 4 2 4 4 9 2 10 4 10 5 6 3
288 199 0 0 320 67 355 554 0 289 0 0 203 448 0 216 220 472 0 0
84 314 0 0 393 201 0 239 0 316 499 130 116 0 424 125 360 354 516 0
19 12 85 69 9 2 24 64 8 95 78 33 24 82 5 30 89 8 41 13
66 69 99 45 46 17 72 90 46 55 29 15 14 40 18 91 24 81 67 93
4 1 2 4 5 8 4 10 8 8 4 8 9 1 6 7 6 9 5 3
10 2 2 7 7 7 9 7 6 5 3 6 8 3 4 4 10 6 6 5
316 351 0 0 308 14 512 0 0 419 0 330 0 0 357 0 275 0 0 0
536 0 0 53 139 235 199 423 0 0 0 0 423 208 550 0 297 450 372 0
95 62 4 64 53 38 62 74 64 62 1 13 56 22 50 83 83 59 18 90
30 67 90 41 10 94 30 49 62 40 79 27 56 59 58 93 87 57 65 68
3 1 2 2 1 3 5 8 8 1 2 4 7 3 5 10 2 2 3 8
1 6 7 1 6 1 2 4 3 7 6 1 10 10 10 8 9 4 1 3
395 0 588 300 333 31 340 0 512 537 457 0 0 166 0 0 578 0 571 25
0 515 0 0 0 552 0 222 216 0 454 0 85 0 606 0 0 353 0 498
17 88 28 68 79 94 40 52 64 46 77 23 21 29 41 31 29 81 11 29
93 92 45 70 47 8 78 14 54 25 24 22 4 94 75 58 16 19 100 90
10 7 2 4 1 8 4 10 7 4 6 1 6 1 3 4 10 2 7 5
4 5 8 9 5 3 5 7 7 6 6 6 3 1 4 7 3 8 7 1
1338 2062 1669 1534 1564 1391 2193 2223 1373 1713 1026 1743 1537 2199 1243 1534 1179 1214 1727 921
2359 2189 2155 1015 1245 1339 871 1508 2175 1422 1456 1406 926 1038 1128 2146 1942 2078 2042 2013
52 31 94 85 72 9 68 47 15 83 89 59 50 36 31 17 79 3 45 19
28 72 60 69 53 83 85 70 40 31 4 31 99 64 81 65 72 81 58 84
9 1 9 10 6 3 6 7 10 6 5 8 10 4 2 2 10 9 9 10
5 6 10 3 7 1 3 2 6 10 9 2 3 9 4 5 5 10 4 8
1349 2078 1523 2126 1871 1271 1006 1749 1928 1774 1537 1783 2157 1532 1854 1665 2563 1234 1640 1226
2350 2052 1793 1525 2415 2488 2060 1254 1641 1408 1302 1105 1150 1980 2200 1949 2375 2320 914 2119
90 86 18 19 47 73 33 12 53 61 96 20 1 29 51 86 12 9 23 55
37 85 12 77 52 95 98 3 65 31 38 89 9 36 68 93 45 9 1 77
2 1 1 2 3 7 4 7 4 5 2 4 9 7 5 8 1 4 5 2
9 3 9 2 3 5 5 4 9 8 7 6 5 6 10 4 4 9 5 10
1747 2082 2255 1152 1211 1532 819 880 2087 890 916 2090 1131 1782 1415 2247 1650 2229 2271 1521
1258 2268 1744 1983 1566 1261 1928 1502 1991 2006 1416 2025 1878 1992 840 1960 1881 2049 1593 1427
52 1 94 81 46 32 2 3 44 22 35 9 60 46 12 88 38 32 27 32
50 63 53 38 96 73 42 4 3 50 24 32 27 35 4 28 53 23 70 100
10 10 2 1 10 2 1 4 2 1 3 9 5 10 9 4 9 10 4 8
9 4 5 10 3 5 2 10 3 8 1 9 2 8 9 10 2 2 8 6
1839 685 1442 1414 1747 761 1405 1888 1750 1448 1292 737 1821 1696 897 1655 653 1330 1194 1001
738 695 1941 1384 1101 929 1236 1250 1072 1012 912 668 816 1936 897 1301 1214 1155 716 1817
88 77 95 82 40 84 17 79 78 60 23 32 41 78 1 76 92 62 16 50
26 92 16 98 64 99 22 65 56 68 36 100 79 37 38 55 40 97 84 86
10 9 6 1 3 6 4 6 6 2 6 4 6 1 6 7 9 1 8 8
8 5 2 9 6 4 1 6 2 3 10 3 6 6 9 7 6 9 1 5
2380 2123 2763 2365 1172 1171 1943 1878 1732 1367 1370 986 1583 1114 1156 2097 1554 2193 1594 1622
1725 1454 1528 2535 2205 2885 1562 2664 1016 1537 2429 1427 2647 1422 2377 1712 2335 1377 1354 1078
73 68 69 37 27 80 3 2 78 24 54 97 86 71 83 5 39 41 29 12
50 11 9 7 65 9 18 83 53 17 29 37 16 70 93 66 81 56 40 73
2 3 4 6 5 4 5 1 6 4 5 2 9 3 8 3 5 9 3 2
5 6 8 5 8 2 9 2 10 3 3 1 6 9 2 3 2 8 8 9
426 1677 602 778 1508 480 1314 481 1390 1584 1019 718 1699 586 1048 758 1673 1716 1667 576
992 1056 823 1550 387 1735 1067 466 1497 1620 859 626 1525 1071 1501 1388 537 1036 1416 1843
14 82 47 64 34 24 58 37 92 15 99 18 68 22 3 35 70 63 81 23
37 11 21 17 34 91 90 58 54 83 33 88 19 17 74 53 78 80 13 1
1 3 8 10 9 7 8 8 2 4 5 5 10 3 5 8 10 3 7 10
10 4 4 2 5 5 10 5 8 1 5 4 1 1 2 4 6 2 7 8
512 426 483 1102 835 1669 1676 870 657 766 1767 1700 1635 420 1302 1545 990 1611 1546 1456
478 1646 1676 1729 935 573 1300 1865 611 751 695 1276 1866 1105 1798 765 391 1258 856 1706
43 79 34 85 17 73 61 53 96 87 10 8 83 82 84 27 8 76 66 92
30 37 17 85 37 88 76 92 44 4 59 4 94 14 62 13 60 100 57 14
10 8 5 9 6 2 1 7 2 8 5 6 2 8 6 1 4 5 4 6
9 2 2 6 10 6 8 8 7 9 3 9 8 2 10 8 1 9 8 5
1109 506 2070 665 2085 1505 533 1899 1501 724 1976 1522 581 557 2018 690 1868 1554 844 1590
467 1940 1763 1369 1936 1425 2013 679 1495 724 1630 1037 1915 1932 1138 1338 1323 1165 1816 2105
21 72 15 25 58 39 69 20 96 47 14 86 59 57 25 48 99 81 57 32
98 87 42 69 65 93 92 92 37 72 95 37 79 49 17 44 85 2 4 57
4 10 5 10 6 10 5 8 10 10 9 2 9 7 7 1 5 7 9 1
8 10 2 4 6 1 4 9 5 5 7 9 1 8 8 6 8 6 4 3
1806 1799 1583 1636 1853 2134 780 1173 490 552 782 1959 1216 2203 1886 1435 1192 1493 539 905
1803 1248 2125 1012 2231 586 696 1683 1072 1571 695 1184 641 663 2045 1416 1443 728 2213 1614
37 29 53 10 69 83 16 13 25 55 18 73 51 2 4 63 22 34 3 57
42 13 18 31 40 56 32 65 76 32 5 43 38 63 76 51 40 26 63 79
2 8 1 10 5 1 6 3 1 4 4 8 1 7 5 6 2 3 2 10
1 10 4 4 2 6 9 3 10 10 2 2 5 1 10 7 9 2 4 6
661 1410 923 401 1076 1203 573 1355 1202 647 449 846 818 1337 1200 589 1170 1086 952 664
1001 1267 637 1396 923 672 993 756 723 1567 1476 1369 1178 994 1102 1502 1361 678 1217 788
10 69 88 73 89 24 16 9 43 26 6 95 42 29 79 47 81 39 34 86
86 17 45 36 10 76 68 24 32 81 34 81 63 52 56 39 40 61 21 35
5 10 8 8 10 8 10 6 8 6 7 10 7 1 1 9 10 4 6 8
10 5 2 6 9 9 10 1 7 4 5 3 2 9 7 2 1 4 7 10
420 1309 525 1430 1497 131 131 1514 296 1456 762 1278 426 1374 41 693 575 814 596 175
574 446 977 1315 476 1021 1343 618 409 1383 594 1099 1208 364 492 1369 1164 995 1251 1014
85 65 41 46 85 31 59 91 41 26 43 78 43 1 85 72 10 59 55 39
88 59 1 52 51 8 50 84 3 71 5 12 75 64 50 16 26 55 46 79
10 4 9 5 6 3 1 8 3 5 4 7 5 7 1 1 3 10 7 1
6 1 5 9 3 5 5 8 10 1 7 1 2 5 10 4 2 7 8 1
655 170 1030 673 453 1100 1370 1455 621 209 1163 288 292 1547 506 1074 972 78 128 1240
143 1531 81 269 1265 886 760 1212 1146 673 29 500 1497 377 482 374 981 691 333 256
35 43 7 66 53 26 13 41 36 74 67 53 94 34 32 16 69 7 51 43
29 47 43 52 70 60 7 64 17 6 18 2 23 99 31 94 69 3 80 70
5 9 5 9 5 1 3 6 4 6 1 6 1 9 2 4 4 2 6 5
9 10 3 4 1 8 9 8 2 2 3 5 4 9 6 5 7 7 4 5
892 1198 538 525 1016 650 884 1099 634 992 1092 255 10 253 148 633 1093 974 662 1268
411 66 711 1030 787 261 342 1365 60 1361 382 1375 15 539 575 564 675 314 1190 881
62 83 63 75 18 87 28 46 73 44 99 55 62 99 14 61 48 50 86 24
20 46 6 9 98 92 45 84 27 44 51 19 83 11 49 89 68 58 46 71
4 8 4 3 10 4 5 4 1 9 7 8 1 8 6 3 5 10 4 7
6 1 2 2 6 3 7 7 3 4 10 5 5 6 4 9 10 1 6 1
236 261 1737 227 383 1094 776 1307 1372 671 88 172 684 1525 1628 615 870 1468 1711 1129
623 98 52 983 751 941 916 167 499 441 1124 218 23 609 1714 654 223 1524 1209 1551
97 16 62 14 29 41 26 97 26 62 36 20 43 19 99 89 64 7 99 12
2 73 2 1 98 17 49 69 18 94 60 35 61 9 33 20 51 23 44 46
10 10 7 8 10 1 8 9 8 3 6 2 6 10 9 1 5 10 9 7
4 8 9 6 1 5 10 2 2 8 1 2 2 9 8 1 4 8 10 8
553 1235 689 933 678 1103 595 145 126 988 741 1137 1095 1150 537 118 962 956 754 1100
611 1301 941 1056 768 686 337 1151 475 464 913 357 465 914 1257 1046 221 851 1011 1192
97 29 35 31 69 73 13 86 97 7 53 88 60 69 33 89 64 51 11 43
42 96 23 8 58 3 82 47 1 20 80 24 89 53 88 6 70 57 53 64
6 10 7 9 4 6 8 8 2 1 5 1 9 7 9 4 2 3 10 5
7 2 7 1 8 3 9 1 9 4 9 6 9 5 3 7 10 5 2 5
0 883 280 474 0 1053 782 2 185 0 779 873 232 0 0 332 497 45 629 734
360 1082 434 425 151 821 973 288 1004 616 993 1209 581 675 530 742 1155 0 1174 465
49 59 92 74 44 16 70 11 16 11 3 4 65 80 43 50 20 9 18 52
35 40 37 16 96 68 85 49 14 39 25 63 29 55 100 73 11 68 30 97
1 9 2 10 8 8 4 10 5 1 5 6 9 8 7 9 2 6 3 9
7 8 1 9 6 3 3 2 7 6 3 2 9 8 10 4 6 5 5 3
437 311 882 962 0 0 410 619 899 691 625 0 0 0 631 137 493 411 39 157
0 521 635 0 395 909 84 790 62 936 860 0 736 495 1040 0 607 1050 337 0
67 98 20 98 91 60 55 71 41 60 18 12 39 32 31 65 35 59 96 81
5 80 91 10 58 86 76 8 25 22 85 34 71 83 31 49 84 22 8 17
4 3 1 4 7 5 8 3 10 9 10 1 4 6 9 3 1 2 2 3
8 9 8 8 4 5 10 5 4 4 4 2 2 5 1 8 2 5 2 4
966 151 262 477 980 323 0 1172 0 848 1200 187 0 1148 1030 826 522 0 0 135
0 1206 150 0 0 36 0 243 1007 0 0 0 1244 413 503 0 0 882 192 603
94 92 86 56 74 45 8 68 59 92 8 62 89 62 80 31 38 34 97 71
5 46 12 81 17 84 53 62 31 90 28 21 31 57 23 64 28 34 1 4
3 6 10 10 6 6 6 9 7 5 6 1 3 1 5 4 1 10 10 8
8 3 2 3 7 6 5 10 10 4 9 1 9 4 3 10 2 2 2 1
628 713 0 822 0 413 488 833 0 0 736 1019 439 211 171 794 447 941 1064 845
310 83 654 655 30 0 263 72 497 0 712 62 916 54 155 1043 267 0 781 422
99 38 34 9 87 68 44 8 83 100 59 8 52 57 48 48 88 20 54 71
13 19 2 22 75 40 92 51 54 19 3 9 55 50 94 52 12 75 99 38
2 7 6 3 6 2 7 8 4 7 5 9 9 10 5 1 5 6 9 7
6 4 6 1 10 1 5 8 8 9 4 5 7 5 6 8 1 4 7 7
956 600 1039 413 130 759 56 968 702 442 413 360 985 0 986 389 870 1005 507 290
135 0 929 567 627 667 648 0 0 93 989 234 1137 680 989 1121 655 639 760 0
82 87 86 18 48 76 57 100 56 27 40 5 91 61 74 18 71 55 77 28
37 35 42 29 63 86 45 17 47 40 34 90 17 87 41 51 30 67 73 4
6 9 10 3 9 4 3 1 8 7 10 3 6 4 7 6 4 9 6 5
8 2 1 1 8 7 10 3 8 6 3 10 2 6 4 4 3 9 2 7
303 0 403 0 0 508 114 0 0 273 111 164 0 338 0 0 0 251 0 272
184 328 0 116 0 347 0 0 0 750 54 120 60 0 0 0 0 780 100 804
70 43 42 48 8 70 18 57 49 72 92 11 100 68 74 46 1 30 52 97
16 84 93 3 38 8 44 8 89 34 26 57 19 48 41 99 6 87 68 86
8 4 6 6 2 3 1 3 6 4 9 10 7 1 9 7 4 8 4 8
1 4 9 3 2 1 3 6 8 1 10 3 1 9 4 7 9 7 6 5
76 782 0 0 231 340 381 3 0 730 93 0 273 114 0 0 0 0 0 0
624 0 588 0 157 0 0 0 0 21 0 760 506 69 0 0 0 127 0 184
18 65 81 68 43 4 80 92 60 86 39 90 100 25 41 42 21 90 46 32
11 5 93 45 86 45 99 72 89 37 58 6 91 65 45 41 92 63 10 78
7 8 3 4 3 5 10 6 10 2 3 6 3 5 4 9 5 5 5 10
7 10 4 6 1 2 3 4 5 2 4 2 6 3 6 1 9 8 9 10
0 637 0 0 578 572 0 0 0 390 396 0 358 0 253 0 0 94 0 0
152 878 0 237 296 0 0 714 0 588 0 677 0 362 0 0 386 0 81 388
9 61 58 50 58 86 69 25 17 73 81 5 37 33 48 18 1 34 3 92
17 95 57 62 23 88 97 63 83 38 92 36 91 24 86 23 69 78 3 70
5 4 2 8 9 1 3 7 4 3 7 3 1 6 7 3 10 9 7 9
9 9 7 1 6 8 9 9 4 6 8 8 9 5 4 9 2 6 9 8
257 0 558 0 0 516 0 585 169 0 513 0 576 0 0 653 134 0 168 0
633 0 391 87 711 694 251 0 627 0 501 222 0 637 717 0 783 797 0 0
53 96 10 66 86 76 93 77 74 90 96 26 91 48 45 88 41 13 45 40
54 1 78 62 89 82 5 36 35 77 65 51 5 63 74 95 44 68 27 60
7 10 6 8 3 8 6 10 8 3 9 8 10 8 9 5 5 4 2 4
8 4 10 10 2 2 6 10 9 4 8 9 10 4 5 5 3 10 3 6
0 0 414 395 895 454 0 0 0 0 0 562 0 0 0 0 0 208 502 719
492 689 205 0 0 0 0 0 0 369 0 387 62 0 802 592 115 492 512 0
91 87 47 96 88 88 35 72 14 48 41 23 65 76 61 72 66 30 73 40
70 25 31 57 57 25 67 51 37 51 93 56 47 74 96 8 53 20 44 48
1 1 6 9 9 10 9 3 2 4 9 3 6 5 1 7 1 1 4 2
1 6 9 8 6 2 2 2 2 5 2 8 8 7 10 5 9 6 3 6
1702 2117 2171 2067 2477 2866 1026 1652 1803 1835 1758 2600 1385 1375 2016 1910 1018 1725 1750 2637
2831 2622 1326 1596 1075 1559 771 2629 1913 2043 2335 2093 2105 761 845 2121 2131 2497 1824 2775
90 3 63 19 54 87 60 38 49 11 50 72 93 77 2 90 32 44 64 62
42 20 64 62 24 69 4 68 11 6 69 59 61 2 18 19 61 78 90 35
10 6 2 2 7 7 6 2 4 5 3 10 2 2 1 7 10 6 10 5
8 10 3 6 1 4 7 5 4 2 3 5 10 8 3 4 2 7 7 6
1077 2349 748 1107 612 1111 2393 2411 592 757 1063 1644 1522 1852 2348 1293 1657 1341 728 2475
668 1616 1020 1993 2345 1324 2337 1887 959 596 2234 725 1269 1468 1814 1230 1037 1569 2184 1571
45 68 25 21 1 95 8 6 18 95 36 49 36 66 52 67 22 64 76 75
75 94 6 96 18 16 18 54 5 44 67 74 16 44 84 87 60 34 82 28
9 3 9 3 7 4 2 7 9 1 9 1 1 5 9 1 1 3 3 2
3 7 6 1 10 6 6 6 3 5 7 5 2 4 2 9 6 10 2 8
2017 780 2268 1232 1486 1892 1167 1097 1071 1186 1160 1453 1512 1372 1281 1940 691 1653 1349 1911
1161 1034 2267 1328 1293 663 1519 708 878 1372 1157 2024 1908 2167 1378 942 689 1616 816 1200
80 57 81 87 75 84 97 9 88 69 90 36 83 9 75 30 48 53 43 56
3 7 64 81 94 25 86 76 96 20 35 14 11 52 17 74 72 39 13 35
8 3 6 8 8 1 8 7 2 1 8 1 6 1 7 7 2 9 6 5
1 5 3 7 3 8 8 5 7 10 4 1 7 2 8 9 1 9 1 4
1406 2620 1708 868 2449 1982 2382 2807 2593 1857 767 2280 2118 941 2734 1902 1750 2773 2456 850
2453 2152 2229 2372 1984 750 902 734 1181 2180 710 1712 2678 1651 2201 882 2048 2665 2413 1948
47 99 55 8 49 80 25 85 56 58 82 16 51 25 11 11 48 30 78 81
86 73 22 40 34 7 65 6 88 39 4 99 74 30 16 45 44 92 55 69
8 5 5 2 5 7 8 3 6 1 6 2 4 7 1 2 8 9 8 8
5 8 4 3 1 10 2 4 1 8 6 8 9 1 5 2 5 3 1 6
2131 2372 2386 1464 1665 2256 633 2265 2299 664 1505 1065 1060 2075 2130 791 708 1656 1194 2338
1625 2549 1222 1537 634 2421 1959 977 725 843 676 1033 1948 1700 1397 1779 1233 748 1337 1940
27 77 52 78 26 63 68 74 44 36 58 77 88 88 80 43 90 63 71 31
14 58 43 1 50 24 89 18 16 64 79 50 59 35 60 68 53 48 60 45
7 2 1 3 3 4 8 6 3 5 1 2 5 4 4 8 4 3 1 3
5 4 4 4 10 1 4 4 1 6 10 1 7 8 1 9 6 9 10 9
237 1217 1587 1994 1991 1195 1477 1525 968 1952 2371 822 413 1314 2139 1235 492 2238 755 940
259 1356 635 294 701 295 1559 1768 2369 726 1007 2290 1925 507 2085 1849 606 1743 859 2344
26 27 54 92 35 64 78 18 5 34 43 8 65 24 79 64 70 76 92 90
5 83 69 95 81 93 72 90 40 7 45 91 49 78 6 14 5 13 55 80
1 4 4 10 7 1 10 9 3 10 6 6 5 8 6 4 4 8 10 5
2 9 7 1 8 6 3 7 9 9 6 8 2 5 7 9 1 7 2 8
894 2007 1726 868 1628 2120 505 575 2001 1808 1630 2012 2263 248 1103 2307 1114 1751 1595 914
1848 367 2220 600 535 1488 2027 1040 610 2228 334 1923 1054 340 228 769 422 2079 441 264
82 36 18 50 34 69 88 66 19 33 42 4 85 12 82 13 12 44 88 45
4 20 17 56 95 85 5 4 49 36 64 50 55 23 89 58 32 50 47 97
7 8 5 1 7 4 6 4 4 10 4 2 9 4 7 2 9 6 3 10
4 5 5 2 8 5 10 8 6 5 7 6 10 1 9 6 2 6 4 8
674 456 1540 1236 1816 2008 878 1173 422 1376 244 1143 883 602 1167 285 1934 783 241 823
194 1543 568 1513 211 1447 1829 1291 1282 1186 572 2010 1924 275 722 947 1558 241 867 963
58 47 84 55 10 17 6 65 93 69 35 59 79 84 44 33 66 97 85 86
84 96 86 21 88 22 55 42 62 69 79 57 18 85 20 78 97 70 21 20
7 6 10 7 4 3 4 6 3 6 6 8 9 9 5 4 9 4 2 4
6 8 1 9 3 4 9 1 1 10 9 3 9 1 4 10 4 8 4 7
1786 896 2051 2195 254 2157 2573 2021 795 341 585 1241 1619 1215 1151 568 2437 2473 1213 1246
1907 2446 1672 1456 922 613 1896 929 2394 1623 2428 2047 490 1764 1840 397 1497 2348 1784 2266
48 54 68 13 77 100 22 69 65 31 83 74 3 26 96 72 14 17 85 7
48 89 50 30 82 80 72 91 23 81 7 47 4 35 91 55 87 41 39 76
3 4 8 9 7 5 4 10 5 3 4 3 9 10 6 3 2 8 3 4
5 2 1 2 6 5 10 1 3 4 2 10 2 4 4 7 7 4 5 1
1579 287 1273 2303 1093 2152 1853 299 1321 1075 1570 957 1683 718 697 2018 2311 1762 1056 764
1694 1301 2055 1484 1854 1925 2096 344 1691 351 1064 1454 2161 807 1741 1745 1769 1515 1533 580
72 6 63 32 78 62 99 33 97 60 22 52 45 76 47 78 63 40 70 4
26 32 63 26 30 88 79 43 6 96 46 56 8 96 72 71 21 83 42 97
7 8 2 9 3 4 2 2 3 2 3 8 8 7 6 4 5 6 5 10
3 6 7 3 6 7 4 5 9 6 1 7 3 7 4 10 1 8 6 9
1023 0 0 660 228 0 732 1145 1008 1912 1104 1101 861 1191 372 1551 1685 958 0 0
846 969 1185 1958 798 141 767 0 143 302 1448 1685 1068 123 655 649 414 1046 1680 251
78 3 41 24 83 100 84 16 84 51 69 97 18 27 86 4 50 54 100 76
75 11 57 56 13 30 80 89 14 95 71 25 56 44 8 15 45 69 50 15
7 6 8 10 7 7 4 9 1 3 2 3 4 6 5 2 4 5 9 9
2 4 2 7 1 3 8 10 2 9 2 4 4 2 3 6 4 2 5 1
94 1227 63 140 429 625 1510 1616 370 1643 1336 103 1152 1814 1462 1506 1339 195 0 1240
754 912 1291 1690 1319 1245 0 1841 677 1349 330 299 1271 589 483 1420 0 1076 39 1839
43 100 53 5 90 67 98 80 45 52 19 20 65 22 78 6 39 1 13 26
82 63 41 69 37 39 58 27 76 9 36 97 98 8 26 77 31 24 59 69
1 5 5 5 4 10 1 10 8 8 4 1 6 1 9 3 1 7 1 2
2 8 3 6 8 5 9 4 7 1 5 5 4 8 3 9 2 3 7 8
422 532 1715 1540 598 781 1339 326 1439 39 296 800 938 1552 89 1275 1747 389 823 989
1257 426 1513 1014 182 1139 1359 307 425 947 51 514 28 1541 999 64 779 1484 0 929
73 4 28 92 28 67 40 91 29 63 42 32 57 60 67 43 22 75 24 60
61 82 3 18 39 5 71 56 50 24 72 18 14 70 29 49 83 28 45 98
4 5 7 10 5 3 9 3 3 8 6 4 8 1 4 3 9 10 2 1
2 5 2 8 3 6 10 8 5 7 4 3 1 8 8 9 10 4 8 1
422 192 488 1319 1672 163 137 427 1141 674 1429 1364 676 587 993 839 363 417 179 1366
263 0 1537 691 1188 241 511 1292 697 0 1032 1714 1521 666 1478 335 0 1297 710 83
100 75 71 8 49 56 90 17 13 41 90 48 93 92 76 77 21 25 28 86
55 10 9 58 84 70 57 79 22 79 88 38 13 66 99 28 29 13 61 46
2 5 9 10 2 2 4 8 4 7 6 7 5 10 2 2 9 7 2 6
10 8 2 7 9 1 6 10 7 9 7 2 3 2 9 3 2 4 8 1
1246 152 965 1255 353 1193 1701 1284 1061 960 1505 1466 318 1651 1082 282 1048 985 400 1832
1151 243 1182 1721 861 411 1850 0 382 1578 17 0 766 1244 394 1199 1550 200 0 1856
86 27 68 77 39 46 5 28 2 91 91 86 99 21 4 73 83 52 97 18
35 47 3 49 64 28 32 1 8 65 74 9 31 84 94 14 28 65 39 58
5 8 2 3 4 1 8 5 7 8 7 4 9 9 7 7 10 7 9 2
10 4 10 10 9 5 8 1 1 3 5 7 4 6 6 10 10 8 2 3
0 0 152 1288 16 275 1087 0 462 1130 1134 805 798 1273 370 1290 0 0 495 0
199 751 1299 334 1309 735 0 0 1240 1183 1096 78 319 0 459 10 767 0 879 160
20 27 81 26 8 99 18 100 29 73 52 68 30 7 31 99 86 9 81 69
99 44 7 52 100 27 91 31 49 27 93 88 32 67 54 9 66 22 89 85
7 3 8 6 8 7 7 8 6 9 6 1 10 4 7 9 9 8 2 3
7 9 8 6 2 3 7 5 5 2 10 4 9 2 7 1 4 8 7 1
1338 923 0 770 1335 300 0 251 1167 1117 326 518 198 951 909 1494 241 0 7 360
1072 795 1055 1145 1299 0 728 0 303 785 0 0 1254 1142 1225 1178 194 467 0 1221
20 95 51 86 95 33 43 11 55 3 56 19 70 58 12 27 34 5 8 58
73 4 21 33 40 68 5 82 16 63 92 33 9 8 93 20 58 76 97 79
6 5 4 6 2 6 7 7 4 1 3 5 9 9 3 8 1 10 3 2
4 4 1 4 8 6 9 4 3 5 2 1 9 9 9 6 1 9 3 10
0 407 1105 76 733 1032 363 397 0 403 65 811 529 525 835 607 0 0 82 0
1011 710 0 747 0 1073 880 1134 393 864 882 0 1175 0 0 378 113 887 473 1207
30 3 97 91 68 17 70 40 71 46 68 65 29 38 83 31 61 100 86 6
14 85 24 60 61 6 24 68 7 24 91 5 82 56 6 54 45 71 31 96
1 7 1 5 9 7 1 7 2 6 10 4 3 10 1 7 2 10 9 6
10 5 6 3 4 7 4 2 1 7 1 5 5 9 7 8 1 5 5 5
1068 1151 1235 0 0 14 0 283 0 0 1263 269 229 0 0 23 907 79 0 0
191 683 698 1288 278 486 0 538 822 0 958 0 0 0 82 0 1142 0 359 34
26 77 17 78 22 74 68 72 92 21 27 38 47 65 56 89 28 6 98 38
3 98 73 4 69 48 78 7 51 15 91 71 100 13 65 24 100 7 34 94
7 4 1 3 3 6 5 2 10 8 5 6 8 3 8 7 4 3 10 1
6 5 4 4 6 10 5 3 9 7 1 5 7 2 4 9 7 5 10 5
557 1428 0 0 0 759 0 0 0 0 0 0 904 909 0 500 0 1016 0 1431
0 916 719 290 1306 0 19 543 64 599 891 67 150 548 609 0 1338 493 1399 739
8 97 86 87 82 81 86 93 65 3 53 72 92 8 22 81 24 92 8 83
53 6 1 40 96 54 73 22 100 92 71 99 40 31 21 45 19 33 28 37
10 10 2 10 4 7 5 9 5 8 8 10 8 9 6 3 8 8 9 6
8 1 1 9 9 1 8 4 10 4 1 1 10 5 2 4 5 3 9 6
378 913 0 0 534 0 91 0 0 461 0 191 0 48 690 945 0 0 0 0
0 140 0 0 261 719 927 0 0 0 0 881 241 0 0 0 0 0 0 675
7 95 56 62 98 66 47 95 63 17 43 4 58 89 50 92 67 76 56 69
2 26 23 46 3 38 93 37 40 67 86 59 7 19 1 35 31 54 14 88
4 5 5 9 4 6 5 2 4 4 1 8 7 2 10 9 4 9 2 9
4 9 4 1 5 4 3 1 3 9 1 4 2 8 3 7 6 9 7 9
266 139 686 373 572 37 0 376 716 0 558 0 0 0 0 0 0 0 63 0
473 0 819 0 316 0 634 151 0 574 52 0 0 0 796 0 665 0 140 401
81 57 60 48 52 13 56 70 89 43 72 73 71 86 88 8 3 32 61 32
19 27 28 1 81 66 1 78 80 2 73 27 34 36 13 16 90 27 70 16
10 3 2 4 10 9 10 10 2 9 2 10 7 7 8 10 10 8 1 9
8 9 6 3 5 8 4 2 5 1 7 5 7 9 3 5 2 2 2 2
0 350 627 0 383 122 936 804 0 875 357 252 0 0 0 0 111 0 935 0
871 0 0 0 0 0 0 131 282 0 0 416 848 0 0 542 247 0 376 0
15 21 8 96 50 55 94 15 72 12 94 23 81 26 60 20 4 86 22 7
98 32 86 91 46 59 38 78 60 14 42 80 82 98 41 13 79 63 53 93
8 5 2 9 9 4 9 1 3 2 2 9 6 9 3 4 2 3 7 6
3 7 10 9 10 8 6 5 2 3 7 8 7 2 2 3 1 2 4 7
0 740 0 0 571 272 0 0 0 0 0 870 845 765 668 208 0 281 745 0
0 0 0 799 555 537 595 752 572 0 41 0 258 61 0 0 933 1021 0 778
26 78 87 57 31 82 20 28 71 10 41 1 69 94 71 21 74 17 12 37
63 19 43 1 44 89 23 69 49 74 86 99 41 69 47 52 10 25 97 93
7 8 5 8 6 9 3 4 8 8 4 8 4 5 1 6 5 7 8 3
10 5 7 6 6 7 9 10 9 8 2 6 3 6 4 10 2 9 9 5
506 0 0 197 0 0 772 818 660 0 801 420 0 593 0 249 0 0 292 0
469 122 0 719 42 152 0 824 241 0 0 966 0 0 0 0 430 0 814 0

1127
examples/data/weighted_tardiness/wt50.txt Normal file
View File

File diff suppressed because it is too large Load Diff

27
makefiles/Makefile.cpp.mk
View File

@@ -1,7 +1,7 @@
# Makefile targets.
# Main target
cc: ortoolslibs cpexe lpexe
cc: ortoolslibs ccexe
# Clean target
@@ -101,7 +101,7 @@ FLATZINC_LNK = $(PRE_LIB)fz$(POST_LIB) $(OR_TOOLS_LNK)
# Binaries
CP_BINARIES = \
CC_BINARIES = \
$(BIN_DIR)/costas_array$E \
$(BIN_DIR)/cryptarithm$E \
$(BIN_DIR)/cvrp_disjoint_tw$E \
@@ -114,6 +114,8 @@ CP_BINARIES = \
$(BIN_DIR)/golomb$E \
$(BIN_DIR)/jobshop$E \
$(BIN_DIR)/jobshop_ls$E \
$(BIN_DIR)/jobshop_sat$E \
$(BIN_DIR)/jobshop_earlytardy \
$(BIN_DIR)/linear_assignment_api$E \
$(BIN_DIR)/ls_api$E \
$(BIN_DIR)/magic_square$E \
@@ -124,9 +126,8 @@ CP_BINARIES = \
$(BIN_DIR)/pdptw$E \
$(BIN_DIR)/dimacs_assignment$E \
$(BIN_DIR)/sports_scheduling$E \
$(BIN_DIR)/tsp$E
LP_BINARIES = \
$(BIN_DIR)/tsp$E \
$(BIN_DIR)/weighted_tardiness_sat \
$(BIN_DIR)/integer_programming$E \
$(BIN_DIR)/linear_programming$E \
$(BIN_DIR)/linear_solver_protocol_buffers$E \
@@ -134,9 +135,7 @@ LP_BINARIES = \
$(BIN_DIR)/mps_driver$E \
$(BIN_DIR)/solve$E
cpexe: $(CP_BINARIES)
lpexe: $(LP_BINARIES)
ccexe: $(CC_BINARIES)
# CVRPTW common library
@@ -364,6 +363,12 @@ $(OBJ_DIR)/jobshop_earlytardy.$O: $(EX_DIR)/cpp/jobshop_earlytardy.cc $(EX_DIR)/
$(BIN_DIR)/jobshop_earlytardy$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/jobshop_earlytardy.$O
$(CCC) $(CFLAGS) $(OBJ_DIR)/jobshop_earlytardy.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sjobshop_earlytardy$E
$(OBJ_DIR)/jobshop_sat.$O: $(EX_DIR)/cpp/jobshop_sat.cc $(CP_DEPS)
$(CCC) $(CFLAGS) -c $(EX_DIR)$Scpp/jobshop_sat.cc $(OBJ_OUT)$(OBJ_DIR)$Sjobshop_sat.$O
$(BIN_DIR)/jobshop_sat$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/jobshop_sat.$O
$(CCC) $(CFLAGS) $(OBJ_DIR)/jobshop_sat.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sjobshop_sat$E
$(OBJ_DIR)/magic_square.$O: $(EX_DIR)/cpp/magic_square.cc $(CP_DEPS)
$(CCC) $(CFLAGS) -c $(EX_DIR)$Scpp/magic_square.cc $(OBJ_OUT)$(OBJ_DIR)$Smagic_square.$O
@@ -424,6 +429,12 @@ $(OBJ_DIR)/tsp.$O: $(EX_DIR)/cpp/tsp.cc $(ROUTING_DEPS)
$(BIN_DIR)/tsp$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/tsp.$O
$(CCC) $(CFLAGS) $(OBJ_DIR)/tsp.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Stsp$E
$(OBJ_DIR)/weighted_tardiness_sat.$O: $(EX_DIR)/cpp/weighted_tardiness_sat.cc $(CP_DEPS)
$(CCC) $(CFLAGS) -c $(EX_DIR)$Scpp/weighted_tardiness_sat.cc $(OBJ_OUT)$(OBJ_DIR)$Sweighted_tardiness_sat.$O
$(BIN_DIR)/weighted_tardiness_sat$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/weighted_tardiness_sat.$O
$(CCC) $(CFLAGS) $(OBJ_DIR)/weighted_tardiness_sat.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS) $(EXE_OUT)$(BIN_DIR)$Sweighted_tardiness_sat$E
# CP tests.
$(OBJ_DIR)/bug_pack.$O: $(EX_DIR)/tests/bug_pack.cc $(CP_DEPS)

67
makefiles/Makefile.gen.mk
View File

@@ -1294,8 +1294,10 @@ SAT_DEPS = \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/sat/sat_solver.h \
@@ -1355,12 +1357,17 @@ SAT_DEPS = \
SAT_LIB_OBJS = \
$(OBJ_DIR)/sat/boolean_problem.$O \
$(OBJ_DIR)/sat/clause.$O \
$(OBJ_DIR)/sat/disjunctive.$O \
$(OBJ_DIR)/sat/drat.$O \
$(OBJ_DIR)/sat/encoding.$O \
$(OBJ_DIR)/sat/integer.$O \
$(OBJ_DIR)/sat/integer_sum.$O \
$(OBJ_DIR)/sat/intervals.$O \
$(OBJ_DIR)/sat/lp_utils.$O \
$(OBJ_DIR)/sat/no_cycle.$O \
$(OBJ_DIR)/sat/optimization.$O \
$(OBJ_DIR)/sat/pb_constraint.$O \
$(OBJ_DIR)/sat/precedences.$O \
$(OBJ_DIR)/sat/sat_solver.$O \
$(OBJ_DIR)/sat/simplification.$O \
$(OBJ_DIR)/sat/symmetry.$O \
@@ -1388,6 +1395,14 @@ $(SRC_DIR)/sat/clause.h: \
$(SRC_DIR)/util/bitset.h \
$(SRC_DIR)/util/stats.h
$(SRC_DIR)/sat/disjunctive.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
$(SRC_DIR)/util/stats.h
$(SRC_DIR)/sat/drat.h: \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h \
@@ -1405,6 +1420,18 @@ $(SRC_DIR)/sat/integer.h: \
$(SRC_DIR)/util/bitset.h \
$(SRC_DIR)/util/iterators.h
$(SRC_DIR)/sat/integer_sum.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h
$(SRC_DIR)/sat/intervals.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
$(SRC_DIR)/sat/sat_solver.h
$(SRC_DIR)/sat/lp_utils.h: \
$(GEN_DIR)/sat/boolean_problem.pb.h \
$(SRC_DIR)/sat/sat_solver.h \
@@ -1415,6 +1442,11 @@ $(SRC_DIR)/sat/model.h: \
$(SRC_DIR)/base/map_util.h \
$(SRC_DIR)/base/typeid.h
$(SRC_DIR)/sat/no_cycle.h: \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h \
$(SRC_DIR)/sat/sat_solver.h
$(SRC_DIR)/sat/optimization.h: \
$(SRC_DIR)/sat/boolean_problem.h \
$(SRC_DIR)/sat/integer.h \
@@ -1426,6 +1458,13 @@ $(SRC_DIR)/sat/pb_constraint.h: \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/util/stats.h
$(SRC_DIR)/sat/precedences.h: \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/sat_base.h \
$(SRC_DIR)/sat/sat_solver.h \
$(SRC_DIR)/util/bitset.h
$(SRC_DIR)/sat/sat_base.h: \
$(SRC_DIR)/base/int_type.h \
$(SRC_DIR)/base/int_type_indexed_vector.h \
@@ -1486,6 +1525,11 @@ $(OBJ_DIR)/sat/clause.$O: \
$(SRC_DIR)/util/time_limit.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/clause.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sclause.$O
$(OBJ_DIR)/sat/disjunctive.$O: \
$(SRC_DIR)/sat/disjunctive.h \
$(SRC_DIR)/sat/sat_solver.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/disjunctive.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdisjunctive.$O
$(OBJ_DIR)/sat/drat.$O: \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/base/commandlineflags.h
@@ -1500,6 +1544,14 @@ $(OBJ_DIR)/sat/integer.$O: \
$(SRC_DIR)/base/stl_util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/integer.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sinteger.$O
$(OBJ_DIR)/sat/integer_sum.$O: \
$(SRC_DIR)/sat/integer_sum.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/integer_sum.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sinteger_sum.$O
$(OBJ_DIR)/sat/intervals.$O: \
$(SRC_DIR)/sat/intervals.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/intervals.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sintervals.$O
$(OBJ_DIR)/sat/lp_utils.$O: \
$(SRC_DIR)/sat/boolean_problem.h \
$(SRC_DIR)/sat/lp_utils.h \
@@ -1508,6 +1560,11 @@ $(OBJ_DIR)/sat/lp_utils.$O: \
$(SRC_DIR)/glop/lp_solver.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/lp_utils.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Slp_utils.$O
$(OBJ_DIR)/sat/no_cycle.$O: \
$(SRC_DIR)/sat/no_cycle.h \
$(SRC_DIR)/base/stl_util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/no_cycle.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sno_cycle.$O
$(OBJ_DIR)/sat/optimization.$O: \
$(SRC_DIR)/sat/encoding.h \
$(SRC_DIR)/sat/optimization.h
@@ -1519,6 +1576,12 @@ $(OBJ_DIR)/sat/pb_constraint.$O: \
$(SRC_DIR)/util/saturated_arithmetic.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/pb_constraint.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Spb_constraint.$O
$(OBJ_DIR)/sat/precedences.$O: \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/base/cleanup.h \
$(SRC_DIR)/base/stl_util.h
$(CCC) $(CFLAGS) -c $(SRC_DIR)/sat/precedences.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sprecedences.$O
$(OBJ_DIR)/sat/sat_solver.$O: \
$(SRC_DIR)/sat/sat_solver.h \
$(SRC_DIR)/base/integral_types.h \
@@ -1611,8 +1674,10 @@ BOP_DEPS = \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/sat/sat_solver.h \
@@ -2128,8 +2193,10 @@ CP_DEPS = \
$(SRC_DIR)/sat/clause.h \
$(SRC_DIR)/sat/drat.h \
$(SRC_DIR)/sat/integer.h \
$(SRC_DIR)/sat/intervals.h \
$(SRC_DIR)/sat/model.h \
$(SRC_DIR)/sat/pb_constraint.h \
$(SRC_DIR)/sat/precedences.h \
$(SRC_DIR)/sat/sat_base.h \
$(GEN_DIR)/sat/sat_parameters.pb.h \
$(SRC_DIR)/sat/sat_solver.h \

874
src/sat/disjunctive.cc Normal file
View File

@@ -0,0 +1,874 @@
// Copyright 2010-2014 Google
// 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.
#include "sat/disjunctive.h"
//#include "base/iterator_adaptors.h"
#include "sat/sat_solver.h"
namespace operations_research {
namespace sat {
std::function<void(Model*)> DisjunctiveWithBooleanPrecedences(
const std::vector<IntervalVariable>& vars) {
return [=](Model* model) {
SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
for (int i = 0; i < vars.size(); ++i) {
for (int j = 0; j < i; ++j) {
const BooleanVariable boolean_var = sat_solver->NewBooleanVariable();
const Literal i_before_j = Literal(boolean_var, true);
const Literal j_before_i = i_before_j.Negated();
precedences->AddConditionalPrecedence(intervals->EndVar(vars[i]),
intervals->StartVar(vars[j]),
i_before_j);
precedences->AddConditionalPrecedence(intervals->EndVar(vars[j]),
intervals->StartVar(vars[i]),
j_before_i);
}
}
DisjunctiveConstraint* disjunctive = new DisjunctiveConstraint(
vars, model->GetOrCreate<IntegerTrail>(), intervals, precedences);
disjunctive->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
disjunctive->SetParameters(sat_solver->parameters());
model->TakeOwnership(disjunctive);
};
}
void TaskSet::AddEntry(const Entry& e) {
sorted_tasks_.push_back(e);
int j = static_cast<int>(sorted_tasks_.size()) - 1;
while (j > 0 && sorted_tasks_[j - 1].min_start > e.min_start) {
sorted_tasks_[j] = sorted_tasks_[j - 1];
--j;
}
sorted_tasks_[j] = e;
DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
// If the task is added after optimized_restart_, we know that we don't need
// to scan the task before optimized_restart_ in the next ComputeMinEnd().
if (j <= optimized_restart_) optimized_restart_ = 0;
}
void TaskSet::AddOrderedLastEntry(const Entry& e) {
if (DEBUG_MODE && !sorted_tasks_.empty()) {
CHECK_GE(e.min_start, sorted_tasks_.back().min_start);
}
sorted_tasks_.push_back(e);
}
// Note that we can keep the optimized_restart_ at its current value here.
void TaskSet::NotifyEntryIsNowLastIfPresent(const Entry& e) {
const int size = sorted_tasks_.size();
for (int i = 0;; ++i) {
if (i == size) return;
if (sorted_tasks_[i].task == e.task) {
sorted_tasks_.erase(sorted_tasks_.begin() + i);
break;
}
}
sorted_tasks_.push_back(e);
DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
}
void TaskSet::RemoveEntryWithIndex(int index) {
sorted_tasks_.erase(sorted_tasks_.begin() + index);
optimized_restart_ = 0;
}
int TaskSet::ComputeMinEnd(int task_to_ignore, int* critical_index) const {
// The order in which we process tasks with the same min-start doesn't matter.
DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
bool ignored = false;
const int size = sorted_tasks_.size();
int min_end = std::numeric_limits<int>::min();
for (int i = optimized_restart_; i < size; ++i) {
const Entry& e = sorted_tasks_[i];
if (e.task == task_to_ignore) {
ignored = true;
continue;
}
if (e.min_start >= min_end) {
*critical_index = i;
if (!ignored) optimized_restart_ = i;
min_end = e.min_start + e.min_duration;
} else {
min_end += e.min_duration;
}
}
return min_end;
}
DisjunctiveConstraint::DisjunctiveConstraint(
const std::vector<IntervalVariable>& non_overlapping_intervals,
IntegerTrail* integer_trail, IntervalsRepository* intervals,
PrecedencesPropagator* precedences)
: non_overlapping_intervals_(non_overlapping_intervals),
integer_trail_(integer_trail),
intervals_(intervals),
precedences_(precedences),
stats_("DisjunctiveConstraint") {}
void DisjunctiveConstraint::SwitchToMirrorProblem() {
std::swap(start_vars_, minus_end_vars_);
std::swap(end_vars_, minus_start_vars_);
std::swap(task_by_increasing_min_start_, task_by_decreasing_max_end_);
std::swap(task_by_increasing_min_end_, task_by_decreasing_max_start_);
std::swap(before_, after_);
}
bool DisjunctiveConstraint::Propagate(Trail* trail) {
SCOPED_TIME_STAT(&stats_);
start_vars_.clear();
end_vars_.clear();
minus_end_vars_.clear();
minus_start_vars_.clear();
duration_vars_.clear();
fixed_durations_.clear();
reason_for_presence_.clear();
task_is_currently_present_.clear();
for (const IntervalVariable i : non_overlapping_intervals_) {
if (intervals_->IsOptional(i)) {
const Literal l = intervals_->IsPresentLiteral(i);
if (trail->Assignment().LiteralIsFalse(l)) continue;
task_is_currently_present_.push_back(
trail->Assignment().LiteralIsTrue(l));
reason_for_presence_.push_back(l.Index());
} else {
task_is_currently_present_.push_back(true);
reason_for_presence_.push_back(kNoLiteralIndex);
}
if (intervals_->SizeVar(i) == kNoIntegerVariable) {
duration_vars_.push_back(kNoLbVar);
fixed_durations_.push_back(intervals_->FixedSize(i));
} else {
duration_vars_.push_back(LbVarOf(intervals_->SizeVar(i)));
fixed_durations_.push_back(0);
}
start_vars_.push_back(LbVarOf(intervals_->StartVar(i)));
minus_end_vars_.push_back(MinusUbVarOf(intervals_->EndVar(i)));
// For the precedences computation.
if (intervals_->IsOptional(i) && !task_is_currently_present_.back()) {
// If the task presence is unknow, we don't take it into account.
// We however insest a kNoLbVar so the indices are still valid.
end_vars_.push_back(kNoLbVar);
minus_start_vars_.push_back(kNoLbVar);
} else {
end_vars_.push_back(LbVarOf(intervals_->EndVar(i)));
minus_start_vars_.push_back(MinusUbVarOf(intervals_->StartVar(i)));
}
}
// Because this class doesn't add any new precedences, we can compute the
// set of task before (and after) some LbVar only once before we enter the
// propagation loop below.
if (parameters_.use_precedences_in_disjunctive_constraint()) {
precedences_->ComputePrecedences(end_vars_, &before_);
precedences_->ComputePrecedences(minus_start_vars_, &after_);
}
// This is variable as it depends on the optional tasks that are present.
const int num_tasks = start_vars_.size();
DCHECK_EQ(num_tasks, minus_end_vars_.size());
DCHECK_EQ(num_tasks, duration_vars_.size());
DCHECK_EQ(num_tasks, fixed_durations_.size());
DCHECK_EQ(num_tasks, reason_for_presence_.size());
DCHECK_EQ(num_tasks, task_is_currently_present_.size());
// Initialize our "order" vectors with all the task indices.
if (task_by_increasing_min_start_.size() != num_tasks) {
task_by_increasing_min_start_.resize(num_tasks);
task_by_increasing_min_end_.resize(num_tasks);
task_by_decreasing_max_start_.resize(num_tasks);
task_by_decreasing_max_end_.resize(num_tasks);
for (int t = 0; t < num_tasks; ++t) {
task_by_increasing_min_start_[t] = t;
task_by_increasing_min_end_[t] = t;
task_by_decreasing_max_start_[t] = t;
task_by_decreasing_max_end_[t] = t;
}
}
// Loop until we reach the fixed-point. It should be unique (see Petr Villim
// PhD).
while (true) {
const int64 old_timestamp = integer_trail_->num_enqueues();
// This one is symmetric so there is no need to do it backward in time too.
// It only detects conflict, it never propagates anything.
if (!OverloadCheckingPass(integer_trail_, trail)) return false;
if (!DetectablePrecedencePass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (!DetectablePrecedencePass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (old_timestamp != integer_trail_->num_enqueues()) continue;
if (!NotLastPass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (!NotLastPass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (old_timestamp != integer_trail_->num_enqueues()) continue;
if (!EdgeFindingPass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (!EdgeFindingPass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (old_timestamp != integer_trail_->num_enqueues()) continue;
if (parameters_.use_precedences_in_disjunctive_constraint()) {
if (!PrecedencePass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (!PrecedencePass(integer_trail_, trail)) return false;
SwitchToMirrorProblem();
if (old_timestamp != integer_trail_->num_enqueues()) continue;
}
break;
}
return true;
}
void DisjunctiveConstraint::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntervalVariable i : non_overlapping_intervals_) {
watcher->WatchLbVar(LbVarOf(intervals_->StartVar(i)), id);
watcher->WatchLbVar(MinusUbVarOf(intervals_->EndVar(i)), id);
if (intervals_->SizeVar(i) != kNoIntegerVariable) {
watcher->WatchLbVar(LbVarOf(intervals_->SizeVar(i)), id);
}
if (intervals_->IsOptional(i)) {
watcher->WatchLiteral(intervals_->IsPresentLiteral(i), id);
}
}
}
void DisjunctiveConstraint::AddPresenceAndDurationReason(int t) {
if (reason_for_presence_[t] != kNoLiteralIndex) {
literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated());
}
if (duration_vars_[t] != kNoLbVar) {
integer_reason_.push_back(
integer_trail_->ValueAsLiteral(duration_vars_[t]));
}
}
void DisjunctiveConstraint::AddMinDurationReason(int t) {
if (duration_vars_[t] != kNoLbVar) {
integer_reason_.push_back(
integer_trail_->ValueAsLiteral(duration_vars_[t]));
}
}
void DisjunctiveConstraint::AddMinStartReason(int t, int lower_bound) {
integer_reason_.push_back(
IntegerLiteral::FromLbVar(start_vars_[t], lower_bound));
}
void DisjunctiveConstraint::AddMaxEndReason(int t, int upper_bound) {
integer_reason_.push_back(
IntegerLiteral::FromLbVar(minus_end_vars_[t], -upper_bound));
}
bool DisjunctiveConstraint::CheckIntervalForConflict(int t, Trail* trail) {
if (MinStart(t) + MinDuration(t) > MaxEnd(t)) {
integer_reason_.clear();
integer_reason_.push_back(integer_trail_->ValueAsLiteral(start_vars_[t]));
integer_reason_.push_back(
integer_trail_->ValueAsLiteral(minus_end_vars_[t]));
if (duration_vars_[t] != kNoLbVar) {
integer_reason_.push_back(
integer_trail_->ValueAsLiteral(duration_vars_[t]));
}
if (!task_is_currently_present_[t]) {
// We can propagate reason_for_presence_[t] to false.
// Note that it could have been already propagated in which case we do
// nothing.
if (trail->Assignment().LiteralIsFalse(
Literal(reason_for_presence_[t]))) {
return true;
}
DCHECK_NE(reason_for_presence_[t], kNoLiteralIndex);
literal_reason_.clear();
integer_trail_->EnqueueLiteral(Literal(reason_for_presence_[t]).Negated(),
literal_reason_, integer_reason_, trail);
return true;
} else {
// Conflict.
std::vector<Literal>* conflict = trail->MutableConflict();
conflict->clear();
if (reason_for_presence_[t] != kNoLiteralIndex) {
conflict->push_back(Literal(reason_for_presence_[t]).Negated());
}
integer_trail_->MergeReasonInto(integer_reason_, conflict);
return false;
}
}
return true;
}
// Experiments showed that checking first if the array is sorted resulted in
// about 15% of speed gain. This is not that surprising because these vectors
// are often already sorted.
void DisjunctiveConstraint::UpdateTaskByIncreasingMinStart() {
// TODO(user): tie-breaking?
if (!std::is_sorted(
task_by_increasing_min_start_.begin(),
task_by_increasing_min_start_.end(),
[this](int t1, int t2) { return MinStart(t1) < MinStart(t2); })) {
std::stable_sort(
task_by_increasing_min_start_.begin(),
task_by_increasing_min_start_.end(),
[this](int t1, int t2) { return MinStart(t1) < MinStart(t2); });
}
}
void DisjunctiveConstraint::UpdateTaskByIncreasingMinEnd() {
// TODO(user): tie-breaking?
if (!std::is_sorted(
task_by_increasing_min_end_.begin(),
task_by_increasing_min_end_.end(),
[this](int t1, int t2) { return MinEnd(t1) < MinEnd(t2); })) {
std::stable_sort(
task_by_increasing_min_end_.begin(), task_by_increasing_min_end_.end(),
[this](int t1, int t2) { return MinEnd(t1) < MinEnd(t2); });
}
}
void DisjunctiveConstraint::UpdateTaskByDecreasingMaxStart() {
// TODO(user): tie-breaking?
if (!std::is_sorted(
task_by_decreasing_max_start_.begin(),
task_by_decreasing_max_start_.end(),
[this](int t1, int t2) { return MaxStart(t1) > MaxStart(t2); })) {
std::stable_sort(
task_by_decreasing_max_start_.begin(),
task_by_decreasing_max_start_.end(),
[this](int t1, int t2) { return MaxStart(t1) > MaxStart(t2); });
}
}
void DisjunctiveConstraint::UpdateTaskByDecreasingMaxEnd() {
// TODO(user): tie-breaking?
if (!std::is_sorted(
task_by_decreasing_max_end_.begin(),
task_by_decreasing_max_end_.end(),
[this](int t1, int t2) { return MaxEnd(t1) > MaxEnd(t2); })) {
std::stable_sort(
task_by_decreasing_max_end_.begin(), task_by_decreasing_max_end_.end(),
[this](int t1, int t2) { return MaxEnd(t1) > MaxEnd(t2); });
}
}
bool DisjunctiveConstraint::OverloadCheckingPass(IntegerTrail* integer_trail,
Trail* trail) {
SCOPED_TIME_STAT(&stats_);
UpdateTaskByDecreasingMaxEnd();
task_set_.Clear();
for (auto it = task_by_decreasing_max_end_.rbegin();
it != task_by_decreasing_max_end_.rend(); ++it) {
const int t = *it;
if (task_is_currently_present_[t]) {
task_set_.AddEntry({t, MinStart(t), MinDuration(t)});
}
int critical_index = 0;
const int min_end_of_critical_tasks =
task_set_.ComputeMinEnd(/*task_to_ignore=*/-1, &critical_index);
const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
// Check if we can detect that this optional task can't be executed.
// TODO(user): This test doesn't detect all the cases. A better way to do
// it would be like in the EdgeFindingPass() with the concept of gray tasks.
if (!task_is_currently_present_[t] && !sorted_tasks.empty()) {
// Skip if it was already shown not to be there.
if (trail->Assignment().LiteralIsFalse(
Literal(reason_for_presence_[t]))) {
continue;
}
const int critical_start = sorted_tasks[critical_index].min_start;
if (MinEnd(t) <= critical_start) continue;
const int new_min_end =
MinStart(t) >= critical_start
? min_end_of_critical_tasks + MinDuration(t)
: min_end_of_critical_tasks + MinEnd(t) - critical_start;
if (new_min_end > MaxEnd(t)) {
// TODO(user): This could be done lazily, like most of the loop to
// compute the reasons in this class.
integer_reason_.clear();
literal_reason_.clear();
const int window_start =
std::min(MinStart(t), sorted_tasks[critical_index].min_start);
const int window_end = new_min_end - 1;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
AddMaxEndReason(ct, window_end);
}
AddMinDurationReason(t);
AddMinStartReason(t, window_start);
AddMaxEndReason(t, window_end);
DCHECK_NE(reason_for_presence_[t], kNoLiteralIndex);
integer_trail->EnqueueLiteral(
Literal(reason_for_presence_[t]).Negated(), literal_reason_,
integer_reason_, trail);
}
}
// Overload checking.
if (min_end_of_critical_tasks > MaxEnd(t)) {
DCHECK(task_is_currently_present_[t]);
literal_reason_.clear();
integer_reason_.clear();
const int window_start = sorted_tasks[critical_index].min_start;
const int window_end = min_end_of_critical_tasks - 1;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
AddMaxEndReason(ct, window_end);
}
std::vector<Literal>* conflict = trail->MutableConflict();
*conflict = literal_reason_;
integer_trail->MergeReasonInto(integer_reason_, conflict);
return false;
}
}
return true;
}
bool DisjunctiveConstraint::DetectablePrecedencePass(
IntegerTrail* integer_trail, Trail* trail) {
SCOPED_TIME_STAT(&stats_);
UpdateTaskByIncreasingMinEnd();
UpdateTaskByDecreasingMaxStart();
const int num_tasks = start_vars_.size();
int queue_index = num_tasks - 1;
task_set_.Clear();
for (const int t : task_by_increasing_min_end_) {
const int min_end = MinEnd(t);
while (queue_index >= 0) {
const int to_insert = task_by_decreasing_max_start_[queue_index];
if (min_end <= MaxStart(to_insert)) break;
if (task_is_currently_present_[to_insert]) {
task_set_.AddEntry(
{to_insert, MinStart(to_insert), MinDuration(to_insert)});
}
--queue_index;
}
// task_set_ contains all the tasks that must be executed before t.
// They are in "dectable precedence" because their max_start is smaller than
// the min-end of t like so:
// [(the task t)
// (a task in task_set_)]
// From there, we deduce that the min-start of t is greater or equal to the
// min-end of the critical tasks.
//
// Note that this works as well when task_is_currently_present_[t] is false.
int critical_index = 0;
const int min_end_of_critical_tasks =
task_set_.ComputeMinEnd(/*task_to_ignore=*/t, &critical_index);
if (min_end_of_critical_tasks > MinStart(t)) {
const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
literal_reason_.clear();
integer_reason_.clear();
// We need:
// - MaxStart(ct) < MinEnd(t) for the detectable precedence
// - MinStart(ct) > window_start for the min_end_of_critical_tasks reason.
const int window_start = sorted_tasks[critical_index].min_start;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
if (ct == t) continue;
DCHECK(task_is_currently_present_[ct]);
DCHECK_GE(MinStart(ct), window_start);
DCHECK_LT(MaxStart(ct), min_end);
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
AddMaxEndReason(ct, min_end + MinDuration(ct) - 1);
}
// Add the reason for t (we don't need the max-end or presence reason).
AddMinDurationReason(t);
AddMinStartReason(t, MinStart(t));
// This augment the min-start of t and subsequently it can augment the
// next min_end_of_critical_tasks, but our deduction is still valid.
integer_trail->Enqueue(
IntegerLiteral::FromLbVar(start_vars_[t], min_end_of_critical_tasks),
literal_reason_, integer_reason_);
if (!CheckIntervalForConflict(t, trail)) return false;
// We need to reorder t inside task_set_.
task_set_.NotifyEntryIsNowLastIfPresent({t, MinStart(t), MinDuration(t)});
}
}
return true;
}
bool DisjunctiveConstraint::PrecedencePass(IntegerTrail* integer_trail,
Trail* trail) {
SCOPED_TIME_STAT(&stats_);
const int num_tasks = start_vars_.size();
// We don't care about the initial content of this vector.
reason_for_beeing_before_.resize(num_tasks, kNoLiteralIndex);
int critical_index;
const int size = before_.size();
for (int i = 0; i < size;) {
const LbVar var = before_[i].var;
DCHECK_NE(var, kNoLbVar);
task_set_.Clear();
for (; i < size && before_[i].var == var; ++i) {
const int task = before_[i].index;
reason_for_beeing_before_[task] = before_[i].reason;
task_set_.AddUnsortedEntry({task, MinStart(task), MinDuration(task)});
}
if (task_set_.SortedTasks().size() < 2) continue;
task_set_.Sort();
const int min_end =
task_set_.ComputeMinEnd(/*task_to_ignore=*/-1, &critical_index);
if (min_end > integer_trail_->ValueAsLiteral(var).bound) {
const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
literal_reason_.clear();
integer_reason_.clear();
const int window_start = sorted_tasks[critical_index].min_start;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
DCHECK(task_is_currently_present_[ct]);
DCHECK_GE(MinStart(ct), window_start);
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
if (reason_for_beeing_before_[ct] != kNoLiteralIndex) {
literal_reason_.push_back(
Literal(reason_for_beeing_before_[ct]).Negated());
}
}
integer_trail->Enqueue(IntegerLiteral::FromLbVar(var, min_end),
literal_reason_, integer_reason_);
// TODO(user): for non-optional intervals, we could check right away that
// the domain of var is non-empty. Or for a var that correspond to one
// of the interval bounds, we could detect infeasibility early with
// CheckIntervalForConflict(). Not doing should be fine, it just postpone
// a bit the conflict detection.
}
}
return true;
}
bool DisjunctiveConstraint::NotLastPass(IntegerTrail* integer_trail,
Trail* trail) {
SCOPED_TIME_STAT(&stats_);
UpdateTaskByDecreasingMaxStart();
UpdateTaskByDecreasingMaxEnd();
const int num_tasks = start_vars_.size();
int queue_index = num_tasks - 1;
task_set_.Clear();
for (auto it = task_by_decreasing_max_end_.rbegin();
it != task_by_decreasing_max_end_.rend(); ++it) {
const int t = *it;
const int max_end = MaxEnd(t);
while (queue_index >= 0) {
const int to_insert = task_by_decreasing_max_start_[queue_index];
if (max_end <= MaxStart(to_insert)) break;
if (task_is_currently_present_[to_insert]) {
task_set_.AddEntry(
{to_insert, MinStart(to_insert), MinDuration(to_insert)});
}
--queue_index;
}
// In the following case, task t cannot be after all the critical tasks
// (i.e. it cannot be last):
//
// [(critical tasks)
// (duration_t)]
//
// So we can deduce that the max-end of t is smaller that the largest
// max-start of the critical tasks.
//
// Note that this works as well when task_is_currently_present_[t] is false.
int critical_index = 0;
const int min_end_of_critical_tasks =
task_set_.ComputeMinEnd(/*task_to_ignore=*/t, &critical_index);
if (min_end_of_critical_tasks <= MaxStart(t)) continue;
// Find the largest max-start of the critical tasks (excluding t). This
// will be a valid new max-end for t.
int new_max_end = -1;
int task_responsible_for_new_max_end = -1;
const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
if (t == ct) continue;
const int max_start = MaxStart(ct);
if (max_start > new_max_end) {
new_max_end = max_start;
task_responsible_for_new_max_end = ct;
}
}
if (max_end > new_max_end) {
literal_reason_.clear();
integer_reason_.clear();
// We don't need the max-end reason of the critical tasks except the
// one for the task responsible for new_max_end.
const int window_start = sorted_tasks[critical_index].min_start;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
if (ct == t) continue;
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
if (ct == task_responsible_for_new_max_end) {
AddMaxEndReason(ct, MaxEnd(ct));
}
}
// Add the reason for t (we don't need the min-start or presence reason).
AddMinDurationReason(t);
AddMaxEndReason(t, min_end_of_critical_tasks + MinDuration(t) - 1);
// Enqueue the new max-end for t.
// Note that changing it will not influence the rest of the loop.
integer_trail->Enqueue(
IntegerLiteral::FromLbVar(minus_end_vars_[t], -new_max_end),
literal_reason_, integer_reason_);
if (!CheckIntervalForConflict(t, trail)) return false;
}
}
return true;
}
bool DisjunctiveConstraint::EdgeFindingPass(IntegerTrail* integer_trail,
Trail* trail) {
SCOPED_TIME_STAT(&stats_);
const int num_tasks = start_vars_.size();
// Some task in sorted_tasks_ will be considered "gray".
// When computing the min-end of the sorted task, we will compute it for:
// - All the non-gray task
// - All the non-gray task + at most one gray task.
is_gray_.resize(num_tasks, false);
// The algorithm is slightly different than the others. We start with a full
// sorted_tasks, and remove tasks one by one starting by the one with highest
// max-end.
task_set_.Clear();
UpdateTaskByIncreasingMinStart();
int num_not_gray = 0;
for (const int t : task_by_increasing_min_start_) {
task_set_.AddOrderedLastEntry({t, MinStart(t), MinDuration(t)});
// We already mark all the non-present task as gray.
if (task_is_currently_present_[t]) {
++num_not_gray;
is_gray_[t] = false;
} else {
is_gray_[t] = true;
}
}
UpdateTaskByDecreasingMaxEnd();
int decreasing_max_end_index = 0;
// At each iteration we either transform a non-gray task into a gray one or
// remove a gray task, so this loop is linear in complexity.
while (num_not_gray > 0) {
// This is really similar to task_set_.ComputeMinEnd() except that we
// deal properly with the "gray" tasks.
int critical_index = -1;
int gray_critical_index = -1;
// Respectively without gray task and with at most one one gray task.
int min_end_of_critical_tasks = std::numeric_limits<int>::min();
int min_end_of_critical_tasks_with_gray = std::numeric_limits<int>::min();
// The index of the gray task in the critical tasks with one gray, if any.
int gray_task_index = -1;
// Set decreasing_max_end_index to the next non-gray task.
while (is_gray_[task_by_decreasing_max_end_[decreasing_max_end_index]]) {
++decreasing_max_end_index;
CHECK_LT(decreasing_max_end_index, num_tasks);
}
const int non_gray_max_end =
MaxEnd(task_by_decreasing_max_end_[decreasing_max_end_index]);
const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
for (int i = 0; i < sorted_tasks.size(); ++i) {
const TaskSet::Entry& e = sorted_tasks[i];
if (is_gray_[e.task]) {
if (e.min_start >= min_end_of_critical_tasks) {
// Is this gray task increasing the min-end by itself?
const int candidate = e.min_start + e.min_duration;
if (candidate >= min_end_of_critical_tasks_with_gray) {
gray_critical_index = gray_task_index = i;
min_end_of_critical_tasks_with_gray = candidate;
}
} else {
// Is the task at the end of the non-gray critical block better?
const int candidate = min_end_of_critical_tasks + e.min_duration;
if (candidate >= min_end_of_critical_tasks_with_gray) {
gray_critical_index = critical_index;
gray_task_index = i;
min_end_of_critical_tasks_with_gray = candidate;
}
}
} else {
DCHECK_LE(MaxEnd(e.task), non_gray_max_end);
// Augment the gray block. We could augment it more if e.min_start >=
// min_end_of_critical_tasks_with_gray, but we don't care much about
// this case because we will only trigger something if
// min_end_of_critical_tasks_with_gray > min_end_of_critical_tasks.
min_end_of_critical_tasks_with_gray += e.min_duration;
// Augment the non-gray block.
if (e.min_start >= min_end_of_critical_tasks) {
critical_index = i;
min_end_of_critical_tasks = e.min_start + e.min_duration;
} else {
min_end_of_critical_tasks += e.min_duration;
}
}
}
// Overload checking.
if (min_end_of_critical_tasks > non_gray_max_end) {
literal_reason_.clear();
integer_reason_.clear();
// We need the reasons for the critical tasks to fall in:
const int window_start = sorted_tasks[critical_index].min_start;
const int window_end = min_end_of_critical_tasks - 1;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
if (is_gray_[ct]) continue;
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
AddMaxEndReason(ct, window_end);
}
std::vector<Literal>* conflict = trail->MutableConflict();
*conflict = literal_reason_;
integer_trail->MergeReasonInto(integer_reason_, conflict);
return false;
}
// Optimization, we can remove all the gray tasks that starts at or after
// min_end_of_critical_tasks. Note that we deal with the case where
// gray_task_index is removed by this code below.
while (is_gray_[sorted_tasks.back().task] &&
sorted_tasks.back().min_start >= min_end_of_critical_tasks) {
task_set_.RemoveEntryWithIndex(sorted_tasks.size() - 1);
CHECK(!sorted_tasks.empty());
}
// Edge-finding.
// If we have a situation like:
// [(critical_task_with_gray_task)
// ]
// ^ max-end without the gray task.
//
// Then the gray task must be after all the critical tasks (all the non-gray
// tasks in sorted_tasks actually), otherwise there will be no way to
// schedule the critical_tasks inside their time window.
if (min_end_of_critical_tasks_with_gray > non_gray_max_end) {
DCHECK_NE(gray_task_index, -1);
// We may have removed it with the optimization above, so simply continue
// in this case.
if (gray_task_index >= sorted_tasks.size()) continue;
const int gray_task = sorted_tasks[gray_task_index].task;
DCHECK(is_gray_[gray_task]);
// Since the gray task is after all the other, we have a new lower bound.
if (min_end_of_critical_tasks > MinStart(gray_task)) {
literal_reason_.clear();
integer_reason_.clear();
const int window_start = sorted_tasks[gray_critical_index].min_start;
const int window_end = min_end_of_critical_tasks_with_gray - 1;
for (int i = gray_critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
if (is_gray_[ct]) continue;
AddPresenceAndDurationReason(ct);
AddMinStartReason(ct, window_start);
AddMaxEndReason(ct, window_end);
}
// Add the reason for the gray_task (we don't need the max-end or
// presence reason).
AddMinDurationReason(gray_task);
AddMinStartReason(gray_task, window_start);
// Enqueue the new min-start for gray_task.
//
// TODO(user): propagate the precedence Boolean here too? I think it
// will be more powerful. Even if eventually all these precedence will
// become detectable (see Petr Villim PhD).
integer_trail->Enqueue(
IntegerLiteral::FromLbVar(start_vars_[gray_task],
min_end_of_critical_tasks),
literal_reason_, integer_reason_);
if (!CheckIntervalForConflict(gray_task, trail)) return false;
}
// Remove the gray_task from sorted_tasks_.
task_set_.RemoveEntryWithIndex(gray_task_index);
} else {
// Change more task into gray ones.
if (num_not_gray == 1) break;
// Optimization: the non_gray_max_end must move below this threshold
// before we need to recompute anything.
const int threshold = std::max(min_end_of_critical_tasks,
min_end_of_critical_tasks_with_gray);
do {
DCHECK(
!is_gray_[task_by_decreasing_max_end_[decreasing_max_end_index]]);
is_gray_[task_by_decreasing_max_end_[decreasing_max_end_index]] = true;
--num_not_gray;
if (num_not_gray == 0) break;
// Set decreasing_max_end_index to the next non-gray task.
while (
is_gray_[task_by_decreasing_max_end_[decreasing_max_end_index]]) {
++decreasing_max_end_index;
CHECK_LT(decreasing_max_end_index, num_tasks);
}
} while (MaxEnd(task_by_decreasing_max_end_[decreasing_max_end_index]) >=
threshold);
}
}
return true;
}
} // namespace sat
} // namespace operations_research

234
src/sat/disjunctive.h Normal file
View File

@@ -0,0 +1,234 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_DISJUNCTIVE_H_
#define OR_TOOLS_SAT_DISJUNCTIVE_H_
#include "sat/integer.h"
#include "sat/intervals.h"
#include "sat/model.h"
#include "sat/precedences.h"
#include "sat/sat_base.h"
#include "util/stats.h"
namespace operations_research {
namespace sat {
// Enforces a disjunctive (or no overlap) constraints on the given interval
// variables and create a Boolean variables for all the possible precedences of
// the form (task i is before task j).
std::function<void(Model*)> DisjunctiveWithBooleanPrecedences(
const std::vector<IntervalVariable>& vars);
// Helper class to compute the min-end of a set of tasks given their min-start
// and min-duration. In Petr Vilim PhD "Global Constraints in Scheduling", this
// corresponds to his Theta-tree except that we use a O(n) implementation for
// most of the function here, not a O(log(n)) one.
class TaskSet {
public:
TaskSet() : optimized_restart_(0) {}
struct Entry {
int task;
int min_start;
int min_duration;
// Note that the tie-breaking is not important here.
bool operator<(Entry other) const { return min_start < other.min_start; }
};
// Insertion and modification. These leave sorted_tasks_ sorted.
void Clear() {
sorted_tasks_.clear();
optimized_restart_ = 0;
}
void AddEntry(const Entry& e);
void NotifyEntryIsNowLastIfPresent(const Entry& e);
void RemoveEntryWithIndex(int index);
// Like AddEntry() when we already know that e.min_start will be the largest
// one. This is checked in debug mode.
void AddOrderedLastEntry(const Entry& e);
// Advanced usage. Instead of calling many AddEntry(), it is more efficient to
// call AddUnsortedEntry() instead, but then Sort() MUST be called just after
// the insertions. Nothing is checked here, so it is up to the client to do
// that properly.
void AddUnsortedEntry(const Entry& e) { sorted_tasks_.push_back(e); }
void Sort() { std::sort(sorted_tasks_.begin(), sorted_tasks_.end()); }
// Returns the min-end for the task in the set. The time profile of the tasks
// packed to the left will always be a set of contiguous tasks separated by
// empty space:
//
// [Bunch of tasks] ... [Bunch of tasks] ... [critical tasks].
//
// We call "critical tasks" the last group. These tasks will be the sole
// responsible for the min-end of the whole set. The returned critical_index
// will be the index of the first critical task in SortedTasks().
//
// A reason for the min end is:
// - The min-duration of all the critical tasks.
// - The fact that all critical tasks have a min-start greater or equal to the
// first of them, that is SortedTasks()[critical_index].min_start.
//
// It is possible to behave like if one task was not in the set by setting
// task_to_ignore to the id of this task. This returns 0 if the set is empty
// in which case critical_index will be left unchanged.
int ComputeMinEnd(int task_to_ignore, int* critical_index) const;
const std::vector<Entry>& SortedTasks() const { return sorted_tasks_; }
private:
std::vector<Entry> sorted_tasks_;
mutable int optimized_restart_;
DISALLOW_COPY_AND_ASSIGN(TaskSet);
};
// This class contains the propagation algorithms with explanation for a
// disjunctive constraint.
class DisjunctiveConstraint : public PropagatorInterface {
public:
// Creates a disjunctive constraint (or no overlap constraint) between the
// given IntervalVariable.
DisjunctiveConstraint(
const std::vector<IntervalVariable>& non_overlapping_intervals,
IntegerTrail* integer_trail, IntervalsRepository* task_repository,
PrecedencesPropagator* precedences);
~DisjunctiveConstraint() final {
IF_STATS_ENABLED(LOG(INFO) << stats_.StatString());
}
// The algorithm is quadratic in the number of tasks.
bool Propagate(Trail* trail) final;
// Registers this constraint with the GenericLiteralWatcher.
void RegisterWith(GenericLiteralWatcher* watcher);
void SetParameters(const SatParameters& parameters) {
parameters_ = parameters;
}
private:
// Reverses the time and all the relevant quantities. This is needed because
// most passes will propagate different stuff in the reverse time. For
// example, the not-last propagation will become the not-first one in the
// reverse time direction.
void SwitchToMirrorProblem();
// Helpers for the current bounds on a task time window.
// [(min-duration) ... (min-duration)]
// ^ ^ ^ ^
// min-start min-end max-start max-end
int MinDuration(int t) const {
return duration_vars_[t] == kNoLbVar
? fixed_durations_[t]
: integer_trail_->Value(duration_vars_[t]);
}
int MinStart(int t) const { return integer_trail_->Value(start_vars_[t]); }
int MaxEnd(int t) const { return -integer_trail_->Value(minus_end_vars_[t]); }
int MaxStart(int t) const { return MaxEnd(t) - MinDuration(t); }
int MinEnd(int t) const { return MinStart(t) + MinDuration(t); }
// Helper functions to compute the reason of a propagation.
// Append to literal_reason_ and integer_reason_ the corresponding reason.
void AddPresenceAndDurationReason(int t);
void AddMinDurationReason(int t);
void AddMinStartReason(int t, int lower_bound);
void AddMaxEndReason(int t, int upper_bound);
// Checks that the interval [min_start_t, max_end_t] is larger than
// min_duration_t. Returns false and report an conflict otherwise.
bool CheckIntervalForConflict(int t, Trail* trail);
// All these passes use the algorithms described in Petr Vilim PhD "Global
// Constraints in Scheduling". Except that we don't use the O(log(n)) balanced
// tree to compute the min end of a set of task but O(n) algorithm.
//
// This allows to integrate right away any changes we make to the bounds and
// to have a simpler code. Since we also need to produces the reason of each
// propagation, it is unclear if tree-based structure will be a lot better
// here (especially because on the kind of problem we can solve n is
// relatively small, like 30).
bool OverloadCheckingPass(IntegerTrail* integer_trail, Trail* trail);
bool DetectablePrecedencePass(IntegerTrail* integer_trail, Trail* trail);
bool NotLastPass(IntegerTrail* integer_trail, Trail* trail);
bool EdgeFindingPass(IntegerTrail* integer_trail, Trail* trail);
// Exploits the precedences relations of the form "this set of disjoint
// IntervalVariables must be performed before a given IntegerVariable". The
// relations are computed with PrecedencesPropagator::ComputePrecedences().
bool PrecedencePass(IntegerTrail* integer_trail, Trail* trail);
// Sorts the corresponding vectors of tasks. See below.
void UpdateTaskByIncreasingMinStart();
void UpdateTaskByIncreasingMinEnd();
void UpdateTaskByDecreasingMaxStart();
void UpdateTaskByDecreasingMaxEnd();
// The LbVar of each tasks that must be considered for this constraint (note
// that the index is not an IntevalVariable but a new one local to this
// constraint). For optional tasks, we don't list the one that are already
// known to be absent.
std::vector<LbVar> start_vars_;
std::vector<LbVar> end_vars_;
std::vector<LbVar> minus_start_vars_;
std::vector<LbVar> minus_end_vars_;
std::vector<LbVar> duration_vars_;
std::vector<int> fixed_durations_;
std::vector<LiteralIndex> reason_for_presence_;
// This is used by PrecedencePass().
std::vector<LiteralIndex> reason_for_beeing_before_;
std::vector<PrecedencesPropagator::LbVarPrecedences> before_;
std::vector<PrecedencesPropagator::LbVarPrecedences> after_;
// True for the optional tasks that are known to be present and false for the
// one we don't know yet. The one that are known to be absent are not listed.
// The index is the same as for the *_vars vector.
std::vector<bool> task_is_currently_present_;
// Various task orders. The indices are index in the *_vars vectors. We keep
// them separate so that in most cases they are almost sorted and std::sort()
// should be faster. The increasing/decreasing order is choosen so that
// SwitchToMirrorProblem() works in O(1) and permute these vectors
// accordingly.
//
// TODO(user): Using sets or maintaining these vectors sorted at all time
// may be faster.
std::vector<int> task_by_increasing_min_start_;
std::vector<int> task_by_increasing_min_end_;
std::vector<int> task_by_decreasing_max_start_;
std::vector<int> task_by_decreasing_max_end_;
// Reason vectors. Declared here to avoid costly initialization.
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
const std::vector<IntervalVariable> non_overlapping_intervals_;
IntegerTrail* integer_trail_;
IntervalsRepository* intervals_;
PrecedencesPropagator* precedences_;
TaskSet task_set_;
std::vector<bool> is_gray_;
SatParameters parameters_;
mutable StatsGroup stats_;
DISALLOW_COPY_AND_ASSIGN(DisjunctiveConstraint);
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_DISJUNCTIVE_H_

75
src/sat/integer_sum.cc Normal file
View File

@@ -0,0 +1,75 @@
// Copyright 2010-2014 Google
// 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.
#include "sat/integer_sum.h"
namespace operations_research {
namespace sat {
IntegerSum::IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coeffs, IntegerVariable sum,
IntegerTrail* integer_trail)
: vars_(vars), coeffs_(coeffs), sum_(sum), integer_trail_(integer_trail) {}
bool IntegerSum::Propagate(Trail* trail) {
if (vars_.empty()) return true;
int new_lb = integer_trail_->LowerBound(vars_[0]) * coeffs_[0];
for (int i = 1; i < vars_.size(); ++i) {
new_lb += integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
}
// Update the sum lower-bound.
if (new_lb > integer_trail_->LowerBound(sum_)) {
integer_reason_.clear();
for (const IntegerVariable& var : vars_) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
}
integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(sum_, new_lb),
literal_reason_, integer_reason_);
if (integer_trail_->DomainIsEmpty(sum_, trail)) return false;
}
// Update the variables upper-bound.
const int sum_upper_bound = integer_trail_->UpperBound(sum_);
for (int i = 0; i < vars_.size(); ++i) {
const int new_term_ub = sum_upper_bound - new_lb +
integer_trail_->LowerBound(vars_[i]) * coeffs_[i];
const int new_ub = new_term_ub / coeffs_[i];
if (new_ub < integer_trail_->UpperBound(vars_[i])) {
integer_reason_.clear();
for (int j = 0; j < vars_.size(); ++j) {
if (i == j) continue;
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(vars_[j]));
}
integer_reason_.push_back(integer_trail_->UpperBoundAsLiteral(sum_));
integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(vars_[i], new_ub),
literal_reason_, integer_reason_);
if (integer_trail_->DomainIsEmpty(vars_[i], trail)) return false;
}
}
return true;
}
void IntegerSum::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntegerVariable& var : vars_) {
watcher->WatchIntegerVariable(var, id);
}
watcher->WatchIntegerVariable(sum_, id);
}
} // namespace sat
} // namespace operations_research

79
src/sat/integer_sum.h Normal file
View File

@@ -0,0 +1,79 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_INTEGER_SUM_H_
#define OR_TOOLS_SAT_INTEGER_SUM_H_
#include "sat/integer.h"
#include "sat/model.h"
#include "sat/sat_base.h"
namespace operations_research {
namespace sat {
// A really basic implementation of a sum of integer variables.
// The complexity is in O(num_variables) at each propagation.
//
// TODO(user): handle negative coefficients.
// TODO(user): Propagate all the bounds.
// TODO(user): If one has many such constraint, it will be more efficient to
// propagate all of them at once rather than doing it one at the time.
class IntegerSum : public PropagatorInterface {
public:
IntegerSum(const std::vector<IntegerVariable>& vars,
const std::vector<int>& coefficients, IntegerVariable sum,
IntegerTrail* integer_trail);
// Currently we only propagates the directions:
// * vars lower-bound -> sum lower-bound.
// * for all vars i,
// vars lower-bound (excluding i) + sum upper_bound -> i upper-bound.
bool Propagate(Trail* trail) final;
void RegisterWith(GenericLiteralWatcher* watcher);
private:
std::vector<IntegerVariable> vars_;
std::vector<int> coeffs_;
IntegerVariable sum_;
IntegerTrail* integer_trail_;
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
DISALLOW_COPY_AND_ASSIGN(IntegerSum);
};
// Model-based function to create an IntegerVariable that corresponds to the
// given weighted sum of other IntegerVariables.
inline std::function<IntegerVariable(Model*)> NewWeightedSum(
const std::vector<int>& coefficients, const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// The trival bounds will be propagated correctly at level zero.
// TODO(user): pay attention to integer overflow. It currently work but
// it is not really robust.
IntegerVariable sum = integer_trail->AddIntegerVariable(
std::numeric_limits<int>::min(), std::numeric_limits<int>::max());
IntegerSum* constraint =
new IntegerSum(vars, coefficients, sum, integer_trail);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
return sum;
};
}
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_INTEGER_SUM_H_

68
src/sat/intervals.cc Normal file
View File

@@ -0,0 +1,68 @@
// Copyright 2010-2014 Google
// 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.
#include "sat/intervals.h"
namespace operations_research {
namespace sat {
IntervalVariable IntervalsRepository::CreateNewInterval() {
const IntervalVariable task_id(start_vars_.size());
// TODO(user): clean-up the upper bound and make sure we don't have any
// overflow when creating task. We cannot use std::numeric_limits<int>::max()
// because we may add a size to this bound, and we don't want any overflow
// when we do that.
const int ub = std::numeric_limits<int>::max() / 2;
start_vars_.push_back(integer_trail_->AddIntegerVariable(0, ub));
end_vars_.push_back(integer_trail_->AddIntegerVariable(0, ub));
size_vars_.push_back(kNoIntegerVariable);
fixed_sizes_.push_back(0);
is_present_.push_back(kNoLiteralIndex);
return task_id;
}
IntervalVariable IntervalsRepository::CreateInterval(int min_size,
int max_size) {
CHECK_LE(min_size, max_size);
if (min_size == max_size) {
return CreateIntervalWithFixedSize(min_size);
}
const IntervalVariable t = CreateNewInterval();
size_vars_.back() = integer_trail_->AddIntegerVariable(min_size, max_size);
precedences_->AddPrecedenceWithVariableOffset(StartVar(t), EndVar(t),
LbVarOf(SizeVar(t)));
precedences_->AddPrecedenceWithVariableOffset(EndVar(t), StartVar(t),
MinusUbVarOf(SizeVar(t)));
return t;
}
IntervalVariable IntervalsRepository::CreateIntervalWithFixedSize(int size) {
const IntervalVariable t = CreateNewInterval();
fixed_sizes_.back() = size;
precedences_->AddPrecedenceWithOffset(StartVar(t), EndVar(t), size);
precedences_->AddPrecedenceWithOffset(EndVar(t), StartVar(t), -size);
return t;
}
IntervalVariable IntervalsRepository::CreateOptionalIntervalWithFixedSize(
int size, Literal is_present) {
const IntervalVariable t = CreateIntervalWithFixedSize(size);
is_present_.back() = is_present.Index();
precedences_->MarkIntegerVariableAsOptional(StartVar(t), is_present);
precedences_->MarkIntegerVariableAsOptional(EndVar(t), is_present);
return t;
}
} // namespace sat
} // namespace operations_research

227
src/sat/intervals.h Normal file
View File

@@ -0,0 +1,227 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_INTERVALS_H_
#define OR_TOOLS_SAT_INTERVALS_H_
#include "sat/integer.h"
#include "sat/model.h"
#include "sat/precedences.h"
#include "sat/sat_base.h"
#include "sat/sat_solver.h"
namespace operations_research {
namespace sat {
DEFINE_INT_TYPE(IntervalVariable, int32);
const IntervalVariable kNoIntervalVariable(-1);
// This class maintains a set of intervals which correspond to three integer
// variables (start, end and size). It automatically registers with the
// PrecedencesPropagator the relation between the bounds of each interval and
// provides many helper functions to add precedences relation between intervals.
class IntervalsRepository {
public:
IntervalsRepository(IntegerTrail* integer_trail,
PrecedencesPropagator* precedences)
: integer_trail_(integer_trail), precedences_(precedences) {}
static IntervalsRepository* CreateInModel(Model* model) {
IntervalsRepository* intervals =
new IntervalsRepository(model->GetOrCreate<IntegerTrail>(),
model->GetOrCreate<PrecedencesPropagator>());
model->TakeOwnership(intervals);
return intervals;
}
// Returns the current number of intervals in the repository.
// The interval will always be identified by an integer in [0, num_intervals).
int NumIntervals() const { return start_vars_.size(); }
// Functions to add a new interval to the repository.
IntervalVariable CreateInterval(int min_size, int max_size);
IntervalVariable CreateIntervalWithFixedSize(int size);
IntervalVariable CreateOptionalIntervalWithFixedSize(int size,
Literal is_present);
// Returns whether or not a interval is optional and the associated literal.
bool IsOptional(IntervalVariable i) const {
return is_present_[i] != kNoLiteralIndex;
}
Literal IsPresentLiteral(IntervalVariable i) const {
return Literal(is_present_[i]);
}
// The 3 integer variables associated to a interval.
// Fixed size intervals will have a kNoIntegerVariable as size.
//
// Note: For an optional interval, the start/end variables are propagated
// asssuming the interval is present. Because of that, these variables can
// cross each other or have an empty domain. If any of this happend, then the
// IsPresentLiteral() of this interval will be propagated to false.
IntegerVariable SizeVar(IntervalVariable i) const { return size_vars_[i]; }
IntegerVariable StartVar(IntervalVariable i) const { return start_vars_[i]; }
IntegerVariable EndVar(IntervalVariable i) const { return end_vars_[i]; }
// Only meaningfull if SizeVar(i) == kNoIntegerVariable.
int FixedSize(IntervalVariable i) const { return fixed_sizes_[i]; }
private:
// Creates a new interval and returns its id.
IntervalVariable CreateNewInterval();
// External classes needed.
IntegerTrail* integer_trail_;
PrecedencesPropagator* precedences_;
// Literal indicating if the tasks is executed. Tasks that are always executed
// will have a kNoLiteralIndex entry in this vector.
ITIVector<IntervalVariable, LiteralIndex> is_present_;
// The integer variables for each tasks.
ITIVector<IntervalVariable, IntegerVariable> start_vars_;
ITIVector<IntervalVariable, IntegerVariable> end_vars_;
ITIVector<IntervalVariable, IntegerVariable> size_vars_;
ITIVector<IntervalVariable, int> fixed_sizes_;
DISALLOW_COPY_AND_ASSIGN(IntervalsRepository);
};
// =============================================================================
// Model based functions.
// =============================================================================
inline std::function<IntegerVariable(const Model&)> StartVar(
IntervalVariable v) {
return [=](const Model& model) {
return model.Get<IntervalsRepository>()->StartVar(v);
};
}
inline std::function<IntegerVariable(const Model&)> EndVar(IntervalVariable v) {
return [=](const Model& model) {
return model.Get<IntervalsRepository>()->EndVar(v);
};
}
inline std::function<IntegerVariable(const Model&)> SizeVar(
IntervalVariable v) {
return [=](const Model& model) {
return model.Get<IntervalsRepository>()->SizeVar(v);
};
}
inline std::function<IntervalVariable(Model*)> NewInterval(int size) {
return [=](Model* model) {
return model->GetOrCreate<IntervalsRepository>()
->CreateIntervalWithFixedSize(size);
};
}
inline std::function<IntervalVariable(Model*)> NewIntervalWithVariableSize(
int min_size, int max_size) {
return [=](Model* model) {
return model->GetOrCreate<IntervalsRepository>()->CreateInterval(min_size,
max_size);
};
}
inline std::function<IntervalVariable(Model*)> NewOptionalInterval(
int size, Literal is_present) {
return [=](Model* model) {
return model->GetOrCreate<IntervalsRepository>()
->CreateOptionalIntervalWithFixedSize(size, is_present);
};
}
inline std::function<void(Model*)> EndBefore(IntervalVariable i1,
IntegerVariable ivar) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
precedences->AddPrecedence(intervals->EndVar(i1), ivar);
};
}
inline std::function<void(Model*)> EndBeforeWithOffset(IntervalVariable i1,
IntegerVariable ivar,
int offset) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
precedences->AddPrecedenceWithOffset(intervals->EndVar(i1), ivar, offset);
};
}
inline std::function<void(Model*)> EndBeforeStart(IntervalVariable i1,
IntervalVariable i2) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
precedences->AddPrecedence(intervals->EndVar(i1), intervals->StartVar(i2));
};
}
inline std::function<void(Model*)> StartAtStart(IntervalVariable i1,
IntervalVariable i2) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
precedences->AddPrecedence(intervals->StartVar(i1),
intervals->StartVar(i2));
precedences->AddPrecedence(intervals->StartVar(i2),
intervals->StartVar(i1));
};
}
inline std::function<void(Model*)> EndAtEnd(IntervalVariable i1,
IntervalVariable i2) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
PrecedencesPropagator* precedences =
model->GetOrCreate<PrecedencesPropagator>();
precedences->AddPrecedence(intervals->EndVar(i1), intervals->EndVar(i2));
precedences->AddPrecedence(intervals->EndVar(i2), intervals->EndVar(i1));
};
}
// TODO(user): Add a propagator on the interval duration depending
// on the set of alternatives that are currently not executable.
//
// This requires that all the alternatives are optional tasks.
inline std::function<void(Model*)> IntervalWithAlternatives(
IntervalVariable master, const std::vector<IntervalVariable>& members) {
return [=](Model* model) {
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
// Create an "exactly one executed" constraint on the alternatives.
std::vector<LiteralWithCoeff> sat_ct;
for (const IntervalVariable member : members) {
CHECK(intervals->IsOptional(member));
const Literal is_present = intervals->IsPresentLiteral(member);
sat_ct.push_back({is_present, Coefficient(1)});
model->Add(StartAtStart(master, member));
model->Add(EndAtEnd(member, master));
}
model->Add(BooleanLinearConstraint(1, 1, &sat_ct));
};
}
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_INTERVALS_H_

326
src/sat/no_cycle.cc Normal file
View File

@@ -0,0 +1,326 @@
// Copyright 2010-2014 Google
// 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.
#include "sat/no_cycle.h"
#include <numeric>
#include "base/stl_util.h"
namespace operations_research {
namespace sat {
bool NoCyclePropagator::Propagate(Trail* trail) {
if (problem_is_unsat_) {
trail->MutableConflict()->clear();
return false;
}
if (!initialization_is_done_) {
CHECK_EQ(0, trail->CurrentDecisionLevel());
initialization_is_done_ = true;
// Propagate all that can be propagated using the fixed arcs.
for (int node = 0; node < graph_.size(); ++node) {
FillNodeIsReachedWithAntecedentOf(node);
for (const Arc arc : potential_graph_[node]) {
if (!node_is_reached_[arc.head]) continue;
// We know that l must be false.
const Literal l(arc.literal_index);
if (trail->Assignment().VariableIsAssigned(l.Variable())) {
if (trail->Assignment().LiteralIsTrue(l)) {
// The problem is UNSAT.
trail->MutableConflict()->clear();
return false;
}
} else {
trail->EnqueueWithUnitReason(l.Negated());
}
}
}
}
while (propagation_trail_index_ < trail->Index()) {
const Literal literal = (*trail)[propagation_trail_index_++];
if (literal.Index() >= potential_arcs_.size()) continue;
for (const std::pair<int, int>& p : potential_arcs_[literal.Index()]) {
{
// Remove this arc from the potential_graph_.
//
// TODO(user): this is not super efficient, but it helps speeding up
// the propagation here and in the makespan constraint.
int new_size = 0;
std::vector<Arc>& ref = potential_graph_[p.first];
const int size = ref.size();
while (new_size < size &&
ref[new_size].literal_index != literal.Index()) {
++new_size;
}
for (int i = new_size; i < size; ++i) {
if (ref[i].literal_index != literal.Index()) {
ref[new_size++] = ref[i];
}
}
ref.resize(new_size);
}
if (!include_propagated_arcs_in_graph_ &&
trail->AssignmentType(literal.Variable()) == propagator_id_) {
continue;
}
// Warning: The order of the following 3 lines matter!
if (IsReachable(p.first, p.second)) continue;
newly_reachable_ = NewlyReachable(p.second, &node_is_reached_);
FillNodeIsReachedWithAntecedentOf(p.first);
// Do nothing if we reached the threshold on the number of arcs.
if (num_arcs_ == num_arcs_threshold_) continue;
if (node_is_reached_[p.second]) { // Conflict.
// Note that this modifies node_is_reached_ and reached_nodes_, but
// since we abort aftewards, it is fine.
FindReasonForPath(*trail, p.second, p.first, propagation_trail_index_,
trail->MutableConflict());
trail->MutableConflict()->push_back(literal.Negated());
return false;
}
++num_arcs_;
graph_[p.first].push_back({p.second, literal.Index()});
reverse_graph_[p.second].push_back({p.first, literal.Index()});
for (const int node : newly_reachable_) {
for (const Arc arc : potential_graph_[node]) {
CHECK_NE(arc.literal_index, kNoLiteralIndex);
if (node_is_reached_[arc.head]) {
const Literal l(arc.literal_index);
if (trail->Assignment().VariableIsAssigned(l.Variable())) {
// TODO(user): we could detect a conflict earlier if the literal
// l is already assigned to true.
continue;
}
// Save the information needed for the lazy-explanation and enqueue
// the fact that "arc" cannot be in the graph.
const int trail_index = trail->Index();
if (trail_index >= reason_arc_.size()) {
reason_arc_.resize(trail_index + 1);
reason_trail_limit_.resize(trail_index + 1);
}
reason_arc_[trail_index] = {node, arc.head};
reason_trail_limit_[trail_index] = propagation_trail_index_;
trail->Enqueue(l.Negated(), propagator_id_);
}
}
}
}
}
return true;
}
void NoCyclePropagator::Untrail(const Trail& trail, int trail_index) {
while (propagation_trail_index_ > trail_index) {
const Literal literal = trail[--propagation_trail_index_];
if (literal.Index() >= potential_arcs_.size()) continue;
for (const std::pair<int, int>& p : potential_arcs_[literal.Index()]) {
DCHECK_LT(p.first, graph_.size());
DCHECK_GE(p.first, 0);
potential_graph_[p.first].push_back({p.second, literal.Index()});
// We only remove this arc if it was added. That is if it is the last arc
// in graph_[p.first].
if (graph_[p.first].empty()) continue;
if (graph_[p.first].back().literal_index != literal.Index()) continue;
--num_arcs_;
graph_[p.first].pop_back();
reverse_graph_[p.second].pop_back();
}
}
}
// TODO(user): If one literal propagate many arcs, and more than one is needed
// to form a cycle, this will not work properly.
ClauseRef NoCyclePropagator::Reason(const Trail& trail, int trail_index) const {
const int source = reason_arc_[trail_index].second;
const int target = reason_arc_[trail_index].first;
const int trail_limit = reason_trail_limit_[trail_index];
std::vector<Literal>* const reason = trail.GetVectorToStoreReason(trail_index);
// Note that this modify node_is_reached_ and reached_nodes_.
FindReasonForPath(trail, source, target, trail_limit, reason);
return ClauseRef(*reason);
}
namespace {
// This sets the given vector of Booleans to all false using a vector of its
// positions at true in order to exploit sparsity.
//
// TODO(user): Add a test depending on position.size() or use directly
// util::operations_research::SparseBitset.
void ResetBitsetWithPosition(int new_size, std::vector<bool>* bitset,
std::vector<int>* true_positions) {
bitset->resize(new_size, false);
for (const int i : *true_positions) {
DCHECK((*bitset)[i]);
(*bitset)[i] = false;
}
true_positions->clear();
DCHECK(
std::none_of(bitset->begin(), bitset->end(), [](bool v) { return v; }));
}
} // namespace
// We use a BFS to try to minimize the reason.
void NoCyclePropagator::FindReasonForPath(const Trail& trail, int source,
int target, int trail_limit,
std::vector<Literal>* reason) const {
CHECK_NE(source, target);
ResetBitsetWithPosition(graph_.size(), &node_is_reached_, &reached_nodes_);
// This is the same code as IsReachable() below, except that we need to
// remember the path taken to the target and we work on a subgraph.
reached_nodes_.push_back(source);
parent_index_with_literal_.clear();
parent_index_with_literal_.push_back({0, LiteralIndex(-1)});
node_is_reached_[source] = true;
int i = 0;
for (; i < reached_nodes_.size(); ++i) {
const int node = reached_nodes_[i];
if (node == target) break;
// Only consider arc whose literal was assigned before trail_limit. The arcs
// in graph_[node] are ordered by increasing trail index, so it is okay to
// abort as soon as an arc was added after trail_limit.
for (const Arc& arc : graph_[node]) {
if (arc.literal_index != kNoLiteralIndex) {
const BooleanVariable var = Literal(arc.literal_index).Variable();
if (trail.Info(var).trail_index >= trail_limit) break;
}
if (node_is_reached_[arc.head]) continue;
node_is_reached_[arc.head] = true;
reached_nodes_.push_back(arc.head);
parent_index_with_literal_.push_back({i, arc.literal_index});
}
}
// Follow the path backward and fill the reason.
CHECK_LT(i, reached_nodes_.size()) << "The target is not reachable!";
reason->clear();
while (i != 0) {
const LiteralIndex literal_index = parent_index_with_literal_[i].second;
if (literal_index != kNoLiteralIndex) {
reason->push_back(Literal(literal_index).Negated());
}
i = parent_index_with_literal_[i].first;
}
}
bool NoCyclePropagator::IsReachable(int source, int destination) const {
if (source == destination) return true;
ResetBitsetWithPosition(graph_.size(), &node_is_reached_, &reached_nodes_);
reached_nodes_.push_back(source);
node_is_reached_[source] = true;
for (int i = 0; i < reached_nodes_.size(); ++i) {
for (const Arc& arc : graph_[reached_nodes_[i]]) {
if (arc.head == destination) return true;
if (node_is_reached_[arc.head]) continue;
node_is_reached_[arc.head] = true;
reached_nodes_.push_back(arc.head);
}
}
return false;
}
void NoCyclePropagator::FillNodeIsReachedWithAntecedentOf(int source) const {
ResetBitsetWithPosition(graph_.size(), &node_is_reached_, &reached_nodes_);
reached_nodes_.push_back(source);
node_is_reached_[source] = true;
for (int i = 0; i < reached_nodes_.size(); ++i) {
for (const Arc& arc : reverse_graph_[reached_nodes_[i]]) {
if (node_is_reached_[arc.head]) continue;
node_is_reached_[arc.head] = true;
reached_nodes_.push_back(arc.head);
}
}
}
std::vector<int> NoCyclePropagator::NewlyReachable(
int source, std::vector<bool>* already_reached) const {
if ((*already_reached)[source]) return std::vector<int>();
std::vector<int> result;
result.push_back(source);
(*already_reached)[source] = true;
for (int i = 0; i < result.size(); ++i) {
for (const Arc& arc : graph_[result[i]]) {
if ((*already_reached)[arc.head]) continue;
(*already_reached)[arc.head] = true;
result.push_back(arc.head);
}
}
// Restore already_reached to its original value.
for (const int node : result) (*already_reached)[node] = false;
return result;
}
void NoCyclePropagator::AdjustSizes(int tail, int head, int literal_index) {
CHECK_NE(tail, head);
CHECK(!initialization_is_done_);
CHECK_EQ(0, propagation_trail_index_);
const int m = std::max(tail, head);
DCHECK_GE(m, 0);
if (m >= graph_.size()) {
graph_.resize(m + 1);
potential_graph_.resize(m + 1);
reverse_graph_.resize(m + 1);
}
DCHECK_GE(literal_index, 0);
if (literal_index >= potential_arcs_.size()) {
potential_arcs_.resize(literal_index + 1);
}
}
void NoCyclePropagator::AddArc(int tail, int head) {
AdjustSizes(tail, head, 0);
// Deal with the corner case of a cycle with the fixed arcs.
if (problem_is_unsat_ || IsReachable(head, tail)) {
problem_is_unsat_ = true;
return;
}
// TODO(user): test IsReachable(tail, head) and do not add the arc if true?
++num_arcs_;
graph_[tail].push_back({head, LiteralIndex(-1)});
reverse_graph_[head].push_back({tail, LiteralIndex(-1)});
}
void NoCyclePropagator::AddPotentialArc(int tail, int head, Literal literal) {
AdjustSizes(tail, head, literal.Index().value());
potential_arcs_[literal.Index()].push_back({tail, head});
potential_graph_[tail].push_back({head, literal.Index()});
CHECK_EQ(1, potential_arcs_[literal.Index()].size())
<< "We don't support multiple arcs associated to the same literal. "
<< "However, it should be fairly easy to support this case.";
}
} // namespace sat
} // namespace operations_research

179
src/sat/no_cycle.h Normal file
View File

@@ -0,0 +1,179 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_NO_CYCLE_H_
#define OR_TOOLS_SAT_NO_CYCLE_H_
#include <vector>
#include "sat/model.h"
#include "sat/sat_base.h"
#include "sat/sat_solver.h"
namespace operations_research {
namespace sat {
// The "no-cycle" constraint.
//
// Each arc will be associated to a literal and this propagator will make sure
// that there is no cycle in the graph with only the arcs whose associated
// literal is set to true.
class NoCyclePropagator : public Propagator {
public:
NoCyclePropagator()
: Propagator("NoCyclePropagator"),
num_arcs_(0),
problem_is_unsat_(false),
initialization_is_done_(false),
num_arcs_threshold_(std::numeric_limits<int64>::max()),
include_propagated_arcs_in_graph_(true) {}
~NoCyclePropagator() final {}
static NoCyclePropagator* CreateInModel(Model* model) {
NoCyclePropagator* no_cycle = new NoCyclePropagator();
model->GetOrCreate<SatSolver>()->AddPropagator(
std::unique_ptr<NoCyclePropagator>(no_cycle));
return no_cycle;
}
bool Propagate(Trail* trail) final;
void Untrail(const Trail& trail, int trail_index) final;
ClauseRef Reason(const Trail& trail, int trail_index) const final;
// Stops doing anything when the number of arcs in the graph becomes greater
// that the given value. This allows to use this class to model a circuit
// constraint on n nodes: we don't want any cycle, but it is okay to have one
// when we add the n-th arc. Of course we also need to make sure that each
// node as an unique successor using at-most-one constraints.
void AllowCycleWhenNumArcsIsGreaterThan(int64 value) {
num_arcs_threshold_ = value;
}
// If this is false, then we don't track inside our graphs the arcs that we
// propagated. This is meant to be turned on if an arc and its reverse are
// controlled by a literal and its negation. When this is the case, then we
// know that all the arcs propagated by this class don't change the
// reachability of the graph.
void IncludePropagatedArcsInGraph(bool value) {
include_propagated_arcs_in_graph_ = value;
}
// Adds a "constant" arc to the graph.
// Self-arc are not allowed (it would create a trivial cycle).
void AddArc(int tail, int head);
// Registers an arc that will be present in the graph iff 'literal' is true.
// Self-arc are not allowed (it would fix the given literal to false).
//
// TODO(user): support more than one arc associated to the same literal.
void AddPotentialArc(int tail, int head, Literal literal);
// Getters for the current graph. This is only in sync with the trail iff
// Propagator::PropagationIsDone() is true.
//
// Note that these graphs will NOT contain all the arcs but will correctly
// encode the reachability of every node. More specifically, when an arc (tail
// -> head) is about to be added but a path from tail to head already exists
// in the graph, this arc will not be added.
struct Arc {
int head;
LiteralIndex literal_index;
};
const std::vector<std::vector<Arc>>& Graph() const { return graph_; }
const std::vector<std::vector<Arc>>& ReverseGraph() const { return reverse_graph_; }
// Getters for the "potential" arcs. That is the arcs that could be added to
// the graph or not depending on their associated literal value. Note that
// some already added arcs may not appear here for optimization purposes.
const std::vector<std::vector<Arc>>& PotentialGraph() const { return potential_graph_; }
const ITIVector<LiteralIndex, std::vector<std::pair<int, int>>>& PotentialArcs()
const {
return potential_arcs_;
}
private:
// Adjust the internal data structures when a new arc is added.
void AdjustSizes(int tail, int head, int literal_index);
// Returns true if destination is reachable from source in graph_.
// Warning: this modifies node_is_reached_ and reached_nodes_.
bool IsReachable(int source, int destination) const;
// Returns the set of node from which source can be reached (included).
// Warning: this modifies node_is_reached_ and reached_nodes_.
void FillNodeIsReachedWithAntecedentOf(int source) const;
// Returns the vector of node that are reachable from source (included), but
// not in the given already_reached. The already_reached vector is not const
// because this function temporarily modifies it before restoring it to its
// original value for performance reason.
std::vector<int> NewlyReachable(int source, std::vector<bool>* already_reached) const;
// Finds a path from source to target and output its reason.
// Only the arcs whose associated literal is assigned before the given
// trail_limit are considered.
//
// Warning: this modifies node_is_reached_ and reached_nodes_.
void FindReasonForPath(const Trail& trail, int source, int target,
int trail_limit, std::vector<Literal>* reason) const;
// The number of arcs in graph_ and reverse_graph_.
int64 num_arcs_;
// Just used to detect the corner case of a cycle with fixed arcs.
bool problem_is_unsat_;
bool initialization_is_done_;
// Control the options of this class.
int64 num_arcs_threshold_;
bool include_propagated_arcs_in_graph_;
// The current graph wich is kept in sync with the literal trail. For each
// node, graph_[node] list the pair (head, literal_index) of the outgoing
// arcs.
//
// Important: this will always be kept acyclic.
std::vector<std::vector<Arc>> graph_;
std::vector<std::vector<Arc>> reverse_graph_;
// The graph formed by all the potential arcs in the same format as graph_.
std::vector<std::vector<Arc>> potential_graph_;
// The set of potential arc (tail, head) indexed by literal_index.
//
// TODO(user): Introduce a struct with .tail and .head to make the code more
// readable.
ITIVector<LiteralIndex, std::vector<std::pair<int, int>>> potential_arcs_;
// Temporary vectors used by the various BFS computations. We always have:
// node_is_reached_[node] is true iff reached_nodes_ contains node.
mutable std::vector<int> reached_nodes_;
mutable std::vector<bool> node_is_reached_;
// Temporary vector to hold the result of NewlyReachable().
std::vector<int> newly_reachable_;
// Temporary vector used by FindReasonForPath().
mutable std::vector<std::pair<int, LiteralIndex>> parent_index_with_literal_;
// The arc that caused the literal at a given trail_index to be propagated.
std::vector<std::pair<int, int>> reason_arc_;
std::vector<int> reason_trail_limit_;
DISALLOW_COPY_AND_ASSIGN(NoCyclePropagator);
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_NO_CYCLE_H_

627
src/sat/precedences.cc Normal file
View File

@@ -0,0 +1,627 @@
// Copyright 2010-2014 Google
// 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.
#include "sat/precedences.h"
#include "base/cleanup.h"
#include "base/stl_util.h"
namespace operations_research {
namespace sat {
namespace {
bool IsInvalidOrTrue(LiteralIndex index, const Trail& trail) {
return index == kNoLiteralIndex ||
trail.Assignment().LiteralIsTrue(Literal(index));
}
void AppendNegationIfValid(LiteralIndex i, std::vector<Literal>* reason) {
if (i != kNoLiteralIndex) reason->push_back(Literal(i).Negated());
}
void AppendValueIfValid(LbVar var, const IntegerTrail& i_trail,
std::vector<IntegerLiteral>* reason) {
if (var != kNoLbVar) reason->push_back(i_trail.ValueAsLiteral(var));
}
} // namespace
bool PrecedencesPropagator::Propagate(Trail* trail) {
while (propagation_trail_index_ < trail->Index()) {
const Literal literal = (*trail)[propagation_trail_index_++];
if (literal.Index() < potential_nodes_.size()) {
// We need to mark these nodes since they are now "present".
for (const int node : potential_nodes_[literal.Index()]) {
const IntegerVariable i(node);
modified_vars_.Set(LbVarOf(i));
modified_vars_.Set(MinusUbVarOf(i));
}
}
if (literal.Index() >= potential_arcs_.size()) continue;
// IMPORTANT: Because of the way Untrail() work, we need to add all the
// potential arcs before we can abort. It is why we iterate twice here.
for (const int arc_index : potential_arcs_[literal.Index()]) {
const ArcInfo& arc = arcs_[arc_index];
impacted_arcs_[arc.tail_var].push_back(arc_index);
if (arc.offset_var != kNoLbVar) {
impacted_arcs_[arc.offset_var].push_back(arc_index);
}
}
// Iterate again to check for a propagation and indirectly update
// modified_vars_.
for (const int arc_index : potential_arcs_[literal.Index()]) {
const ArcInfo& arc = arcs_[arc_index];
if (!IsInvalidOrTrue(OptionalLiteralOf(arc.tail_var), *trail)) {
continue;
}
const int new_head_lb =
integer_trail_->Value(arc.tail_var) + ArcOffset(arc);
if (new_head_lb > integer_trail_->Value(arc.head_var)) {
if (!EnqueueAndCheck(arc, new_head_lb, trail)) return false;
}
PropagateMaxOffsetIfNeeded(arc, trail);
}
}
// Do the actual propagation of the IntegerVariable bounds.
InitializeBFQueueWithModifiedNodes();
if (!BellmanFordTarjan(trail)) return false;
DCHECK(NoPropagationLeft(*trail));
// Propagate the presence literal of the arcs that can't be added.
PropagateOptionalArcs(trail);
// Clean-up modified_vars_ to do as little as possible on the next call.
modified_vars_.ClearAndResize(LbVar(integer_trail_->NumLbVars()));
return true;
}
void PrecedencesPropagator::Untrail(const Trail& trail, int trail_index) {
if (propagation_trail_index_ > trail_index) {
// This means that we already propagated all there is to propagate
// at the level trail_index, so we can safely clear modified_vars_ in case
// it wasn't already done.
modified_vars_.ClearAndResize(LbVar(integer_trail_->NumLbVars()));
}
while (propagation_trail_index_ > trail_index) {
const Literal literal = trail[--propagation_trail_index_];
if (literal.Index() >= potential_arcs_.size()) continue;
for (const int arc_index : potential_arcs_[literal.Index()]) {
const ArcInfo& arc = arcs_[arc_index];
impacted_arcs_[arc.tail_var].pop_back();
if (arc.offset_var != kNoLbVar) {
impacted_arcs_[arc.offset_var].pop_back();
}
}
}
}
// Instead of simply sorting the LbVarPrecedences returned by .var, experiments
// showed that it is faster to regroup all the same .var "by hand" by first
// computing how many times they appear and then apply the sorting permutation.
void PrecedencesPropagator::ComputePrecedences(
const std::vector<LbVar>& to_consider, std::vector<LbVarPrecedences>* output) {
tmp_sorted_lbvars_.clear();
tmp_precedences_.clear();
for (int index = 0; index < to_consider.size(); ++index) {
const LbVar var = to_consider[index];
if (var == kNoLbVar || var >= impacted_arcs_.size()) continue;
for (const int i : impacted_arcs_[var]) {
const ArcInfo& arc = arcs_[i];
if (arc.tail_var != var) continue; // Skip variable duration.
// We don't handle offsets and just care about "is before or at", so we
// skip negative offsets and just treat a positive one as zero. Because of
// this, we may miss some propagation opportunities.
if (arc.offset < 0) continue;
if (lbvar_to_degree_[arc.head_var] == 0) {
tmp_sorted_lbvars_.push_back(
{arc.head_var, integer_trail_->ValueAsLiteral(arc.head_var).bound});
} else {
// This "seen" mechanism is needed because we may have multi-arc and we
// don't want any duplicates in the "is_before" relation. Note that it
// works because lbvar_to_last_index_ is reset by the
// lbvar_to_degree_ == 0 case.
if (lbvar_to_last_index_[arc.head_var] == index) continue;
}
lbvar_to_last_index_[arc.head_var] = index;
lbvar_to_degree_[arc.head_var]++;
tmp_precedences_.push_back({index, arc.head_var, arc.presence_l});
}
}
// This order is a topological order for the precedences relation order
// provided that all the offset between the involved LbVar are positive.
//
// TODO(user): use an order that is always topological? This is not clear
// since it may be slower to compute and not worth it because the order below
// is more natural and may work better.
std::sort(tmp_sorted_lbvars_.begin(), tmp_sorted_lbvars_.end());
// Permute tmp_precedences_ into the output to put it in the correct order.
// For that we transform lbvar_to_degree_ to point to the first position of
// each lbvar in the output vector.
int start = 0;
for (const SortedLbVar pair : tmp_sorted_lbvars_) {
const int degree = lbvar_to_degree_[pair.var];
lbvar_to_degree_[pair.var] = start;
start += degree;
}
output->resize(start);
for (const LbVarPrecedences& precedence : tmp_precedences_) {
(*output)[lbvar_to_degree_[precedence.var]++] = precedence;
}
// Cleanup lbvar_to_degree_, note that we don't need to clean
// lbvar_to_last_index_.
for (const SortedLbVar pair : tmp_sorted_lbvars_) {
lbvar_to_degree_[pair.var] = 0;
}
}
void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
if (i.value() >= optional_literals_.size()) {
optional_literals_.resize(i.value() + 1, kNoLiteralIndex);
}
const int index = std::max(LbVarOf(i).value(), MinusUbVarOf(i).value());
if (index >= impacted_arcs_.size()) {
modified_vars_.Resize(LbVar(index) + 1);
for (LbVar var(impacted_arcs_.size()); var <= index; ++var) {
watcher_->WatchLbVar(var, watcher_id_);
}
impacted_arcs_.resize(index + 1);
impacted_potential_arcs_.resize(index + 1);
lbvar_to_degree_.resize(index + 1);
lbvar_to_last_index_.resize(index + 1);
}
}
void PrecedencesPropagator::MarkIntegerVariableAsOptional(IntegerVariable i,
Literal is_present) {
AdjustSizeFor(i);
optional_literals_[i] = is_present.Index();
if (is_present.Index() >= potential_nodes_.size()) {
potential_nodes_.resize(is_present.Index().value() + 1);
}
potential_nodes_[is_present.Index()].push_back(i.value());
}
void PrecedencesPropagator::AddArc(IntegerVariable tail, IntegerVariable head,
int offset, LbVar offset_var,
LiteralIndex l) {
AdjustSizeFor(tail);
AdjustSizeFor(head);
if (offset_var != kNoLbVar) {
AdjustSizeFor(IntegerVariableOf(LbVar(offset_var)));
}
for (const bool forward : {true, false}) {
const LbVar tail_var = forward ? LbVarOf(tail) : MinusUbVarOf(head);
const LbVar head_var = forward ? LbVarOf(head) : MinusUbVarOf(tail);
// Since we add a new arc, we will need to consider its tail during the next
// propagation.
//
// TODO(user): Adding arcs and then calling Untrail() before Propagate()
// will cause this mecanism to break. Find a more robust implementation.
modified_vars_.Set(tail_var);
const int arc_index = arcs_.size();
if (l == kNoLiteralIndex) {
impacted_arcs_[tail_var].push_back(arc_index);
if (offset_var != kNoLbVar) {
impacted_arcs_[offset_var].push_back(arc_index);
}
} else {
impacted_potential_arcs_[tail_var].push_back(arc_index);
if (offset_var != kNoLbVar) {
impacted_potential_arcs_[offset_var].push_back(arc_index);
}
if (l.value() >= potential_arcs_.size()) {
potential_arcs_.resize(l.value() + 1);
}
potential_arcs_[l].push_back(arc_index);
}
arcs_.push_back({tail_var, head_var, offset, offset_var, l});
}
}
// TODO(user): On jobshop problems with a lot of tasks per machine (500), this
// takes up a big chunck of the running time even before we find a solution.
// This is because, for each LbVar changed, we inspect 500 arcs even though they
// will never be propagated because the other bound is still at the horizon.
// Find and even sparser algorithm?
void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
for (const LbVar var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= impacted_potential_arcs_.size()) continue;
// We can't deduce anything if this is the case.
if (!IsInvalidOrTrue(OptionalLiteralOf(var), *trail)) continue;
// Note that we can currently do the same computation up to 3 times:
// - if tail_var changed
// - if OtherLbVar(head_var) changed, we will process the "reverse" arc,
// but it will lead to the same computation and the same presence literal
// to be propagated.
// - if offset_var changed.
//
// Note(user): I tried another option, but it was slower:
// - keep the unique and even (i.e direct arc) arc_index.
// - Only call PropagateArcIfNeeded() on them.
for (const int arc_index : impacted_potential_arcs_[var]) {
const ArcInfo& arc = arcs_[arc_index];
const Literal is_present(arc.presence_l);
if (trail->Assignment().VariableIsAssigned(is_present.Variable())) {
continue;
}
// We can't deduce anything if the head node is optional and unassigned.
if (!IsInvalidOrTrue(OptionalLiteralOf(arc.head_var), *trail)) {
continue;
}
// We want the other bound of head to test infeasibility of the head
// IntegerVariable.
const LbVar other_head_var = OtherLbVar(arc.head_var);
const int tail_value = integer_trail_->Value(arc.tail_var);
const int head_value = integer_trail_->Value(other_head_var);
if (tail_value + ArcOffset(arc) > -head_value) {
std::vector<Literal>* literal_reason;
std::vector<IntegerLiteral>* integer_reason;
integer_trail_->EnqueueLiteral(is_present.Negated(), &literal_reason,
&integer_reason, trail);
integer_reason->push_back(integer_trail_->ValueAsLiteral(arc.tail_var));
integer_reason->push_back(
integer_trail_->ValueAsLiteral(other_head_var));
AppendValueIfValid(arc.offset_var, *integer_trail_, integer_reason);
AppendNegationIfValid(
optional_literals_[IntegerVariableOf(arc.tail_var)],
literal_reason);
AppendNegationIfValid(
optional_literals_[IntegerVariableOf(arc.head_var)],
literal_reason);
}
}
}
}
int PrecedencesPropagator::ArcOffset(const ArcInfo& arc) const {
return arc.offset + (arc.offset_var == kNoLbVar ? 0 : integer_trail_->Value(
arc.offset_var));
}
bool PrecedencesPropagator::EnqueueAndCheck(const ArcInfo& arc, int new_head_lb,
Trail* trail) {
DCHECK_GT(new_head_lb, integer_trail_->Value(arc.head_var));
// Compute the reason for new_head_lb.
literal_reason_.clear();
AppendNegationIfValid(arc.presence_l, &literal_reason_);
AppendNegationIfValid(optional_literals_[IntegerVariableOf(arc.tail_var)],
&literal_reason_);
integer_reason_.clear();
integer_reason_.push_back(integer_trail_->ValueAsLiteral(arc.tail_var));
AppendValueIfValid(arc.offset_var, *integer_trail_, &integer_reason_);
// Conflict?
const LbVar other_head_var = OtherLbVar(arc.head_var);
if (new_head_lb > -integer_trail_->Value(other_head_var)) {
integer_reason_.push_back(integer_trail_->ValueAsLiteral(other_head_var));
// This test if the head integer variable is either optional and present or
// always present, so if this is true then we have a conflict.
if (IsInvalidOrTrue(OptionalLiteralOf(arc.head_var), *trail)) {
std::vector<Literal>* conflict = trail->MutableConflict();
*conflict = literal_reason_;
integer_trail_->MergeReasonInto(integer_reason_, conflict);
return false;
} else {
// It is actually not a conflict if head is optional and not assigned.
const Literal lit(optional_literals_[IntegerVariableOf(arc.head_var)]);
if (!trail->Assignment().LiteralIsFalse(lit)) {
// TODO(user): better interface.
std::vector<Literal>* literal_reason_ptr;
std::vector<IntegerLiteral>* integer_reason_ptr;
integer_trail_->EnqueueLiteral(lit.Negated(), &literal_reason_ptr,
&integer_reason_ptr, trail);
*literal_reason_ptr = literal_reason_;
integer_reason_ptr->clear();
for (const IntegerLiteral l : integer_reason_) {
integer_reason_ptr->push_back(l);
}
}
}
// TRICKY: It is not really needed, but we still enqueue the new bound in
// this case so that:
// 1. Our sparse cleaning algo in CleanUpMarkedArcsAndParents() works.
// 2. NoPropagationLeft() is happy too.
}
// Propagate.
integer_trail_->Enqueue(IntegerLiteral::FromLbVar(arc.head_var, new_head_lb),
literal_reason_, integer_reason_);
return true;
}
bool PrecedencesPropagator::PropagateMaxOffsetIfNeeded(const ArcInfo& arc,
Trail* trail) {
if (arc.offset_var == kNoLbVar) return false;
if (!IsInvalidOrTrue(OptionalLiteralOf(arc.head_var), *trail)) return false;
const LbVar other_head_var = OtherLbVar(arc.head_var);
const int max_duration = -integer_trail_->Value(other_head_var) -
integer_trail_->Value(arc.tail_var);
const LbVar offset_ub = OtherLbVar(LbVar(arc.offset_var));
if (max_duration < -integer_trail_->Value(offset_ub)) {
literal_reason_.clear();
AppendNegationIfValid(arc.presence_l, &literal_reason_);
AppendNegationIfValid(optional_literals_[IntegerVariableOf(arc.tail_var)],
&literal_reason_);
integer_reason_.clear();
integer_reason_.push_back(integer_trail_->ValueAsLiteral(arc.tail_var));
integer_reason_.push_back(integer_trail_->ValueAsLiteral(other_head_var));
integer_trail_->Enqueue(IntegerLiteral::FromLbVar(offset_ub, -max_duration),
literal_reason_, integer_reason_);
return true;
}
return false;
}
bool PrecedencesPropagator::NoPropagationLeft(const Trail& trail) const {
const int num_nodes = impacted_arcs_.size();
for (LbVar var(0); var < num_nodes; ++var) {
for (const int index : impacted_arcs_[var]) {
const ArcInfo& arc = arcs_[index];
if (!IsInvalidOrTrue(OptionalLiteralOf(arc.tail_var), trail)) continue;
if (integer_trail_->Value(arc.tail_var) + ArcOffset(arc) >
integer_trail_->Value(arc.head_var)) {
return false;
}
}
}
return true;
}
void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
// Sparse clear of the queue. TODO(user): only use the sparse version if
// queue.size() is small or use SparseBitset.
const int num_nodes = impacted_arcs_.size();
bf_in_queue_.resize(num_nodes, false);
for (const int node : bf_queue_) bf_in_queue_[node] = false;
bf_queue_.clear();
DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
[](bool v) { return v; }));
for (const LbVar var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= num_nodes) continue;
bf_queue_.push_back(var.value());
bf_in_queue_[var.value()] = true;
}
}
void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
// To be sparse, we use the fact that each node with a parent must be in
// modified_vars_.
const int num_nodes = impacted_arcs_.size();
for (const LbVar var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= num_nodes) continue;
const int parent_arc_index = bf_parent_arc_of_[var.value()];
if (parent_arc_index != -1) {
arcs_[parent_arc_index].is_marked = false;
bf_parent_arc_of_[var.value()] = -1;
bf_can_be_skipped_[var.value()] = false;
}
}
DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
[](int v) { return v != -1; }));
DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
[](bool v) { return v; }));
}
bool PrecedencesPropagator::DisassembleSubtree(int source, int target,
std::vector<bool>* can_be_skipped) {
// Note that we explore a tree, so we can do it in any order, and the one
// below seems to be the fastest.
tmp_vector_.clear();
tmp_vector_.push_back(source);
while (!tmp_vector_.empty()) {
const int tail = tmp_vector_.back();
tmp_vector_.pop_back();
for (const int arc_index : impacted_arcs_[LbVar(tail)]) {
const ArcInfo& arc = arcs_[arc_index];
if (arc.is_marked) {
arc.is_marked = false; // mutable.
if (arc.head_var.value() == target) return true;
DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
(*can_be_skipped)[arc.head_var.value()] = true;
tmp_vector_.push_back(arc.head_var.value());
}
}
}
return false;
}
// Note(user): because of our "special" graph, we can't just follow the
// bf_parent_arc_of_[] to reconstruct the cycle, this is because given an arc,
// we don't know if it was impacted by its tail or by it offset_var (if not
// equal to kNoLbVar).
//
// Our solution is to walk again the forward graph using a DFS to reconstruct
// the arcs that form a positive cycle.
void PrecedencesPropagator::ReportPositiveCycle(int first_arc, Trail* trail) {
// TODO(user): I am not sure we have a theoretical guarantee than the
// set of arcs appearing in bf_parent_arc_of_[] form a tree here because
// we consider all of them, not just the non-maked one. Because of that,
// for now we use an extra vector to be on the safe side.
std::vector<bool> in_queue(impacted_arcs_.size(), false);
const int first_node = arcs_[first_arc].head_var.value();
tmp_vector_.clear();
tmp_vector_.push_back(first_node);
in_queue[first_node] = true;
std::vector<int> arc_queue{first_arc};
std::vector<int> arc_on_cycle{first_arc};
bool found = false;
while (!found && !tmp_vector_.empty()) {
const int node = tmp_vector_.back();
const int incoming_arc = arc_queue.back();
if (node == -1) {
// We are coming back up in the tree.
tmp_vector_.pop_back();
arc_queue.pop_back();
arc_on_cycle.pop_back();
continue;
}
// We are going down in the tree.
tmp_vector_.back() = -1; // Mark as explored.
arc_on_cycle.push_back(incoming_arc);
for (const int arc_index : impacted_arcs_[LbVar(node)]) {
if (arc_index == first_arc) {
// The cycle is complete.
found = true;
break;
}
const ArcInfo& arc = arcs_[arc_index];
// We already cleared is_marked, so we use a slower detection of the
// arc in the tree. Note that this code is called a lot less often than
// DisassembleSubtree(), so this is probably good enough.
const int head_node = arc.head_var.value();
if (!in_queue[head_node] && bf_parent_arc_of_[head_node] == arc_index) {
tmp_vector_.push_back(head_node);
arc_queue.push_back(arc_index);
in_queue[head_node] = true;
}
}
}
CHECK(found);
CHECK_EQ(arc_on_cycle.front(), first_arc);
// Report the positive cycle.
std::vector<Literal>* conflict = trail->MutableConflict();
integer_reason_.clear();
conflict->clear();
int sum = 0;
for (const int arc_index : arc_on_cycle) {
const ArcInfo& arc = arcs_[arc_index];
sum += ArcOffset(arc);
AppendValueIfValid(arc.offset_var, *integer_trail_, &integer_reason_);
AppendNegationIfValid(arc.presence_l, conflict);
AppendNegationIfValid(optional_literals_[IntegerVariableOf(arc.tail_var)],
conflict);
}
integer_trail_->MergeReasonInto(integer_reason_, conflict);
CHECK_GT(sum, 0);
// We don't want any duplicates.
// TODO(user): I think we could handle them, so maybe this is not needed.
STLSortAndRemoveDuplicates(conflict);
}
// Note that in our settings it is important to use an algorithm that tries to
// minimize the number of integer_trail_->Enqueue() as much as possible.
//
// TODO(user): The current algorithm is quite efficient, but there is probably
// still room for improvments.
bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
const int num_nodes = impacted_arcs_.size();
// These vector are reset by CleanUpMarkedArcsAndParents() so resize is ok.
bf_can_be_skipped_.resize(num_nodes, false);
bf_parent_arc_of_.resize(num_nodes, -1);
const auto cleanup =
::operations_research::util::MakeCleanup([this]() { CleanUpMarkedArcsAndParents(); });
// The queue initialization is done by InitializeBFQueueWithModifiedNodes().
while (!bf_queue_.empty()) {
const int node = bf_queue_.front();
bf_queue_.pop_front();
bf_in_queue_[node] = false;
// TODO(user): we don't need bf_can_be_skipped_ since we can detect this
// if this node has a parent arc which is not marked. Investigate if it is
// faster without the std::vector<bool>.
//
// TODO(user): An alternative algorithm is to remove all these nodes from
// the queue instead of simply marking them. This should also lead to a
// better "relaxation" order of the arcs. It is however a bit more work to
// remove them since we need to track their position.
if (bf_can_be_skipped_[node]) {
DCHECK_NE(bf_parent_arc_of_[node], -1);
DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
continue;
}
// Note that while this look like a graph traversal, it is slightly trickier
// because we may iterate on arcs without the same tail here (when the node
// appear as an offset_var). The algo should still work fine though.
for (const int arc_index : impacted_arcs_[LbVar(node)]) {
const ArcInfo& arc = arcs_[arc_index];
if (!IsInvalidOrTrue(OptionalLiteralOf(arc.tail_var), *trail)) continue;
if (PropagateMaxOffsetIfNeeded(arc, trail)) {
const LbVar offset_ub = OtherLbVar(LbVar(arc.offset_var));
// TODO(user): We currently don't have any cycle detection here.
bf_can_be_skipped_[offset_ub.value()] = false;
if (!bf_in_queue_[offset_ub.value()]) {
bf_queue_.push_back(offset_ub.value());
bf_in_queue_[offset_ub.value()] = true;
}
}
const int candidate =
integer_trail_->Value(arc.tail_var) + ArcOffset(arc);
if (candidate > integer_trail_->Value(arc.head_var)) {
if (!EnqueueAndCheck(arc, candidate, trail)) return false;
// This is the Tarjan contribution to Bellman-Ford. This code detect
// positive cycle, and because it disassemble the subtree while doing
// so, the cost is amortized during the algorithm execution. Another
// advantages is that it will mark the node explored here as skippable
// which will avoid to propagate them too early (knowing that they will
// need to be propagated again later).
if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
&bf_can_be_skipped_)) {
ReportPositiveCycle(arc_index, trail);
return false;
}
// We need to enforce the invariant that only the arc_index in
// bf_parent_arc_of_[] are marked (but not necessarily all of them since
// we unmark some in DisassembleSubtree()).
if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked = false;
}
bf_parent_arc_of_[arc.head_var.value()] = arc_index;
bf_can_be_skipped_[arc.head_var.value()] = false;
arcs_[arc_index].is_marked = true;
if (!bf_in_queue_[arc.head_var.value()]) {
bf_queue_.push_back(arc.head_var.value());
bf_in_queue_[arc.head_var.value()] = true;
}
}
}
}
return true;
}
} // namespace sat
} // namespace operations_research

292
src/sat/precedences.h Normal file
View File

@@ -0,0 +1,292 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_PRECEDENCES_H_
#define OR_TOOLS_SAT_PRECEDENCES_H_
#include <algorithm>
#include <queue>
#include "sat/integer.h"
#include "sat/model.h"
#include "sat/sat_base.h"
#include "sat/sat_solver.h"
#include "util/bitset.h"
namespace operations_research {
namespace sat {
// This class implement a propagator on simple inequalities between integer
// variables of the form (i1 + offset <= i2). The offset can be constant or
// given by the value of a third integer variable. Offsets can also be negative.
//
// The algorithm work by mapping the problem onto a graph where the edges carry
// the offset and the nodes correspond to one of the two bounds of an integer
// variable (lower_bound or -upper_bound). It then find the fixed point using an
// incremental variant of the Bellman-Ford(-Tarjan) algorithm.
//
// This is also known as an "integer difference logic theory" in the SMT world.
// Another word is "separation logic".
class PrecedencesPropagator : public Propagator {
public:
PrecedencesPropagator(IntegerTrail* integer_trail,
GenericLiteralWatcher* watcher)
: Propagator("PrecedencesPropagator"),
integer_trail_(integer_trail),
watcher_(watcher),
watcher_id_(watcher->Register(this)) {
integer_trail_->RegisterWatcher(&modified_vars_);
}
static PrecedencesPropagator* CreateInModel(Model* model) {
PrecedencesPropagator* precedences =
new PrecedencesPropagator(model->GetOrCreate<IntegerTrail>(),
model->GetOrCreate<GenericLiteralWatcher>());
// TODO(user): Find a way to have more control on the order in which
// the propagators are added.
model->GetOrCreate<SatSolver>()->AddPropagator(
std::unique_ptr<PrecedencesPropagator>(precedences));
return precedences;
}
bool Propagate(Trail* trail) final;
void Untrail(const Trail& trail, int trail_index) final;
// Add a precedence relation (i1 + offset <= i2) between integer variables.
void AddPrecedence(IntegerVariable i1, IntegerVariable i2);
void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2,
int offset);
// Same as above, but the relation is only true when the given literal is.
void AddConditionalPrecedence(IntegerVariable i1, IntegerVariable i2,
Literal l);
void AddConditionalPrecedenceWithOffset(IntegerVariable i1,
IntegerVariable i2, int offset,
Literal l);
// Note that we currently do not support marking a variable appearing as
// an offset_var as optional (with MarkIntegerVariableAsOptional()). We could
// give it a meaning (like the arcs are not propagated if it is optional), but
// the code currently do not implement this.
//
// TODO(user): support optional offset_var?
//
// TODO(user): the variable offset should probably be tested more because
// when I wrote this, I just had a couple of problems to test this on.
void AddPrecedenceWithVariableOffset(IntegerVariable i1, IntegerVariable i2,
LbVar offset_var);
// An optional integer variable has a special behavior:
// - If the bounds on i cross each other, then is_present must be false.
// - It will only propagate any outgoing arcs if is_present is true.
//
// TODO(user): Accept a BinaryImplicationGraph* here, so that and arc
// (tail -> head) can still propagate if tail.is_present => head.is_present.
// Note that such propagation is only useful if the status of tail presence
// is still undecided. Or at least propagate if both tail and head is_present
// are the same literal.
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_present);
// Finds all the LbVar that are "after" one of the LbVar in to_consider.
// Returns a vector of these precedences relation sorted by
// LbVarPrecedences.var so that it is efficient to find all the LbVar "before"
// another one.
//
// Note that we only consider direct precedences here. Given our usage, it may
// be better to compute the full reachability in the precedence graph, but in
// pratice that may be too slow. On a good note, because we have all the
// potential precedences between tasks in disjunctions, on a single machine,
// both notion should be the same since we automatically work on the
// transitive closure.
//
// Note that the LbVar in the vector are also returned in topological order
// for a more efficient propagation in
// DisjunctiveConstraint::PrecedencesPass() where this is used.
struct LbVarPrecedences {
int index; // in to_consider.
LbVar var; // An LbVar that is >= to to_consider[index].
LiteralIndex reason; // The reaon for it to be >= or kNoLiteralIndex.
// Only needed for testing.
bool operator==(const LbVarPrecedences& o) const {
return index == o.index && var == o.var && reason == o.reason;
}
};
void ComputePrecedences(const std::vector<LbVar>& to_consider,
std::vector<LbVarPrecedences>* output);
private:
// Information about an individual arc.
struct ArcInfo {
LbVar tail_var;
LbVar head_var;
int offset;
LbVar offset_var; // kNoLbVar if none.
LiteralIndex presence_l; // kNoLiteralIndex if none.
// Used temporarily by our implementation of the Bellman-Ford algorithm. It
// should be false at the beginning of BellmanFordTarjan().
mutable bool is_marked;
};
// Internal functions to add new precedence relations.
void AdjustSizeFor(IntegerVariable i);
void AddArc(IntegerVariable tail, IntegerVariable head, int offset,
LbVar offset_var, LiteralIndex l);
// Helper function for a slightly more readable code.
LiteralIndex OptionalLiteralOf(LbVar var) const {
return optional_literals_[IntegerVariableOf(var)];
}
// Enqueue a new lower bound for the variable arc.head_lb that was deduced
// from the current value of arc.tail_lb and the offset of this arc.
bool EnqueueAndCheck(const ArcInfo& arc, int new_head_lb, Trail* trail);
bool PropagateMaxOffsetIfNeeded(const ArcInfo& arc, Trail* trail);
int ArcOffset(const ArcInfo& arc) const;
// Inspect all the optional arcs that needs inspection (to stay sparse) and
// check if their presence literal can be propagated to false.
void PropagateOptionalArcs(Trail* trail);
// The core algorithm implementation is split in these functions. One must
// first call InitializeBFQueueWithModifiedNodes() that will push all the
// LbVar that have been modified since the last call. Then,
// BellmanFordTarjan() will take care of all the propagation and returns false
// in case of conflict. Internally, it uses DisassembleSubtree() which is the
// Tarjan variant to detect a possible positive cycle. Before exiting, it will
// call CleanUpMarkedArcsAndParents().
//
// The Tarjan version of the Bellam-Ford algorithm is really nice in our
// context because it was really easy to make it incremental. Moreover, it
// supports batch increment!
//
// This implementation is kind of unique because of our context and the fact
// that it is incremental, but a good reference is "Negative-cycle detection
// algorithms", Boris V. Cherkassky, Andrew V. Goldberg, 1996,
// http://people.cs.nctu.edu.tw/~tjshen/doc/ne.pdf
void InitializeBFQueueWithModifiedNodes();
bool BellmanFordTarjan(Trail* trail);
bool DisassembleSubtree(int source, int target, std::vector<bool>* can_be_skipped);
void ReportPositiveCycle(int first_arc, Trail* trail);
void CleanUpMarkedArcsAndParents();
// Loops over all the arcs and verify that there is no propagation left.
// This is only meant to be used in a DCHECK() and is not optimized.
bool NoPropagationLeft(const Trail& trail) const;
// External class needed to get the LbVar values and Enqueue new ones.
IntegerTrail* integer_trail_;
GenericLiteralWatcher* watcher_;
int watcher_id_;
// The key to our incrementality. This will be cleared once the propagation
// is done, and automatically updated by the integer_trail_ with all the
// LbVar that changed since the last clear.
SparseBitset<LbVar> modified_vars_;
// An arc needs to be inspected for propagation (i.e. is impacted) if:
// - Its tail_var changed.
// - Its offset_var changed.
//
// All the int are arc indices in the arcs_ vector.
//
// The first vector (impacted_arcs_) correspond to the arc currently present
// whereas the second vector (impacted_potential_arcs_) list all the potential
// arcs (the one not allways present) and is just used for propagation of the
// arc presence literals.
ITIVector<LbVar, std::vector<int>> impacted_arcs_;
ITIVector<LbVar, std::vector<int>> impacted_potential_arcs_;
// Temporary vectors used by ComputePrecedences().
ITIVector<LbVar, int> lbvar_to_degree_;
ITIVector<LbVar, int> lbvar_to_last_index_;
struct SortedLbVar {
LbVar var;
int lower_bound;
bool operator<(const SortedLbVar& other) const {
return lower_bound < other.lower_bound;
}
};
std::vector<SortedLbVar> tmp_sorted_lbvars_;
std::vector<LbVarPrecedences> tmp_precedences_;
// The set of arcs that must be added to impacted_arcs_ when a literal become
// true.
ITIVector<LiteralIndex, std::vector<int>> potential_arcs_;
// Used for MarkIntegerVariableAsOptional(). The nodes associated to an
// IntegerVariable whose entry is not kNoLiteralIndex will only propagate
// something to its neighbors if the coresponding literal is assigned to true.
ITIVector<IntegerVariable, LiteralIndex> optional_literals_;
ITIVector<LiteralIndex, std::vector<int>> potential_nodes_;
// TODO(user): rearranging the index so that the arc of the same node are
// consecutive like in StaticGraph should have a big performance impact.
std::vector<ArcInfo> arcs_;
// Temp vectors to hold the reason of an assignment.
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
// Temp vectors for the Bellman-Ford algorithm. The graph in which this
// algorithm works is in one to one correspondance with the LbVar in
// impacted_arcs_.
std::deque<int> bf_queue_;
std::vector<bool> bf_in_queue_;
std::vector<bool> bf_can_be_skipped_;
std::vector<int> bf_parent_arc_of_;
// Temp vector used by the tree traversal in DisassembleSubtree().
std::vector<int> tmp_vector_;
DISALLOW_COPY_AND_ASSIGN(PrecedencesPropagator);
};
// =============================================================================
// Implementation of the small API functions below.
// =============================================================================
inline void PrecedencesPropagator::AddPrecedence(IntegerVariable i1,
IntegerVariable i2) {
AddArc(i1, i2, /*offset=*/0, /*offset_var=*/kNoLbVar, /*l=*/kNoLiteralIndex);
}
inline void PrecedencesPropagator::AddPrecedenceWithOffset(IntegerVariable i1,
IntegerVariable i2,
int offset) {
AddArc(i1, i2, offset, /*offset_var=*/kNoLbVar, /*l=*/kNoLiteralIndex);
}
inline void PrecedencesPropagator::AddConditionalPrecedence(IntegerVariable i1,
IntegerVariable i2,
Literal l) {
AddArc(i1, i2, /*offset=*/0, /*offset_var=*/kNoLbVar, l.Index());
}
inline void PrecedencesPropagator::AddConditionalPrecedenceWithOffset(
IntegerVariable i1, IntegerVariable i2, int offset, Literal l) {
AddArc(i1, i2, offset, /*offset_var=*/kNoLbVar, l.Index());
}
inline void PrecedencesPropagator::AddPrecedenceWithVariableOffset(
IntegerVariable i1, IntegerVariable i2, LbVar offset_var) {
AddArc(i1, i2, /*offset=*/0, offset_var, /*l=*/kNoLiteralIndex);
}
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_PRECEDENCES_H_