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

sat: export from google3

Browse Source
This commit is contained in:
Corentin Le Molgat
2024-02-05 18:29:39 +01:00
committed by Mizux Seiha
parent 186362bd15
commit 4d3437e460
7 changed files with 128 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

118
ortools/sat/2d_orthogonal_packing.cc
View File

@@ -18,6 +18,7 @@
#include <limits>
#include <optional>
#include <string>
#include <tuple>
#include <utility>
#include <vector>
@@ -49,6 +50,8 @@ OrthogonalPackingInfeasibilityDetector::
num_trivial_conflicts_});
stats.push_back({"OrthogonalPackingInfeasibilityDetector/conflicts_two_items",
num_conflicts_two_items_});
stats.push_back({"OrthogonalPackingInfeasibilityDetector/no_energy_conflict",
num_scheduling_possible_});
shared_stats_->AddStats(stats);
}
@@ -220,6 +223,94 @@ std::vector<int> GetDffConflict(
return result;
}
// Tries a simple heuristic to find a solution for the Resource-Constrained
// Project Scheduling Problem (RCPSP). The RCPSP can be mapped to a
// 2d bin packing where one dimension (say, x) is chosen to represent the time,
// and every item is cut into items with size_x = 1 that must remain consecutive
// in the x-axis but do not need to be aligned on the y axis. This is often
// called the cumulative relaxation of the 2d bin packing problem.
//
// Bin-packing solution RCPSP solution
// --------------- ---------------
// | ********** | | ***** |
// | ********** | | ***** |
// | ##### | | **#####*** |
// | ##### | | **#####*** |
// --------------- ---------------
//
// One interesting property is if we find an energy conflict using a
// superadditive function it means the problem is infeasible both interpreted as
// a 2d bin packing and as a RCPSP problem. In practice, that means that if we
// find a RCPSP solution for a 2d bin packing problem, there is no point on
// using Maximal DFFs to search for energy conflicts.
//
// Returns true if it found a feasible solution to the RCPSP problem.
bool FindHeuristicSchedulingSolution(
absl::Span<const IntegerValue> sizes,
absl::Span<const IntegerValue> demands,
absl::Span<const int> heuristic_order, IntegerValue global_end_max,
IntegerValue capacity_max,
std::vector<std::pair<IntegerValue, IntegerValue>>& profile,
std::vector<std::pair<IntegerValue, IntegerValue>>& new_profile) {
// The profile (and new profile) is a set of (time, capa_left) pairs, ordered
// by increasing time and capa_left.
profile.clear();
profile.emplace_back(kMinIntegerValue, capacity_max);
profile.emplace_back(kMaxIntegerValue, capacity_max);
IntegerValue start_of_previous_task = kMinIntegerValue;
for (int i = 0; i < heuristic_order.size(); i++) {
const IntegerValue event_size = sizes[heuristic_order[i]];
const IntegerValue event_demand = demands[heuristic_order[i]];
const IntegerValue event_start_min = 0;
const IntegerValue event_start_max = global_end_max - event_size;
const IntegerValue start_min =
std::max(event_start_min, start_of_previous_task);
// Iterate on the profile to find the step that contains start_min.
// Then push until we find a step with enough capacity.
int current = 0;
while (profile[current + 1].first <= start_min ||
profile[current].second < event_demand) {
++current;
}
const IntegerValue actual_start =
std::max(start_min, profile[current].first);
start_of_previous_task = actual_start;
// Compatible with the event.start_max ?
if (actual_start > event_start_max) return false;
const IntegerValue actual_end = actual_start + event_size;
// No need to update the profile on the last loop.
if (i == heuristic_order.size() - 1) break;
// Update the profile.
new_profile.clear();
new_profile.push_back(
{actual_start, profile[current].second - event_demand});
++current;
while (profile[current].first < actual_end) {
new_profile.push_back(
{profile[current].first, profile[current].second - event_demand});
++current;
}
if (profile[current].first > actual_end) {
new_profile.push_back(
{actual_end, new_profile.back().second + event_demand});
}
while (current < profile.size()) {
new_profile.push_back(profile[current]);
++current;
}
profile.swap(new_profile);
}
return true;
}
} // namespace
void OrthogonalPackingInfeasibilityDetector::GetAllCandidatesForKForDff2(
@@ -433,10 +524,17 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl(
std::sort(index_by_decreasing_x_size_.begin(),
index_by_decreasing_x_size_.end(),
[&sizes_x](int a, int b) { return sizes_x[a] > sizes_x[b]; });
[&sizes_x, &sizes_y](int a, int b) {
// Break ties with y-size
return std::tie(sizes_x[a], sizes_y[a]) >
std::tie(sizes_x[b], sizes_y[b]);
});
std::sort(index_by_decreasing_y_size_.begin(),
index_by_decreasing_y_size_.end(),
[&sizes_y](int a, int b) { return sizes_y[a] > sizes_y[b]; });
[&sizes_y, &sizes_x](int a, int b) {
return std::tie(sizes_y[a], sizes_x[a]) >
std::tie(sizes_y[b], sizes_x[b]);
});
// First look for pairwise incompatible pairs.
if (options.use_pairwise) {
@@ -530,6 +628,22 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl(
}
if (options.use_dff_f2) {
// Checking for conflicts using f_2 is expensive, so first try a quick
// algorithm to check if there is no conflict to be found. See the comments
// on top of FindHeuristicSchedulingSolution().
if (FindHeuristicSchedulingSolution(
sizes_x, sizes_y, index_by_decreasing_x_size_,
bounding_box_size.first, bounding_box_size.second,
scheduling_profile_, new_scheduling_profile_) ||
FindHeuristicSchedulingSolution(
sizes_y, sizes_x, index_by_decreasing_y_size_,
bounding_box_size.second, bounding_box_size.first,
scheduling_profile_, new_scheduling_profile_)) {
num_scheduling_possible_++;
CHECK(result.result_ != OrthogonalPackingResult::Status::INFEASIBLE);
return result;
}
// We only check for conflicts applying this DFF on heights and widths, but
// not on both, which would be too expensive if done naively.
auto conflict = CheckFeasibilityWithDualFunction2(

4
ortools/sat/2d_orthogonal_packing.h
View File

@@ -130,8 +130,11 @@ class OrthogonalPackingInfeasibilityDetector {
absl::Span<const int> index_by_decreasing_x_size, IntegerValue x_bb_size,
IntegerValue y_bb_size, int max_number_of_parameters_to_check);
// Buffers cleared and reused at each call of TestFeasibility()
std::vector<int> index_by_decreasing_x_size_;
std::vector<int> index_by_decreasing_y_size_;
std::vector<std::pair<IntegerValue, IntegerValue>> scheduling_profile_;
std::vector<std::pair<IntegerValue, IntegerValue>> new_scheduling_profile_;
int64_t num_calls_ = 0;
int64_t num_conflicts_ = 0;
@@ -139,6 +142,7 @@ class OrthogonalPackingInfeasibilityDetector {
int64_t num_trivial_conflicts_ = 0;
int64_t num_conflicts_dff2_ = 0;
int64_t num_conflicts_dff0_ = 0;
int64_t num_scheduling_possible_ = 0;
absl::BitGenRef random_;
SharedStatistics* shared_stats_;

2
ortools/sat/cp_model.cc
View File

@@ -36,7 +36,7 @@ namespace sat {
BoolVar::BoolVar(int index, CpModelBuilder* builder)
: builder_(builder), index_(index) {}
BoolVar BoolVar::WithName(const std::string& name) {
BoolVar BoolVar::WithName(absl::string_view name) {
DCHECK(builder_ != nullptr);
if (builder_ == nullptr) return *this;
builder_->MutableProto()

2
ortools/sat/cp_model.h
View File

@@ -82,7 +82,7 @@ class BoolVar {
/// Sets the name of the variable.
/// Note that this will always set the "positive" version of this Boolean.
BoolVar WithName(const std::string& name);
BoolVar WithName(absl::string_view name);
/// Returns the name of the variable.
std::string Name() const;

13
ortools/sat/diffn.cc
View File

@@ -422,20 +422,13 @@ NonOverlappingRectanglesEnergyPropagator::FindConflict(
// our rectangle is the bounding box, and we need to fit inside it a set of
// items corresponding to the minimum intersection of the original items
// with this bounding box.
const bool use_expensive_heuristics =
(sizes_x.size() < 10) ||
// Propagating a large conflict is expensive, so it's worth running an
// expensive heuristic to make it smaller.
best_conflict.opp_result.GetResult() ==
OrthogonalPackingResult::Status::INFEASIBLE ||
!rectangles_with_too_much_energy.conflicts.empty();
const auto opp_result = orthogonal_packing_checker_.TestFeasibility(
sizes_x, sizes_y, {r.SizeX(), r.SizeY()},
OrthogonalPackingOptions{.use_pairwise = true,
OrthogonalPackingOptions{
.use_pairwise = true,
.use_dff_f0 = true,
.use_dff_f2 = true,
.dff2_max_number_of_parameters_to_check =
use_expensive_heuristics ? 25 : 3});
.dff2_max_number_of_parameters_to_check = 100});
if (opp_result.GetResult() == OrthogonalPackingResult::Status::INFEASIBLE &&
(best_conflict.opp_result.GetResult() !=
OrthogonalPackingResult::Status::INFEASIBLE ||

4
ortools/sat/probing.cc
View File

@@ -406,7 +406,7 @@ bool Prober::ProbeDnf(absl::string_view name,
num_new_literals_fixed_ > previous_num_literals_fixed) {
VLOG(1) << "ProbeDnf(" << name << ", num_fixed_literals="
<< num_new_literals_fixed_ - previous_num_literals_fixed
<< ", num_pushed_integer_bounds="
<< ", num_fixed_integer_bounds="
<< num_new_integer_bounds_ - previous_num_integer_bounds
<< ", num_valid_conjunctions=" << num_valid_conjunctions << "/"
<< dnf.size() << ")";
@@ -498,7 +498,7 @@ bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
bool FailedLiteralProbingRound(ProbingOptions options, Model* model) {
WallTimer wall_timer;
wall_timer.Start();
options.log_info |= VLOG_IS_ON(2);
options.log_info |= VLOG_IS_ON(1);
// Reset the solver in case it was already used.
auto* sat_solver = model->GetOrCreate<SatSolver>();

2
ortools/sat/samples/multiple_knapsack_sat.py
View File

@@ -86,7 +86,7 @@ def main() -> None:
for i in all_items:
if solver.value(x[i, b]) > 0:
print(
f"Item:{i} weight:{data['weights'][i]} value:{data['values'][i]}"
f'Item:{i} weight:{data["weights"][i]} value:{data["values"][i]}'
)
bin_weight += data["weights"][i]
bin_value += data["values"][i]