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

[CP-SAT] support pb24 problem formats; speed ups 2d packing; bugfixes; cleanups

Browse Source
This commit is contained in:
Laurent Perron
2025-04-02 19:07:51 +02:00
parent 9931110293
commit 61ddd9e109
21 changed files with 731 additions and 249 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
ortools/sat/2d_mandatory_overlap_propagator.cc
View File

@@ -24,6 +24,7 @@
#include "absl/types/span.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/integer_base.h"
#include "ortools/sat/model.h"
#include "ortools/sat/no_overlap_2d_helper.h"
#include "ortools/sat/scheduling_helpers.h"
@@ -57,18 +58,22 @@ bool MandatoryOverlapPropagator::Propagate() {
bool has_zero_area_boxes = false;
absl::Span<const TaskTime> tasks =
helper_.x_helper().TaskByIncreasingNegatedStartMax();
for (int i = tasks.size() - 1; i >= 0; --i) {
for (int i = tasks.size(); --i >= 0;) {
const int b = tasks[i].task_index;
if (!helper_.IsPresent(b)) continue;
const ItemWithVariableSize item = helper_.GetItemWithVariableSize(b);
if (item.x.start_max > item.x.end_min ||
item.y.start_max > item.y.end_min) {
continue;
}
mandatory_regions_.push_back({.x_min = item.x.start_max,
.x_max = item.x.end_min,
.y_min = item.y.start_max,
.y_max = item.y.end_min});
const IntegerValue x_start_max = helper_.x_helper().StartMax(b);
const IntegerValue x_end_min = helper_.x_helper().EndMin(b);
if (x_start_max > x_end_min) continue;
const IntegerValue y_start_max = helper_.y_helper().StartMax(b);
const IntegerValue y_end_min = helper_.y_helper().EndMin(b);
if (y_start_max > y_end_min) continue;
mandatory_regions_.push_back({.x_min = x_start_max,
.x_max = x_end_min,
.y_min = y_start_max,
.y_max = y_end_min});
mandatory_regions_index_.push_back(b);
if (mandatory_regions_.back().SizeX() == 0 ||

15
ortools/sat/2d_try_edge_propagator.cc
View File

@@ -23,6 +23,7 @@
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/log/vlog_is_on.h"
#include "absl/types/span.h"
#include "ortools/base/stl_util.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/integer.h"
@@ -31,6 +32,7 @@
#include "ortools/sat/no_overlap_2d_helper.h"
#include "ortools/sat/synchronization.h"
#include "ortools/sat/util.h"
#include "ortools/set_cover/base_types.h"
#include "ortools/set_cover/set_cover_heuristics.h"
#include "ortools/set_cover/set_cover_invariant.h"
#include "ortools/set_cover/set_cover_model.h"
@@ -117,9 +119,10 @@ bool TryEdgeRectanglePropagator::CanPlace(
.x_max = position.first + active_box_ranges_[box_index].x_size,
.y_min = position.second,
.y_max = position.second + active_box_ranges_[box_index].y_size};
const absl::Span<const Rectangle> mandatory_regions = mandatory_regions_;
for (const int i : has_mandatory_region_) {
if (i == box_index) continue;
const Rectangle& mandatory_region = mandatory_regions_[i];
const Rectangle& mandatory_region = mandatory_regions[i];
if (!mandatory_region.IsDisjoint(placed_box)) {
if (with_conflict != nullptr) {
with_conflict->AppendToLastVector(i);
@@ -149,10 +152,12 @@ bool TryEdgeRectanglePropagator::Propagate() {
// If a mandatory region is changed, we need to replace any cached box that
// now became overlapping with it.
const int num_active_ranges = active_box_ranges_.size();
for (const int mandatory_idx : changed_mandatory_) {
for (int i = 0; i < active_box_ranges_.size(); i++) {
const Rectangle& mandatory_region = mandatory_regions_[mandatory_idx];
for (int i = 0; i < num_active_ranges; i++) {
if (i == mandatory_idx || !is_in_cache_[i]) continue;
if (!placed_boxes_[i].IsDisjoint(mandatory_regions_[mandatory_idx])) {
if (!placed_boxes_[i].IsDisjoint(mandatory_region)) {
changed_item_.push_back(i);
is_in_cache_[i] = false;
}
@@ -323,8 +328,10 @@ std::vector<int> TryEdgeRectanglePropagator::GetMinimumProblemWithPropagation(
}
DCHECK(model.ComputeFeasibility());
SetCoverInvariant inv(&model);
GreedySolutionGenerator greedy_search(&inv);
LazyElementDegreeSolutionGenerator greedy_search(&inv);
CHECK(greedy_search.NextSolution());
LazySteepestSearch steepest_search(&inv);
CHECK(steepest_search.NextSolution());
GuidedLocalSearch search(&inv);
CHECK(search.SetMaxIterations(100).NextSolution());
DCHECK(inv.CheckConsistency(

35
ortools/sat/BUILD.bazel
View File

@@ -101,6 +101,7 @@ cc_library(
deps = [
":diffn_util",
":integer",
":integer_base",
":model",
":no_overlap_2d_helper",
":scheduling_helpers",
@@ -2377,19 +2378,23 @@ cc_test(
size = "small",
srcs = [
"boolean_problem_test.cc",
"opb_reader.h",
],
deps = [
":boolean_problem",
":boolean_problem_cc_proto",
":cp_model_cc_proto",
":cp_model_checker",
":cp_model_symmetries",
":opb_reader",
":sat_parameters_cc_proto",
"//ortools/algorithms:sparse_permutation",
"//ortools/base",
"//ortools/base:file",
"//ortools/base:gmock_main",
"//ortools/base:path",
"//ortools/util:filelineiter",
"//ortools/util:logging",
"//ortools/util:time_limit",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/status",
"@abseil-cpp//absl/strings",
],
)
@@ -3320,6 +3325,7 @@ cc_library(
":synchronization",
":util",
"//ortools/base:stl_util",
"//ortools/set_cover:base_types",
"//ortools/set_cover:set_cover_heuristics",
"//ortools/set_cover:set_cover_invariant",
"//ortools/set_cover:set_cover_model",
@@ -3328,6 +3334,7 @@ cc_library(
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/log:vlog_is_on",
"@abseil-cpp//absl/types:span",
],
)
@@ -3737,19 +3744,35 @@ cc_library(
],
)
cc_library(
name = "opb_reader",
hdrs = ["opb_reader.h"],
deps = [
":cp_model_cc_proto",
":cp_model_utils",
"//ortools/base",
"//ortools/base:stl_util",
"//ortools/util:filelineiter",
"@abseil-cpp//absl/container:flat_hash_map",
"@abseil-cpp//absl/container:flat_hash_set",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/strings",
"@abseil-cpp//absl/types:span",
],
)
cc_binary(
name = "sat_runner",
srcs = [
"opb_reader.h",
"sat_runner.cc",
],
deps = [
":boolean_problem",
":boolean_problem_cc_proto",
":cp_model_cc_proto",
":cp_model_solver",
":cp_model_utils",
":model",
":opb_reader",
":sat_cnf_reader",
":sat_parameters_cc_proto",
"//ortools/base",

100
ortools/sat/boolean_problem_test.cc
View File

@@ -18,7 +18,6 @@
#include <vector>
#include "absl/log/check.h"
#include "absl/status/status.h"
#include "absl/strings/str_cat.h"
#include "absl/strings/string_view.h"
#include "gtest/gtest.h"
@@ -26,66 +25,97 @@
#include "ortools/base/helpers.h"
#include "ortools/base/options.h"
#include "ortools/base/path.h"
#include "ortools/sat/boolean_problem.pb.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/cp_model_symmetries.h"
#include "ortools/sat/opb_reader.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/logging.h"
#include "ortools/util/time_limit.h"
namespace operations_research {
namespace sat {
namespace {
TEST(ValidateBooleanProblemTest, Ok) {
TEST(LoadAndValidateBooleanProblemTest, Ok) {
std::string file =
"min: 1 x1 1 x2 ;\n"
"1 x1 1 x2 >= 1 ;\n"
"1 x1 1 x2 >= 1 ;\n";
LinearBooleanProblem problem;
CpModelProto problem;
OpbReader reader;
const std::string filename = file::JoinPath(::testing::TempDir(), "file.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.Load(filename, &problem));
EXPECT_TRUE(ValidateBooleanProblem(problem).ok());
CHECK(reader.LoadAndValidate(filename, &problem));
EXPECT_TRUE(ValidateCpModel(problem).empty());
EXPECT_EQ(problem.variables_size(), 2);
EXPECT_EQ(reader.num_variables(), 2);
}
TEST(ValidateBooleanProblemTest, ZeroCoefficients) {
TEST(LoadAndValidateBooleanProblemTest, NonLinear) {
std::string file =
"min: 1 x1 1 x2 ~x3;\n"
"1 x1 1 x2 >= 1 ;\n"
"1 x1 x2 x3 >= 1 ;\n";
CpModelProto problem;
OpbReader reader;
const std::string filename = file::JoinPath(::testing::TempDir(), "file.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.LoadAndValidate(filename, &problem));
EXPECT_TRUE(ValidateCpModel(problem).empty());
EXPECT_EQ(problem.variables_size(), 5);
EXPECT_EQ(reader.num_variables(), 3);
}
TEST(LoadAndValidateBooleanProblemTest, Weighted) {
std::string file =
"1 x1 1 x2 >= 1 ;\n"
"[32] 2 x1 = 2 ;\n";
CpModelProto problem;
OpbReader reader;
const std::string filename = file::JoinPath(::testing::TempDir(), "file.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.LoadAndValidate(filename, &problem));
EXPECT_TRUE(ValidateCpModel(problem).empty());
EXPECT_EQ(problem.variables_size(), 3);
EXPECT_EQ(reader.num_variables(), 2);
ASSERT_TRUE(problem.has_objective());
EXPECT_EQ(problem.objective().vars_size(), 1);
EXPECT_EQ(problem.objective().vars(0), 2);
EXPECT_EQ(problem.objective().coeffs(0), 32);
}
TEST(LoadAndValidateBooleanProblemTest, ZeroCoefficients) {
std::string file =
"min: 1 x1 1 x2 ;\n"
"1 x1 0 x2 >= 1 ;\n"
"1 x1 1 x2 >= 1 ;\n";
LinearBooleanProblem problem;
CpModelProto problem;
OpbReader reader;
const std::string filename =
file::JoinPath(::testing::TempDir(), "file2.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.Load(filename, &problem));
EXPECT_FALSE(ValidateBooleanProblem(problem).ok());
}
TEST(ValidateBooleanProblemTest, DuplicateEntries) {
std::string file =
"min: 1 x1 1 x2 ;\n"
"1 x1 1 x2 1 x1 >= 1 ;\n"
"1 x1 1 x2 >= 1 ;\n";
LinearBooleanProblem problem;
OpbReader reader;
const std::string filename =
file::JoinPath(::testing::TempDir(), "file3.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.Load(filename, &problem));
EXPECT_FALSE(ValidateBooleanProblem(problem).ok());
EXPECT_FALSE(reader.LoadAndValidate(filename, &problem));
}
void FindSymmetries(
absl::string_view file,
std::vector<std::unique_ptr<SparsePermutation>>* generators) {
LinearBooleanProblem problem;
CpModelProto problem;
OpbReader reader;
static int counter = 4;
++counter;
const std::string filename = file::JoinPath(
::testing::TempDir(), absl::StrCat("file", counter, ".opb"));
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
CHECK(reader.Load(filename, &problem));
FindLinearBooleanProblemSymmetries(problem, generators);
CHECK(reader.LoadAndValidate(filename, &problem));
SatParameters params;
params.set_symmetry_level(2);
params.set_symmetry_detection_deterministic_time_limit(1000);
SolverLogger logger;
logger.EnableLogging(true);
TimeLimit time_limit;
FindCpModelSymmetries(params, problem, generators, &logger, &time_limit);
}
TEST(FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry1) {
@@ -96,19 +126,17 @@ TEST(FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry1) {
std::vector<std::unique_ptr<SparsePermutation>> generators;
FindSymmetries(file, &generators);
// Note that the permutation is on the literals:
// xi maps to 2i and not(xi) maps to 2i + 1.
EXPECT_EQ(generators.size(), 1);
EXPECT_EQ(generators[0]->DebugString(), "(0 2) (1 3)");
EXPECT_EQ(generators[0]->DebugString(), "(0 1)");
}
TEST(FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry2) {
TEST(DISABLED_FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry2) {
std::string file =
"min: 1 x1 1 x2 ;\n"
"-3 x1 -2 x2 >= -1 ;\n"; // This is simplified to both x1 and x2 false.
std::vector<std::unique_ptr<SparsePermutation>> generators;
FindSymmetries(file, &generators);
EXPECT_EQ(generators.size(), 1);
ASSERT_EQ(generators.size(), 1);
EXPECT_EQ(generators[0]->DebugString(), "(0 2) (1 3)");
}
@@ -120,18 +148,18 @@ TEST(FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry3) {
" 1 x3 2 x1 3 x2 >= 2 ;\n";
std::vector<std::unique_ptr<SparsePermutation>> generators;
FindSymmetries(file, &generators);
EXPECT_EQ(generators.size(), 1);
EXPECT_EQ(generators[0]->DebugString(), "(0 4 2) (1 5 3)");
ASSERT_EQ(generators.size(), 1);
EXPECT_EQ(generators[0]->DebugString(), "(0 2 1)");
}
TEST(FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry4) {
TEST(DISABLED_FindLinearBooleanProblemSymmetriesTest, ProblemWithSymmetry4) {
std::string file =
"min: 1 x1;\n"
" 1 x1 2 x2 >= 2 ;\n"
" 1 x1 -2 x3 >= 0 ;\n";
std::vector<std::unique_ptr<SparsePermutation>> generators;
FindSymmetries(file, &generators);
EXPECT_EQ(generators.size(), 1);
ASSERT_EQ(generators.size(), 1);
// x2 and not(x3) are equivalent.
EXPECT_EQ(generators[0]->DebugString(), "(2 5) (3 4)");

32
ortools/sat/clause.cc
View File

@@ -574,7 +574,8 @@ bool BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
// Tricky: If this is the first clause, the propagator will be added and
// assumed to be in a "propagated" state. This makes sure this is the case.
if (IsEmpty()) propagation_trail_index_ = trail_->Index();
if (no_constraint_ever_added_) propagation_trail_index_ = trail_->Index();
no_constraint_ever_added_ = false;
if (drat_proof_handler_ != nullptr) {
// TODO(user): Like this we will duplicate all binary clause from the
@@ -600,7 +601,6 @@ bool BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
NotifyPossibleDuplicate(a);
NotifyPossibleDuplicate(b);
is_dag_ = false;
num_implications_ += 2;
if (enable_sharing_ && add_binary_callback_ != nullptr) {
add_binary_callback_(a, b);
@@ -634,6 +634,10 @@ bool BinaryImplicationGraph::AddAtMostOne(
DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
if (at_most_one.size() <= 1) return true;
// Same as for AddBinaryClause().
if (no_constraint_ever_added_) propagation_trail_index_ = trail_->Index();
no_constraint_ever_added_ = false;
// Temporarily copy the at_most_one constraint at the end of
// at_most_one_buffer_. It will be cleaned up and added by
// CleanUpAndAddAtMostOnes().
@@ -788,7 +792,6 @@ bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(int base_index) {
NotifyPossibleDuplicate(a);
}
}
num_implications_ += at_most_one.size() * (at_most_one.size() - 1);
// This will erase the at_most_one from the buffer.
local_end = local_start;
@@ -1173,7 +1176,7 @@ void BinaryImplicationGraph::RemoveFixedVariables() {
// TODO(user): This might be a bit slow. Do not call all the time if needed,
// this shouldn't change the correctness of the code.
at_most_ones_.clear();
CleanUpAndAddAtMostOnes(/*base_index=*/0);
CHECK(CleanUpAndAddAtMostOnes(/*base_index=*/0));
DCHECK(InvariantsAreOk());
}
@@ -1428,6 +1431,7 @@ bool BinaryImplicationGraph::DetectEquivalences(bool log_info) {
const Literal rep = RepresentativeOf(l);
if (rep.Index() != representative) representative_list.push_back(rep);
}
dtime += 1e-8 * static_cast<double>(ref.size());
// Add representative <=> literal.
//
@@ -1449,7 +1453,8 @@ bool BinaryImplicationGraph::DetectEquivalences(bool log_info) {
// one.
at_most_ones_.clear();
int saved_trail_index = propagation_trail_index_;
CleanUpAndAddAtMostOnes(/*base_index=*/0);
if (!CleanUpAndAddAtMostOnes(/*base_index=*/0)) return false;
// This might have run the propagation on a few variables without taking
// into account the AMOs. Propagate again.
//
@@ -1459,12 +1464,6 @@ bool BinaryImplicationGraph::DetectEquivalences(bool log_info) {
propagation_trail_index_ = saved_trail_index;
Propagate(trail_);
}
num_implications_ = 0;
for (LiteralIndex i(0); i < size; ++i) {
num_implications_ += implications_[i].size();
}
dtime += 2e-8 * num_implications_;
}
time_limit_->AdvanceDeterministicTime(dtime);
@@ -1475,8 +1474,9 @@ bool BinaryImplicationGraph::DetectEquivalences(bool log_info) {
LOG_IF(INFO, log_info) << "SCC. " << num_equivalences
<< " redundant equivalent literals. "
<< num_fixed_during_scc << " fixed. "
<< num_implications_ << " implications left. "
<< implications_.size() << " literals."
<< ComputeNumImplicationsForLog()
<< " implications left. " << implications_.size()
<< " literals."
<< " size of at_most_one buffer = "
<< at_most_one_buffer_.size() << "."
<< " dtime: " << dtime
@@ -1640,7 +1640,6 @@ bool BinaryImplicationGraph::ComputeTransitiveReduction(bool log_info) {
direct_implications.resize(new_size);
direct_implications.shrink_to_fit();
num_new_redundant_implications += diff;
num_implications_ -= diff;
// Abort if the computation involved is too big.
if (work_done_in_mark_descendants_ > 1e8) {
@@ -1681,7 +1680,8 @@ bool BinaryImplicationGraph::ComputeTransitiveReduction(bool log_info) {
num_redundant_implications_ += num_new_redundant_implications;
LOG_IF(INFO, log_info) << "Transitive reduction removed "
<< num_new_redundant_implications << " literals. "
<< num_fixed << " fixed. " << num_implications_
<< num_fixed << " fixed. "
<< ComputeNumImplicationsForLog()
<< " implications left. " << implications_.size()
<< " literals." << " dtime: " << dtime
<< " wtime: " << wall_timer.Get()
@@ -2681,7 +2681,7 @@ void BinaryImplicationGraph::CleanupAllRemovedAndFixedVariables() {
// Clean-up at most ones.
at_most_ones_.clear();
CleanUpAndAddAtMostOnes(/*base_index=*/0);
CHECK(CleanUpAndAddAtMostOnes(/*base_index=*/0));
// Note that to please the invariant() we also removed fixed literal above.
DCHECK(InvariantsAreOk());

26
ortools/sat/clause.h
View File

@@ -520,10 +520,12 @@ class BinaryImplicationGraph : public SatPropagator {
// Resizes the data structure.
void Resize(int num_variables);
// Returns true if there is no constraints in this class.
bool IsEmpty() const final {
return num_implications_ == 0 && at_most_ones_.empty();
}
// Returns the "size" of this class, that is 2 * num_boolean_variables as
// updated by the larger Resize() call.
int64_t literal_size() const { return implications_.size(); }
// Returns true if no constraints where ever added to this class.
bool IsEmpty() const final { return no_constraint_ever_added_; }
// Adds the binary clause (a OR b), which is the same as (not a => b).
// Note that it is also equivalent to (not b => a).
@@ -721,9 +723,12 @@ class BinaryImplicationGraph : public SatPropagator {
// Returns the number of current implications. Note that a => b and not(b)
// => not(a) are counted separately since they appear separately in our
// propagation lists. The number of size 2 clauses that represent the same
// thing is half this number.
int64_t num_implications() const { return num_implications_; }
int64_t literal_size() const { return implications_.size(); }
// thing is half this number. This should only be used in logs.
int64_t ComputeNumImplicationsForLog() const {
int64_t result = 0;
for (const auto& list : implications_) result += list.size();
return result;
}
// Extract all the binary clauses managed by this class. The Output type must
// support an AddBinaryClause(Literal a, Literal b) function.
@@ -863,7 +868,7 @@ class BinaryImplicationGraph : public SatPropagator {
//
// If the final AMO size is smaller than the at_most_one_expansion_size
// parameters, we fully expand it.
bool CleanUpAndAddAtMostOnes(int base_index);
ABSL_MUST_USE_RESULT bool CleanUpAndAddAtMostOnes(int base_index);
// To be used in DCHECKs().
bool InvariantsAreOk();
@@ -878,6 +883,11 @@ class BinaryImplicationGraph : public SatPropagator {
Trail* trail_;
DratProofHandler* drat_proof_handler_ = nullptr;
// When problems do not have any implications or at_most_ones this allows to
// reduce the number of work we do here. This will be set to true the first
// time something is added.
bool no_constraint_ever_added_ = true;
// Binary reasons by trail_index. We need a deque because we kept pointers to
// elements of this array and this can dynamically change size.
std::deque<Literal> reasons_;

41
ortools/sat/clause_test.cc
View File

@@ -16,6 +16,7 @@
#include <algorithm>
#include <memory>
#include <numeric>
#include <optional>
#include <vector>
#include "absl/container/flat_hash_set.h"
@@ -194,9 +195,9 @@ TEST(BinaryImplicationGraphTest, TransitiveReduction) {
graph->AddBinaryClause(Literal(i, false), Literal(i, true));
}
EXPECT_EQ(graph->num_implications(), 10 * 9);
EXPECT_EQ(graph->ComputeNumImplicationsForLog(), 10 * 9);
EXPECT_TRUE(graph->ComputeTransitiveReduction());
EXPECT_EQ(graph->num_implications(), 9 * 2);
EXPECT_EQ(graph->ComputeNumImplicationsForLog(), 9 * 2);
}
// This basically just test our DCHECKs.
@@ -217,9 +218,9 @@ TEST(BinaryImplicationGraphTest, BasicRandomTransitiveReduction) {
graph->AddImplication(Literal(a, true), Literal(b, true));
}
EXPECT_EQ(graph->num_implications(), 2 * num_added);
EXPECT_EQ(graph->ComputeNumImplicationsForLog(), 2 * num_added);
EXPECT_TRUE(graph->ComputeTransitiveReduction());
EXPECT_LT(graph->num_implications(), num_added);
EXPECT_LT(graph->ComputeNumImplicationsForLog(), num_added);
}
// We generate a random 2-SAT problem, and check that the propagation is
@@ -421,6 +422,38 @@ TEST(BinaryImplicationGraphTest, RandomImpliedLiteral) {
EXPECT_THAT(seen, UnorderedLiteralsAre(-2, -4, -5, +6, +7));
}
TEST(BinaryImplicationGraphTest, DetectEquivalencePropagateThings) {
Model model;
auto* trail = model.GetOrCreate<Trail>();
auto* graph = model.GetOrCreate<BinaryImplicationGraph>();
trail->Resize(10);
graph->Resize(10);
EXPECT_TRUE(graph->AddAtMostOne(Literals({+1, +2, +3, +4})));
EXPECT_TRUE(graph->AddAtMostOne(Literals({-2, -1, +3, +4})));
EXPECT_TRUE(graph->AddAtMostOne(Literals({-4, -1, +2, +3})));
EXPECT_TRUE(graph->AddAtMostOne(Literals({-3, -1, +2, +4})));
EXPECT_TRUE(graph->DetectEquivalences());
}
void TryAmoEquivalences(absl::Span<const std::vector<int>> cliques) {
Model model;
auto* trail = model.GetOrCreate<Trail>();
auto* graph = model.GetOrCreate<BinaryImplicationGraph>();
trail->Resize(1000);
graph->Resize(1000);
for (const auto& clique : cliques) {
std::vector<Literal> literals;
for (const int i : clique) {
literals.push_back(Literal(i));
}
if (!graph->AddAtMostOne(literals)) {
return;
}
}
graph->DetectEquivalences();
}
} // namespace
} // namespace sat
} // namespace operations_research

122
ortools/sat/constraint_violation.cc
View File

@@ -53,6 +53,12 @@ int64_t ExprValue(const LinearExpressionProto& expr,
return result;
}
int64_t AffineValue(const ViewOfAffineLinearExpressionProto& affine,
absl::Span<const int64_t> solution) {
if (affine.coeff == 0) return affine.offset;
return affine.coeff * solution[affine.var] + affine.offset;
}
LinearExpressionProto ExprDiff(const LinearExpressionProto& a,
const LinearExpressionProto& b) {
LinearExpressionProto result;
@@ -1238,6 +1244,56 @@ int64_t CompiledNoOverlap2dConstraint::ComputeViolation(
return violation;
}
template <bool has_enforcement>
int64_t CompiledNoOverlap2dWithTwoBoxes<has_enforcement>::ViolationDelta(
int /*var*/, int64_t /*old_value*/, absl::Span<const int64_t> solution) {
if (has_enforcement) {
for (const int lit : enforcements_) {
if (!LiteralValue(lit, solution)) return -violation_;
}
}
const int64_t x1 = AffineValue(box1_.x_min, solution);
const int64_t X1 = AffineValue(box1_.x_max, solution);
const int64_t x2 = AffineValue(box2_.x_min, solution);
const int64_t X2 = AffineValue(box2_.x_max, solution);
const int64_t repair_x = std::min(X2 - x1, X1 - x2);
if (repair_x <= 0) return -violation_; // disjoint
const int64_t y1 = AffineValue(box1_.y_min, solution);
const int64_t Y1 = AffineValue(box1_.y_max, solution);
const int64_t y2 = AffineValue(box2_.y_min, solution);
const int64_t Y2 = AffineValue(box2_.y_max, solution);
const int64_t repair_y = std::min(Y2 - y1, Y1 - y2);
if (repair_y <= 0) return -violation_; // disjoint
const int64_t overlap_x =
std::min(std::max(std::min(X2 - x2, X1 - x1), int64_t{1}), repair_x);
const int64_t overlap_y =
std::min(std::max(std::min(Y2 - y2, Y1 - y1), int64_t{1}), repair_y);
return std::min(repair_x * overlap_y, repair_y * overlap_x) - violation_;
}
template <bool has_enforcement>
std::vector<int>
CompiledNoOverlap2dWithTwoBoxes<has_enforcement>::UsedVariables(
const CpModelProto& /*model_proto*/) const {
std::vector<int> result;
if (has_enforcement) {
for (const int ref : enforcements_) result.push_back(PositiveRef(ref));
}
box1_.x_min.AppendVarTo(result);
box1_.x_max.AppendVarTo(result);
box1_.y_min.AppendVarTo(result);
box1_.y_max.AppendVarTo(result);
box2_.x_min.AppendVarTo(result);
box2_.x_max.AppendVarTo(result);
box2_.y_min.AppendVarTo(result);
box2_.y_max.AppendVarTo(result);
gtl::STLSortAndRemoveDuplicates(&result);
return result;
}
// ----- CompiledCircuitConstraint -----
// The violation of a circuit has three parts:
@@ -1463,6 +1519,7 @@ LsEvaluator::LsEvaluator(const CpModelProto& cp_model,
const SatParameters& params, TimeLimit* time_limit)
: cp_model_(cp_model), params_(params), time_limit_(time_limit) {
var_to_constraints_.resize(cp_model_.variables_size());
var_to_dtime_estimate_.resize(cp_model_.variables_size());
jump_value_optimal_.resize(cp_model_.variables_size(), true);
num_violated_constraint_per_var_ignoring_objective_.assign(
cp_model_.variables_size(), 0);
@@ -1481,6 +1538,7 @@ LsEvaluator::LsEvaluator(
TimeLimit* time_limit)
: cp_model_(cp_model), params_(params), time_limit_(time_limit) {
var_to_constraints_.resize(cp_model_.variables_size());
var_to_dtime_estimate_.resize(cp_model_.variables_size());
jump_value_optimal_.resize(cp_model_.variables_size(), true);
num_violated_constraint_per_var_ignoring_objective_.assign(
cp_model_.variables_size(), 0);
@@ -1498,8 +1556,11 @@ void LsEvaluator::BuildVarConstraintGraph() {
for (int ct_index = 0; ct_index < constraints_.size(); ++ct_index) {
constraint_to_vars_[ct_index] =
constraints_[ct_index]->UsedVariables(cp_model_);
const double dtime = 1e-8 * constraint_to_vars_[ct_index].size();
for (const int var : constraint_to_vars_[ct_index]) {
var_to_constraints_[var].push_back(ct_index);
var_to_dtime_estimate_[var] += dtime;
}
}
@@ -1734,22 +1795,26 @@ void LsEvaluator::CompileOneConstraint(const ConstraintProto& ct) {
}
for (int i = 0; i + 1 < size; ++i) {
const IntervalConstraintProto& x_interval_i =
cp_model_.constraints(x_intervals[i]).interval();
const ConstraintProto& x_proto_i =
cp_model_.constraints(x_intervals[i]);
const IntervalConstraintProto& x_interval_i = x_proto_i.interval();
const int64_t x_min_start_i = ExprMin(x_interval_i.start(), cp_model_);
const int64_t x_max_end_i = ExprMax(x_interval_i.end(), cp_model_);
const IntervalConstraintProto& y_interval_i =
cp_model_.constraints(y_intervals[i]).interval();
const ConstraintProto& y_proto_i =
cp_model_.constraints(y_intervals[i]);
const IntervalConstraintProto& y_interval_i = y_proto_i.interval();
const int64_t y_min_start_i = ExprMin(y_interval_i.start(), cp_model_);
const int64_t y_max_end_i = ExprMax(y_interval_i.end(), cp_model_);
for (int j = i + 1; j < size; ++j) {
const IntervalConstraintProto& x_interval_j =
cp_model_.constraints(x_intervals[j]).interval();
const ConstraintProto& x_proto_j =
cp_model_.constraints(x_intervals[j]);
const IntervalConstraintProto& x_interval_j = x_proto_j.interval();
const int64_t x_min_start_j =
ExprMin(x_interval_j.start(), cp_model_);
const int64_t x_max_end_j = ExprMax(x_interval_j.end(), cp_model_);
const IntervalConstraintProto& y_interval_j =
cp_model_.constraints(y_intervals[j]).interval();
const ConstraintProto& y_proto_j =
cp_model_.constraints(y_intervals[j]);
const IntervalConstraintProto& y_interval_j = y_proto_j.interval();
const int64_t y_min_start_j =
ExprMin(y_interval_j.start(), cp_model_);
const int64_t y_max_end_j = ExprMax(y_interval_j.end(), cp_model_);
@@ -1757,14 +1822,20 @@ void LsEvaluator::CompileOneConstraint(const ConstraintProto& ct) {
y_min_start_i >= y_max_end_j || y_min_start_j >= y_max_end_i) {
continue;
}
ConstraintProto* diffn = expanded_constraints_.add_constraints();
diffn->mutable_no_overlap_2d()->add_x_intervals(x_intervals[i]);
diffn->mutable_no_overlap_2d()->add_x_intervals(x_intervals[j]);
diffn->mutable_no_overlap_2d()->add_y_intervals(y_intervals[i]);
diffn->mutable_no_overlap_2d()->add_y_intervals(y_intervals[j]);
CompiledNoOverlap2dConstraint* no_overlap_2d =
new CompiledNoOverlap2dConstraint(*diffn, cp_model_);
constraints_.emplace_back(no_overlap_2d);
const bool has_enforcement =
!x_proto_i.enforcement_literal().empty() ||
!x_proto_j.enforcement_literal().empty() ||
!y_proto_i.enforcement_literal().empty() ||
!y_proto_j.enforcement_literal().empty();
if (has_enforcement) {
constraints_.emplace_back(new CompiledNoOverlap2dWithTwoBoxes<true>(
x_proto_i, y_proto_i, x_proto_j, y_proto_j));
} else {
constraints_.emplace_back(
new CompiledNoOverlap2dWithTwoBoxes<false>(
x_proto_i, y_proto_i, x_proto_j, y_proto_j));
}
}
}
break;
@@ -1979,17 +2050,18 @@ double LsEvaluator::WeightedViolationDelta(
const int64_t old_value = mutable_solution[var];
mutable_solution[var] += delta;
const int num_linear_constraints = linear_evaluator_.num_constraints();
for (const int ct_index : var_to_constraints_[var]) {
// We assume linear time delta computation in number of variables.
// TODO(user): refine on a per constraint basis.
dtime_ += 1e-8 * static_cast<double>(constraint_to_vars_[ct_index].size());
// We assume linear time delta computation in number of variables.
// TODO(user): refine on a per constraint basis.
dtime_ += var_to_dtime_estimate_[var];
const int num_linear_constraints = linear_evaluator_.num_constraints();
const std::unique_ptr<CompiledConstraint>* data = constraints_.data();
const auto non_linear_weights = weights.subspan(num_linear_constraints);
for (const int ct_index : var_to_constraints_[var]) {
DCHECK_LT(ct_index, constraints_.size());
const int64_t ct_delta = constraints_[ct_index]->ViolationDelta(
var, old_value, mutable_solution);
result += static_cast<double>(ct_delta) *
weights[ct_index + num_linear_constraints];
const int64_t ct_delta =
data[ct_index]->ViolationDelta(var, old_value, mutable_solution);
result += static_cast<double>(ct_delta) * non_linear_weights[ct_index];
}
// Restore.

89
ortools/sat/constraint_violation.h
View File

@@ -23,6 +23,7 @@
#include "absl/container/flat_hash_map.h"
#include "absl/types/span.h"
#include "ortools/base/stl_util.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/util.h"
@@ -444,6 +445,7 @@ class LsEvaluator {
LinearIncrementalEvaluator linear_evaluator_;
std::vector<std::unique_ptr<CompiledConstraint>> constraints_;
std::vector<std::vector<int>> var_to_constraints_;
std::vector<double> var_to_dtime_estimate_;
std::vector<std::vector<int>> constraint_to_vars_;
std::vector<bool> jump_value_optimal_;
TimeLimit* time_limit_;
@@ -572,8 +574,8 @@ class NoOverlapBetweenTwoIntervals : public CompiledConstraint {
class CompiledNoOverlap2dConstraint : public CompiledConstraintWithProto {
public:
explicit CompiledNoOverlap2dConstraint(const ConstraintProto& ct_proto,
const CpModelProto& cp_model);
CompiledNoOverlap2dConstraint(const ConstraintProto& ct_proto,
const CpModelProto& cp_model);
~CompiledNoOverlap2dConstraint() override = default;
int64_t ComputeViolation(absl::Span<const int64_t> solution) override;
@@ -582,6 +584,89 @@ class CompiledNoOverlap2dConstraint : public CompiledConstraintWithProto {
const CpModelProto& cp_model_;
};
// This is more compact and faster to destroy than storing a
// LinearExpressionProto.
struct ViewOfAffineLinearExpressionProto {
explicit ViewOfAffineLinearExpressionProto(
const LinearExpressionProto& proto) {
if (!proto.vars().empty()) {
DCHECK_EQ(proto.vars().size(), 1);
var = proto.vars(0);
coeff = proto.coeffs(0);
}
offset = proto.offset();
}
void AppendVarTo(std::vector<int>& result) const {
if (coeff != 0) result.push_back(var);
}
int var = 0;
int64_t coeff = 0;
int64_t offset = 0;
};
template <bool has_enforcement = true>
class CompiledNoOverlap2dWithTwoBoxes : public CompiledConstraint {
public:
struct Box {
Box(const ConstraintProto& x, const ConstraintProto& y)
: x_min(x.interval().start()),
x_max(x.interval().end()),
y_min(y.interval().start()),
y_max(y.interval().end()) {}
ViewOfAffineLinearExpressionProto x_min;
ViewOfAffineLinearExpressionProto x_max;
ViewOfAffineLinearExpressionProto y_min;
ViewOfAffineLinearExpressionProto y_max;
};
CompiledNoOverlap2dWithTwoBoxes(const ConstraintProto& x1,
const ConstraintProto& y1,
const ConstraintProto& x2,
const ConstraintProto& y2)
: box1_(x1, y1), box2_(x2, y2) {
if (has_enforcement) {
enforcements_.assign(x1.enforcement_literal().begin(),
x1.enforcement_literal().end());
enforcements_.insert(enforcements_.end(),
y1.enforcement_literal().begin(),
y1.enforcement_literal().end());
enforcements_.insert(enforcements_.end(),
x2.enforcement_literal().begin(),
x2.enforcement_literal().end());
enforcements_.insert(enforcements_.end(),
y2.enforcement_literal().begin(),
y2.enforcement_literal().end());
gtl::STLSortAndRemoveDuplicates(&enforcements_);
}
}
~CompiledNoOverlap2dWithTwoBoxes() final = default;
int64_t ComputeViolation(absl::Span<const int64_t> solution) final {
// Optimization hack: If we create a ComputeViolationInternal() that we call
// from here and in ViolationDelta(), then the later is not inlined below in
// ViolationDelta() where it matter a lot for performance.
violation_ = 0;
violation_ = ViolationDelta(0, 0, solution);
return violation_;
}
// Note(user): this is the same implementation as the base one, but it
// avoid one virtual call !
int64_t ViolationDelta(
int /*var*/, int64_t /*old_value*/,
absl::Span<const int64_t> solution_with_new_value) final;
std::vector<int> UsedVariables(const CpModelProto& model_proto) const final;
private:
std::vector<int> enforcements_;
const Box box1_;
const Box box2_;
};
// This can be used to encode reservoir or a cumulative constraints for LS. We
// have a set of event time, and we use for overal violation the sum of overload
// over time.

51
ortools/sat/diffn.cc
View File

@@ -638,7 +638,8 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
// Optimization: we only initialize the set if we don't have all task here.
absl::flat_hash_set<int> requested_boxes_set;
if (requested_boxes.size() != helper_->NumBoxes()) {
const bool not_all_boxes = requested_boxes.size() != helper_->NumBoxes();
if (not_all_boxes) {
requested_boxes_set = {requested_boxes.begin(), requested_boxes.end()};
}
@@ -648,10 +649,7 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
auto fixed_boxes = already_checked_fixed_boxes_.view();
for (int i = temp.size(); --i >= 0;) {
const int box = temp[i].task_index;
if (requested_boxes.size() != helper_->NumBoxes() &&
!requested_boxes_set.contains(box)) {
continue;
}
if (not_all_boxes && !requested_boxes_set.contains(box)) continue;
// By definition, fixed boxes are always present.
// Doing this check optimize a bit the case where we have many fixed boxes.
@@ -910,43 +908,36 @@ bool RectanglePairwisePropagator::Propagate() {
point_zero_area_boxes_.clear();
fixed_non_zero_area_boxes_.clear();
non_fixed_non_zero_area_boxes_.clear();
fixed_non_zero_area_rectangles_.clear();
for (int b : helper_->connected_components()[component_index]) {
if (!helper_->IsPresent(b)) continue;
const auto [x_size_max, y_size_max] = helper_->GetBoxSizesMax(b);
ItemWithVariableSize* box;
ItemWithVariableSize box = helper_->GetItemWithVariableSize(b);
if (x_size_max == 0) {
if (y_size_max == 0) {
box = &point_zero_area_boxes_.emplace_back();
point_zero_area_boxes_.push_back(std::move(box));
} else {
box = &vertical_zero_area_boxes_.emplace_back();
vertical_zero_area_boxes_.push_back(std::move(box));
}
} else if (y_size_max == 0) {
box = &horizontal_zero_area_boxes_.emplace_back();
horizontal_zero_area_boxes_.push_back(std::move(box));
} else {
if (helper_->IsFixed(b)) {
box = &fixed_non_zero_area_boxes_.emplace_back();
fixed_non_zero_area_rectangles_.push_back(
helper_->GetItemRangeForSizeMin(b).bounding_area);
// TODO(user): if the number of fixed boxes is large, we keep
// reconstructing them each time this is called for no reason.
if (box.IsFixed()) {
fixed_non_zero_area_boxes_.push_back(std::move(box));
} else {
box = &non_fixed_non_zero_area_boxes_.emplace_back();
non_fixed_non_zero_area_boxes_.push_back(std::move(box));
}
}
*box = helper_->GetItemWithVariableSize(b);
}
// We ignore pairs of two fixed boxes. The only thing to propagate between
// two fixed boxes is a conflict and it should already have been taken care
// of by the MandatoryOverlapPropagator propagator.
RETURN_IF_FALSE(FindRestrictionsAndPropagateConflict(
non_fixed_non_zero_area_boxes_, fixed_non_zero_area_boxes_,
&restrictions));
RETURN_IF_FALSE(FindRestrictionsAndPropagateConflict(
fixed_non_zero_area_boxes_, non_fixed_non_zero_area_boxes_,
&restrictions));
// Check zero area boxes against non-zero area boxes.
for (auto& non_zero_area_boxes :
{fixed_non_zero_area_boxes_, non_fixed_non_zero_area_boxes_}) {
@@ -968,24 +959,6 @@ bool RectanglePairwisePropagator::Propagate() {
return true;
}
bool RectanglePairwisePropagator::FindRestrictionsAndPropagateConflict(
absl::Span<const ItemWithVariableSize> items,
std::vector<PairwiseRestriction>* restrictions) {
const int max_pairs =
params_->max_pairs_pairwise_reasoning_in_no_overlap_2d();
if (items.size() * (items.size() - 1) / 2 > max_pairs) {
return true;
}
AppendPairwiseRestrictions(items, restrictions);
for (const PairwiseRestriction& restriction : *restrictions) {
if (restriction.type ==
PairwiseRestriction::PairwiseRestrictionType::CONFLICT) {
RETURN_IF_FALSE(PropagateTwoBoxes(restriction));
}
}
return true;
}
bool RectanglePairwisePropagator::FindRestrictionsAndPropagateConflict(
absl::Span<const ItemWithVariableSize> items1,
absl::Span<const ItemWithVariableSize> items2,

5
ortools/sat/diffn.h
View File

@@ -167,10 +167,6 @@ class RectanglePairwisePropagator : public PropagatorInterface {
delete;
// Return false if a conflict is found.
bool FindRestrictionsAndPropagateConflict(
absl::Span<const ItemWithVariableSize> items,
std::vector<PairwiseRestriction>* restrictions);
bool FindRestrictionsAndPropagateConflict(
absl::Span<const ItemWithVariableSize> items1,
absl::Span<const ItemWithVariableSize> items2,
@@ -186,7 +182,6 @@ class RectanglePairwisePropagator : public PropagatorInterface {
int64_t num_pairwise_conflicts_ = 0;
int64_t num_pairwise_propagations_ = 0;
std::vector<Rectangle> fixed_non_zero_area_rectangles_;
std::vector<ItemWithVariableSize> fixed_non_zero_area_boxes_;
std::vector<ItemWithVariableSize> non_fixed_non_zero_area_boxes_;
std::vector<ItemWithVariableSize> horizontal_zero_area_boxes_;

61
ortools/sat/diffn_util.cc
View File

@@ -599,55 +599,51 @@ void AppendPairwiseRestriction(const ItemWithVariableSize& item1,
return;
}
PairwiseRestriction::PairwiseRestrictionType type;
switch (state) {
case 0:
// Conflict. The two boxes must overlap in both dimensions.
result->push_back(
{.first_index = item1.index,
.second_index = item2.index,
.type = PairwiseRestriction::PairwiseRestrictionType::CONFLICT});
type = PairwiseRestriction::PairwiseRestrictionType::CONFLICT;
break;
case 1:
// box2 can only be after box1 on x.
if (item1.x.end_min > item2.x.start_min ||
item2.x.start_max < item1.x.end_max) {
result->push_back({.first_index = item1.index,
.second_index = item2.index,
.type = PairwiseRestriction::
PairwiseRestrictionType::FIRST_LEFT_OF_SECOND});
type =
PairwiseRestriction::PairwiseRestrictionType::FIRST_LEFT_OF_SECOND;
break;
}
break;
case 2: // box1 an only be after box2 on x.
return;
case 2:
// box1 can only be after box2 on x.
if (item2.x.end_min > item1.x.start_min ||
item1.x.start_max < item2.x.end_max) {
result->push_back({.first_index = item1.index,
.second_index = item2.index,
.type = PairwiseRestriction::
PairwiseRestrictionType::FIRST_RIGHT_OF_SECOND});
type =
PairwiseRestriction::PairwiseRestrictionType::FIRST_RIGHT_OF_SECOND;
break;
}
break;
return;
case 4:
// box2 an only be after box1 on y.
// box2 can only be after box1 on y.
if (item1.y.end_min > item2.y.start_min ||
item2.y.start_max < item1.y.end_max) {
result->push_back({.first_index = item1.index,
.second_index = item2.index,
.type = PairwiseRestriction::
PairwiseRestrictionType::FIRST_BELOW_SECOND});
type = PairwiseRestriction::PairwiseRestrictionType::FIRST_BELOW_SECOND;
break;
}
break;
case 8: // box1 an only be after box2 on y.
return;
case 8:
// box1 can only be after box2 on y.
if (item2.y.end_min > item1.y.start_min ||
item1.y.start_max < item2.y.end_max) {
result->push_back({.first_index = item1.index,
.second_index = item2.index,
.type = PairwiseRestriction::
PairwiseRestrictionType::FIRST_ABOVE_SECOND});
type = PairwiseRestriction::PairwiseRestrictionType::FIRST_ABOVE_SECOND;
break;
}
break;
return;
default:
break;
return;
}
result->push_back(
{.first_index = item1.index, .second_index = item2.index, .type = type});
}
} // namespace
@@ -1942,8 +1938,7 @@ PostProcessedResult ConvertToRectangle32WithNonZeroSizes(
IntegerValue prev_y = 0;
Event prev_event = Event::kEnd;
int cur_index = -1;
for (int i = 0; i < y_events.size(); ++i) {
const auto [y, event, index] = y_events[i];
for (const auto [y, event, index] : y_events) {
if ((prev_event != event && prev_event != Event::kEnd) || prev_y != y ||
event == Event::kPoint || cur_index == -1) {
++cur_index;
@@ -1974,8 +1969,7 @@ PostProcessedResult ConvertToRectangle32WithNonZeroSizes(
IntegerValue prev_x = 0;
prev_event = Event::kEnd;
cur_index = -1;
for (int i = 0; i < x_events.size(); ++i) {
const auto [x, event, index] = x_events[i];
for (const auto [x, event, index] : x_events) {
if ((prev_event != event && prev_event != Event::kEnd) || prev_x != x ||
event == Event::kPoint || cur_index == -1) {
++cur_index;
@@ -2000,8 +1994,7 @@ PostProcessedResult ConvertToRectangle32WithNonZeroSizes(
std::vector<Rectangle32> sorted_rectangles32;
sorted_rectangles32.reserve(rectangles.size());
for (int i = 0; i < x_events.size(); ++i) {
const auto [x, event, index] = x_events[i];
for (const auto [x, event, index] : x_events) {
if (event == Event::kBegin || event == Event::kPoint) {
sorted_rectangles32.push_back(rectangles32[index]);
}

13
ortools/sat/diffn_util.h
View File

@@ -269,15 +269,18 @@ std::vector<int> GetIntervalArticulationPoints(
std::vector<IndexedInterval>* intervals);
struct ItemWithVariableSize {
int index;
struct Interval {
bool IsFixed() const {
return start_min == start_max && end_min == end_max;
}
IntegerValue start_min;
IntegerValue start_max;
IntegerValue end_min;
IntegerValue end_max;
};
Interval x;
Interval y;
bool IsFixed() const { return x.IsFixed() && y.IsFixed(); }
template <typename Sink>
friend void AbslStringify(Sink& sink, const ItemWithVariableSize& item) {
@@ -286,6 +289,10 @@ struct ItemWithVariableSize {
item.x.end_max, item.y.start_min, item.y.start_max,
item.y.end_min, item.y.end_max);
}
int index;
Interval x;
Interval y;
};
struct PairwiseRestriction {

20
ortools/sat/integer_expr.cc
View File

@@ -1524,6 +1524,7 @@ bool FixedModuloPropagator::PropagateSignsAndTargetRange() {
// The sign of target_ is fixed by the sign of expr_.
if (integer_trail_->LowerBound(expr_) >= 0 &&
integer_trail_->LowerBound(target_) < 0) {
// expr >= 0 => target >= 0.
if (!integer_trail_->SafeEnqueue(target_.GreaterOrEqual(0),
{expr_.GreaterOrEqual(0)})) {
return false;
@@ -1532,12 +1533,31 @@ bool FixedModuloPropagator::PropagateSignsAndTargetRange() {
if (integer_trail_->UpperBound(expr_) <= 0 &&
integer_trail_->UpperBound(target_) > 0) {
// expr <= 0 => target <= 0.
if (!integer_trail_->SafeEnqueue(target_.LowerOrEqual(0),
{expr_.LowerOrEqual(0)})) {
return false;
}
}
if (integer_trail_->LowerBound(target_) > 0 &&
integer_trail_->LowerBound(expr_) <= 0) {
// target > 0 => expr > 0.
if (!integer_trail_->SafeEnqueue(expr_.GreaterOrEqual(1),
{target_.GreaterOrEqual(1)})) {
return false;
}
}
if (integer_trail_->UpperBound(target_) < 0 &&
integer_trail_->UpperBound(expr_) >= 0) {
// target < 0 => expr < 0.
if (!integer_trail_->SafeEnqueue(expr_.LowerOrEqual(-1),
{target_.LowerOrEqual(-1)})) {
return false;
}
}
return true;
}

294
ortools/sat/opb_reader.h
View File

@@ -16,14 +16,22 @@
#include <algorithm>
#include <cstdint>
#include <limits>
#include <string>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/strings/numbers.h"
#include "absl/strings/str_split.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/sat/boolean_problem.pb.h"
#include "ortools/base/stl_util.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/util/filelineiter.h"
namespace operations_research {
@@ -31,7 +39,7 @@ namespace sat {
// This class loads a file in pbo file format into a LinearBooleanProblem.
// The format is described here:
// http://www.cril.univ-artois.fr/PB12/format.pdf
// http://www.cril.univ-artois.fr/PB24/format.pdf
class OpbReader {
public:
OpbReader() = default;
@@ -39,25 +47,69 @@ class OpbReader {
OpbReader(const OpbReader&) = delete;
OpbReader& operator=(const OpbReader&) = delete;
// Returns the number of variables in the problem.
int num_variables() const { return num_variables_; }
// Loads the given opb filename into the given problem.
bool Load(const std::string& filename, LinearBooleanProblem* problem) {
problem->Clear();
problem->set_name(ExtractProblemName(filename));
// Returns true on success.
bool LoadAndValidate(const std::string& filename, CpModelProto* model) {
model->Clear();
model->set_name(ExtractProblemName(filename));
num_variables_ = 0;
int num_lines = 0;
// Read constraints line by line (1 constraint per line).
// We process into a temporary structure to support non linear constraints
// and weighted constraints.
for (const std::string& line : FileLines(filename)) {
++num_lines;
ProcessNewLine(problem, line);
ProcessNewLine(line);
}
if (num_lines == 0) {
LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";
LOG(ERROR) << "File '" << filename << "' is empty or can't be read.";
return false;
}
problem->set_num_variables(num_variables_);
LOG(INFO) << "Read " << num_lines << " lines from " << filename;
LOG(INFO) << "#variables: " << num_variables_;
LOG(INFO) << "#constraints: " << constraints_.size();
LOG(INFO) << "#objective: " << objective_.size();
const std::string error_message = ValidateModel();
if (!error_message.empty()) {
LOG(ERROR) << "Error while trying to parse '" << filename
<< "': " << error_message;
return false;
}
BuildModel(model);
return true;
}
private:
// A term is coeff * Product(literals).
// Note that it is okay to have duplicate literals here, we will just merge
// them. Having a literal and its negation will always result in a product of
// zero.
struct PbTerm {
int64_t coeff;
std::vector<int> literals; // CpModelProto literals
};
enum PbConstraintType {
UNDEFINED_OPERATION,
GE_OPERATION,
EQ_OPERATION,
};
struct PbConstraint {
std::vector<PbTerm> terms;
PbConstraintType type = UNDEFINED_OPERATION;
int64_t rhs = std::numeric_limits<int64_t>::min();
int64_t soft_cost = std::numeric_limits<int64_t>::max();
};
// Since the problem name is not stored in the cnf format, we infer it from
// the file name.
static std::string ExtractProblemName(const std::string& filename) {
@@ -67,71 +119,233 @@ class OpbReader {
return problem_name;
}
void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) {
void ProcessNewLine(const std::string& line) {
const std::vector<std::string> words =
absl::StrSplit(line, absl::ByAnyChar(" ;"), absl::SkipEmpty());
if (words.empty() || words[0].empty() || words[0][0] == '*') {
// TODO(user): Parse comments.
return;
}
if (words[0] == "min:") {
LinearObjective* objective = problem->mutable_objective();
for (int i = 1; i < words.size(); ++i) {
const std::string& word = words[i];
if (word.empty() || word[0] == ';') continue;
if (word[0] == 'x') {
int literal;
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
num_variables_ = std::max(num_variables_, literal);
objective->add_literals(literal);
int index;
CHECK(absl::SimpleAtoi(word.substr(1), &index));
num_variables_ = std::max(num_variables_, index);
objective_.back().literals.push_back(
PbLiteralToCpModelLiteral(index));
} else if (word[0] == '~' && word[1] == 'x') {
int index;
CHECK(absl::SimpleAtoi(word.substr(2), &index));
num_variables_ = std::max(num_variables_, index);
objective_.back().literals.push_back(
NegatedRef(PbLiteralToCpModelLiteral(index)));
} else {
int64_t value;
CHECK(absl::SimpleAtoi(word, &value));
objective->add_coefficients(value);
int64_t coefficient;
CHECK(absl::SimpleAtoi(word, &coefficient));
objective_.push_back({coefficient, {}});
}
}
if (objective->literals_size() != objective->coefficients_size()) {
LOG(INFO) << "words.size() = " << words.size();
LOG(FATAL) << "Failed to parse objective:\n " << line;
// Normalize objective literals.
for (PbTerm& term : objective_) {
if (term.literals.size() <= 1) continue;
gtl::STLSortAndRemoveDuplicates(&term.literals);
CHECK_GT(term.literals.size(), 1);
}
return;
}
LinearBooleanConstraint* constraint = problem->add_constraints();
PbConstraint constraint;
for (int i = 0; i < words.size(); ++i) {
const std::string& word = words[i];
CHECK(!word.empty());
if (word == ">=") {
if (word[0] == '[') { // Soft constraint.
int64_t soft_cost;
CHECK(absl::SimpleAtoi(word.substr(1, word.size() - 2), &soft_cost));
constraint.soft_cost = soft_cost;
} else if (word == ">=") {
CHECK_LT(i + 1, words.size());
int64_t value;
CHECK(absl::SimpleAtoi(words[i + 1], &value));
constraint->set_lower_bound(value);
int64_t rhs;
CHECK(absl::SimpleAtoi(words[i + 1], &rhs));
constraint.type = GE_OPERATION;
constraint.rhs = rhs;
break;
} else if (word == "=") {
CHECK_LT(i + 1, words.size());
int64_t value;
CHECK(absl::SimpleAtoi(words[i + 1], &value));
constraint->set_upper_bound(value);
constraint->set_lower_bound(value);
int64_t rhs;
CHECK(absl::SimpleAtoi(words[i + 1], &rhs));
constraint.type = EQ_OPERATION;
constraint.rhs = rhs;
break;
} else if (word[0] == 'x') {
int index;
CHECK(absl::SimpleAtoi(word.substr(1), &index));
num_variables_ = std::max(num_variables_, index);
constraint.terms.back().literals.push_back(
PbLiteralToCpModelLiteral(index));
} else if (word[0] == '~' && word[1] == 'x') {
int index;
CHECK(absl::SimpleAtoi(word.substr(2), &index));
num_variables_ = std::max(num_variables_, index);
constraint.terms.back().literals.push_back(
NegatedRef(PbLiteralToCpModelLiteral(index)));
} else {
if (word[0] == 'x') {
int literal;
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
num_variables_ = std::max(num_variables_, literal);
constraint->add_literals(literal);
} else {
int64_t value;
CHECK(absl::SimpleAtoi(words[i], &value));
constraint->add_coefficients(value);
// Note that coefficient always appear before the variable/variables.
int64_t coefficient;
CHECK(absl::SimpleAtoi(word, &coefficient));
constraint.terms.push_back({coefficient, {}});
}
}
// Normalize literals.
for (PbTerm& term : constraint.terms) {
if (term.literals.size() <= 1) continue;
gtl::STLSortAndRemoveDuplicates(&term.literals);
CHECK_GT(term.literals.size(), 1);
}
constraints_.push_back(std::move(constraint));
}
std::string ValidateModel() {
// Normalize and validate constraints.
for (const PbConstraint& constraint : constraints_) {
if (constraint.rhs == std::numeric_limits<int64_t>::min()) {
return "constraint error: undefined rhs";
}
if (constraint.type == UNDEFINED_OPERATION) {
return "constraint error: undefined operation";
}
for (const PbTerm& term : constraint.terms) {
if (term.coeff == 0) {
return "constraint error: coefficient cannot be zero";
}
if (term.literals.empty()) return "constraint error: empty literals";
if (term.literals.size() == 1) {
if (!RefIsPositive(term.literals[0])) {
return "constraint error: linear terms must use positive literals";
}
}
}
}
if (constraint->literals_size() != constraint->coefficients_size()) {
LOG(FATAL) << "Failed to parse constraint:\n " << line;
// Normalize and validate objective.
if (objective_.empty()) return ""; // No objective.
for (const PbTerm& term : objective_) {
if (term.coeff == 0) return "objective error: coefficient cannot be zero";
if (term.literals.empty()) return "objective error: empty literals";
if (term.literals.size() == 1) {
if (!RefIsPositive(term.literals[0])) {
return "objective error: linear terms must use positive literals";
}
return "";
}
}
return "";
}
static int PbLiteralToCpModelLiteral(int pb_literal) {
return pb_literal > 0 ? pb_literal - 1 : -pb_literal;
}
int GetVariable(const PbTerm& term, CpModelProto* model) {
CHECK(!term.literals.empty());
if (term.literals.size() == 1) {
CHECK(RefIsPositive(term.literals[0]));
return term.literals[0];
}
const auto it = product_to_var_.find(term.literals);
if (it != product_to_var_.end()) {
return it->second;
}
const int var_index = model->variables_size();
IntegerVariableProto* var_proto = model->add_variables();
var_proto->add_domain(0);
var_proto->add_domain(1);
product_to_var_[term.literals] = var_index;
// Link the new variable to the terms.
// var_index => and(literals).
ConstraintProto* var_to_literals = model->add_constraints();
var_to_literals->add_enforcement_literal(var_index);
// and(literals) => var_index.
ConstraintProto* literals_to_var = model->add_constraints();
literals_to_var->mutable_bool_and()->add_literals(var_index);
for (const int proto_literal : term.literals) {
var_to_literals->mutable_bool_and()->add_literals(proto_literal);
literals_to_var->add_enforcement_literal(proto_literal);
}
return var_index;
}
void BuildModel(CpModelProto* model) {
// We know how many variables we have, so we can add them all.
for (int i = 0; i < num_variables_; ++i) {
IntegerVariableProto* var = model->add_variables();
var->add_domain(0);
var->add_domain(1);
}
for (const PbConstraint& constraint : constraints_) {
ConstraintProto* ct = model->add_constraints();
LinearConstraintProto* lin = ct->mutable_linear();
for (const PbTerm& term : constraint.terms) {
lin->add_vars(GetVariable(term, model));
lin->add_coeffs(term.coeff);
}
if (constraint.type == GE_OPERATION) {
lin->add_domain(constraint.rhs);
lin->add_domain(std::numeric_limits<int64_t>::max());
} else if (constraint.type == EQ_OPERATION) {
lin->add_domain(constraint.rhs);
lin->add_domain(constraint.rhs);
} else {
LOG(FATAL) << "Unsupported operation: " << constraint.type;
}
if (constraint.soft_cost != std::numeric_limits<int64_t>::max()) {
const int violation_var_index = model->variables_size();
IntegerVariableProto* violation_var = model->add_variables();
violation_var->add_domain(0);
violation_var->add_domain(1);
// Update the objective.
model->mutable_objective()->add_vars(violation_var_index);
model->mutable_objective()->add_coeffs(constraint.soft_cost);
// Add the enforcement literal to ct.
ct->add_enforcement_literal(NegatedRef(violation_var_index));
}
}
if (!objective_.empty()) {
CpObjectiveProto* obj = model->mutable_objective();
for (const PbTerm& term : objective_) {
obj->add_vars(GetVariable(term, model));
obj->add_coeffs(term.coeff);
}
}
}
int num_variables_;
std::vector<PbTerm> objective_;
std::vector<PbConstraint> constraints_;
absl::flat_hash_map<absl::Span<const int>, int> product_to_var_;
};
} // namespace sat

10
ortools/sat/sat_inprocessing.cc
View File

@@ -163,7 +163,7 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) {
logger_, "[Pure SAT presolve]", " num_fixed: ", trail_->Index(),
" num_redundant: ", implication_graph_->num_redundant_literals() / 2, "/",
sat_solver_->NumVariables(),
" num_implications: ", implication_graph_->num_implications(),
" num_implications: ", implication_graph_->ComputeNumImplicationsForLog(),
" num_watched_clauses: ", clause_manager_->num_watched_clauses(),
" dtime: ", time_limit_->GetElapsedDeterministicTime() - start_dtime, "/",
options.deterministic_time_limit, " wtime: ", wall_timer.Get(),
@@ -280,7 +280,7 @@ bool Inprocessing::InprocessingRound() {
logger_, "Inprocessing.", " fixed:", trail_->Index(),
" equiv:", implication_graph_->num_redundant_literals() / 2,
" bools:", sat_solver_->NumVariables(),
" implications:", implication_graph_->num_implications(),
" implications:", implication_graph_->ComputeNumImplicationsForLog(),
" watched:", clause_manager_->num_watched_clauses(),
" minimization:", mini_num_clause, "|", mini_num_removed,
" dtime:", time_limit_->GetElapsedDeterministicTime() - start_dtime,
@@ -664,8 +664,7 @@ bool StampingSimplifier::DoOneRound(bool log_info) {
num_removed_literals_ = 0;
num_fixed_ = 0;
if (implication_graph_->literal_size() == 0) return true;
if (implication_graph_->num_implications() == 0) return true;
if (implication_graph_->IsEmpty()) return true;
if (!stamps_are_already_computed_) {
// We need a DAG so that we don't have cycle while we sample the tree.
@@ -696,8 +695,7 @@ bool StampingSimplifier::ComputeStampsForNextRound(bool log_info) {
dtime_ = 0.0;
num_fixed_ = 0;
if (implication_graph_->literal_size() == 0) return true;
if (implication_graph_->num_implications() == 0) return true;
if (implication_graph_->IsEmpty()) return true;
implication_graph_->RemoveFixedVariables();
if (!implication_graph_->DetectEquivalences(log_info)) return true;

4
ortools/sat/sat_inprocessing_test.cc
View File

@@ -133,7 +133,7 @@ TEST(InprocessingTest, ClauseSubsumptionAndStrengthening) {
// We added {+1, +2} and {+1, -3} there.
// TODO(user): make sure we don't add twice the implications.
auto* implication_graph = model.GetOrCreate<BinaryImplicationGraph>();
EXPECT_EQ(implication_graph->num_implications(), 6);
EXPECT_EQ(implication_graph->ComputeNumImplicationsForLog(), 6);
EXPECT_EQ(implication_graph->Implications(Literal(-1)).size(), 3);
EXPECT_THAT(implication_graph->Implications(Literal(-1)),
::testing::UnorderedElementsAre(Literal(+2), Literal(+2),
@@ -146,7 +146,7 @@ TEST(InprocessingTest, ClauseSubsumptionAndStrengthening) {
// Depending on the implication added, we don't get the same clauses.
auto* implication_graph = model.GetOrCreate<BinaryImplicationGraph>();
EXPECT_EQ(implication_graph->num_implications(), 2);
EXPECT_EQ(implication_graph->ComputeNumImplicationsForLog(), 2);
EXPECT_EQ(implication_graph->Implications(Literal(-1)).size(), 1);
if (implication_graph->Implications(Literal(-1))[0] == Literal(+2)) {
EXPECT_EQ(all_clauses[2]->AsSpan(), Literals({+2, +6, +1, +1}));

9
ortools/sat/sat_runner.cc
View File

@@ -29,8 +29,6 @@
#include "ortools/base/helpers.h"
#include "ortools/base/options.h"
#include "ortools/base/path.h"
#include "ortools/sat/boolean_problem.h"
#include "ortools/sat/boolean_problem.pb.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
@@ -95,13 +93,12 @@ std::string ExtractName(absl::string_view full_filename) {
bool LoadProblem(const std::string& filename, absl::string_view hint_file,
absl::string_view domain_file, CpModelProto* cp_model) {
if (absl::EndsWith(filename, ".opb") ||
absl::EndsWith(filename, ".opb.bz2")) {
absl::EndsWith(filename, ".opb.bz2") ||
absl::EndsWith(filename, ".opb.gz")) {
OpbReader reader;
LinearBooleanProblem problem;
if (!reader.Load(filename, &problem)) {
if (!reader.LoadAndValidate(filename, cp_model)) {
LOG(FATAL) << "Cannot load file '" << filename << "'.";
}
*cp_model = BooleanProblemToCpModelproto(problem);
} else if (absl::EndsWith(filename, ".cnf") ||
absl::EndsWith(filename, ".cnf.xz") ||
absl::EndsWith(filename, ".cnf.gz") ||

5
ortools/sat/sat_solver.cc
View File

@@ -1408,7 +1408,7 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit,
SOLVER_LOG(logger_, "Number of clauses (size > 2): ",
clauses_propagator_->num_clauses());
SOLVER_LOG(logger_, "Number of binary clauses: ",
binary_implication_graph_->num_implications());
binary_implication_graph_->ComputeNumImplicationsForLog());
SOLVER_LOG(logger_, "Number of linear constraints: ",
pb_constraints_->NumberOfConstraints());
SOLVER_LOG(logger_, "Number of fixed variables: ", trail_->Index());
@@ -1812,7 +1812,8 @@ std::string SatSolver::RunningStatisticsString() const {
clauses_propagator_->num_clauses() -
clauses_propagator_->num_removable_clauses(),
clauses_propagator_->num_removable_clauses(),
binary_implication_graph_->num_implications(), restart_->NumRestarts(),
binary_implication_graph_->ComputeNumImplicationsForLog(),
restart_->NumRestarts(),
num_variables_.value() - num_processed_fixed_variables_);
}

18
ortools/sat/scheduling_helpers.cc
View File

@@ -246,7 +246,9 @@ void SchedulingConstraintHelper::InitSortedVectors() {
recompute_all_cache_ = true;
recompute_cache_.Resize(num_tasks);
non_fixed_intervals_.resize(num_tasks);
for (int t = 0; t < num_tasks; ++t) {
non_fixed_intervals_[t] = t;
recompute_cache_.Set(t);
}
@@ -313,9 +315,23 @@ bool SchedulingConstraintHelper::SynchronizeAndSetTimeDirection(
}
if (recompute_all_cache_) {
for (int t = 0; t < recompute_cache_.size(); ++t) {
for (const int t : non_fixed_intervals_) {
if (!UpdateCachedValues(t)) return false;
}
// We also update non_fixed_intervals_ at level zero so that we will never
// scan them again.
if (sat_solver_->CurrentDecisionLevel() == 0) {
int new_size = 0;
for (const int t : non_fixed_intervals_) {
if (IsPresent(t) && StartIsFixed(t) && EndIsFixed(t) &&
SizeIsFixed(t)) {
continue;
}
non_fixed_intervals_[new_size++] = t;
}
non_fixed_intervals_.resize(new_size);
}
} else {
for (const int t : recompute_cache_) {
if (!UpdateCachedValues(t)) return false;

5
ortools/sat/scheduling_helpers.h
View File

@@ -457,6 +457,11 @@ class SchedulingConstraintHelper : public PropagatorInterface {
bool recompute_all_cache_ = true;
Bitset64<int> recompute_cache_;
// For large problems, LNS will have a lot of fixed intervals.
// And fixed intervals will never changes, so there is no point recomputing
// the cache for them.
std::vector<int> non_fixed_intervals_;
// Reason vectors.
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;