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

rename internal sat method; more tests

Browse Source
This commit is contained in:
Laurent Perron
2025-04-03 16:12:45 +02:00
parent 61ddd9e109
commit 45cb968568
23 changed files with 16294 additions and 90 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/bop/bop_fs.cc
View File

@@ -345,7 +345,7 @@ BopOptimizerBase::Status BopRandomFirstSolutionGenerator::Optimize(
}
// This can be proved during the call to RestoreSolverToAssumptionLevel().
if (sat_propagator_->IsModelUnsat()) {
if (sat_propagator_->ModelIsUnsat()) {
// The solution is proved optimal (if any).
learned_info->lower_bound = best_cost;
return best_cost == std::numeric_limits<int64_t>::max()

18
ortools/bop/bop_lns.cc
View File

@@ -110,7 +110,7 @@ BopOptimizerBase::Status BopCompleteLNSOptimizer::SynchronizeIfNeeded(
/*use_lower_bound=*/false, sat::Coefficient(0),
/*use_upper_bound=*/true, sat::Coefficient(num_relaxed_vars), &cst);
if (sat_solver_->IsModelUnsat()) return BopOptimizerBase::ABORT;
if (sat_solver_->ModelIsUnsat()) return BopOptimizerBase::ABORT;
// It sounds like a good idea to force the solver to find a similar solution
// from the current one. On another side, this is already somewhat enforced by
@@ -255,7 +255,7 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
const double initial_dt = sat_propagator_->deterministic_time();
auto sat_propagator_cleanup =
::absl::MakeCleanup([initial_dt, this, &learned_info, &time_limit]() {
if (!sat_propagator_->IsModelUnsat()) {
if (!sat_propagator_->ModelIsUnsat()) {
sat_propagator_->SetAssumptionLevel(0);
sat_propagator_->RestoreSolverToAssumptionLevel();
ExtractLearnedInfoFromSatSolver(sat_propagator_, learned_info);
@@ -289,7 +289,7 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
<< problem_state.original_problem().num_variables();
// Special case if the difficulty is too high.
if (!sat_propagator_->IsModelUnsat()) {
if (!sat_propagator_->ModelIsUnsat()) {
if (sat_propagator_->CurrentDecisionLevel() == 0) {
VLOG(2) << "Nothing fixed!";
adaptive_difficulty_.DecreaseParameter();
@@ -300,7 +300,7 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
// Since everything is already set-up, we try the sat_propagator_ with
// a really low conflict limit. This allow to quickly skip over UNSAT
// cases without the costly new problem setup.
if (!sat_propagator_->IsModelUnsat()) {
if (!sat_propagator_->ModelIsUnsat()) {
sat::SatParameters params;
params.set_max_number_of_conflicts(
local_parameters.max_number_of_conflicts_for_quick_check());
@@ -329,13 +329,13 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
// propagator_ will be used to construct the local problem below.
// Note that calling RestoreSolverToAssumptionLevel() might actually prove
// the infeasibility. It is important to check the UNSAT status afterward.
if (!sat_propagator_->IsModelUnsat()) {
if (!sat_propagator_->ModelIsUnsat()) {
sat_propagator_->RestoreSolverToAssumptionLevel();
}
// Check if the problem is proved UNSAT, by previous the search or the
// RestoreSolverToAssumptionLevel() call above.
if (sat_propagator_->IsModelUnsat()) {
if (sat_propagator_->ModelIsUnsat()) {
return problem_state.solution().IsFeasible()
? BopOptimizerBase::OPTIMAL_SOLUTION_FOUND
: BopOptimizerBase::INFEASIBLE;
@@ -466,7 +466,7 @@ void ObjectiveBasedNeighborhood::GenerateNeighborhood(
break;
}
sat_propagator->EnqueueDecisionAndBacktrackOnConflict(literal);
if (sat_propagator->IsModelUnsat()) return;
if (sat_propagator->ModelIsUnsat()) return;
}
}
@@ -515,7 +515,7 @@ void ConstraintBasedNeighborhood::GenerateNeighborhood(
for (const sat::Literal literal : to_fix) {
if (variable_is_relaxed[literal.Variable().value()]) continue;
sat_propagator->EnqueueDecisionAndBacktrackOnConflict(literal);
if (sat_propagator->IsModelUnsat()) return;
if (sat_propagator->ModelIsUnsat()) return;
}
}
@@ -595,7 +595,7 @@ void RelationGraphBasedNeighborhood::GenerateNeighborhood(
}
}
}
if (sat_propagator->IsModelUnsat()) return;
if (sat_propagator->ModelIsUnsat()) return;
}
VLOG(2) << "target:" << target << " relaxed:" << num_relaxed << " actual:"
<< num_variables - sat_propagator->LiteralTrail().Index();

2
ortools/bop/bop_ls.cc
View File

@@ -665,7 +665,7 @@ int SatWrapper::ApplyDecision(sat::Literal decision_literal,
const int old_decision_level = sat_solver_->CurrentDecisionLevel();
const int new_trail_index =
sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision_literal);
if (sat_solver_->IsModelUnsat()) {
if (sat_solver_->ModelIsUnsat()) {
return old_decision_level + 1;
}

2
ortools/bop/bop_ls.h
View File

@@ -75,7 +75,7 @@ class SatWrapper {
// the SAT solver is not able to prove it; After some decisions / learned
// conflicts, the SAT solver might be able to prove UNSAT and so this will
// return true.
bool IsModelUnsat() const { return sat_solver_->IsModelUnsat(); }
bool IsModelUnsat() const { return sat_solver_->ModelIsUnsat(); }
// Return the current solver VariablesAssignment.
const sat::VariablesAssignment& SatAssignment() const {

2
ortools/bop/bop_util.cc
View File

@@ -112,7 +112,7 @@ void ExtractLearnedInfoFromSatSolver(sat::SatSolver* solver,
CHECK(nullptr != info);
// This should never be called if the problem is UNSAT.
CHECK(!solver->IsModelUnsat());
CHECK(!solver->ModelIsUnsat());
// Fixed variables.
info->fixed_literals.clear();

27
ortools/graph/BUILD.bazel
View File

@@ -44,6 +44,22 @@ cc_library(
],
)
cc_test(
name = "graph_test",
size = "small",
srcs = ["graph_test.cc"],
deps = [
":graph",
"//ortools/base:gmock_main",
"//ortools/base:intops",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/random",
"@abseil-cpp//absl/strings",
"@abseil-cpp//absl/types:span",
"@com_google_benchmark//:benchmark",
],
)
cc_library(
name = "flow_graph",
hdrs = ["flow_graph.h"],
@@ -835,6 +851,17 @@ cc_library(
hdrs = ["iterators.h"],
)
cc_test(
name = "iterators_test",
size = "small",
srcs = ["iterators_test.cc"],
deps = [
":iterators",
"//ortools/base:gmock_main",
"//ortools/base:int_type",
],
)
cc_library(
name = "random_graph",
srcs = ["random_graph.cc"],

1319
ortools/graph/graph_test.cc Normal file
View File

File diff suppressed because it is too large Load Diff

175
ortools/graph/iterators_test.cc Normal file
View File

@@ -0,0 +1,175 @@
// Copyright 2010-2025 Google LLC
// 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 "ortools/graph/iterators.h"
#include <cstdint>
#include <iterator>
#include <vector>
#include "gtest/gtest.h"
#include "ortools/base/int_type.h"
namespace util {
namespace {
DEFINE_INT_TYPE(TestIndex, int64_t);
#if __cplusplus >= 202002L
static_assert(std::random_access_iterator<IntegerRangeIterator<int>>);
static_assert(std::random_access_iterator<IntegerRangeIterator<TestIndex>>);
#endif // __cplusplus >= 202002L
TEST(IntegerRangeTest, VariousEmptyRanges) {
bool went_inside = false;
for ([[maybe_unused]] const int i : IntegerRange<int>(0, 0)) {
went_inside = true;
}
for ([[maybe_unused]] const int i : IntegerRange<int>(10, 10)) {
went_inside = true;
}
for ([[maybe_unused]] const int i : IntegerRange<int>(-10, -10)) {
went_inside = true;
}
EXPECT_FALSE(went_inside);
}
TEST(IntegerRangeTest, NormalBehavior) {
int reference_index = 0;
for (const int i : IntegerRange<int>(0, 100)) {
EXPECT_EQ(i, reference_index);
++reference_index;
}
EXPECT_EQ(reference_index, 100);
}
TEST(IntegerRangeTest, NormalBehaviorWithIntType) {
TestIndex reference_index(0);
for (const TestIndex i :
IntegerRange<TestIndex>(TestIndex(0), TestIndex(100))) {
EXPECT_EQ(i, reference_index);
++reference_index;
}
EXPECT_EQ(reference_index, TestIndex(100));
}
TEST(IntegerRangeTest, AssignToVector) {
static const int kRangeSize = 100;
IntegerRange<int> range(0, kRangeSize);
ASSERT_EQ(kRangeSize, range.size());
std::vector<int> vector_from_range(range.begin(), range.end());
ASSERT_EQ(kRangeSize, vector_from_range.size());
for (int i = 0; i < kRangeSize; ++i) {
EXPECT_EQ(i, vector_from_range[i]);
}
}
TEST(ChasingIteratorTest, ChasingIterator) {
static constexpr int kSentinel = 42;
struct Tag {};
using Iterator = ChasingIterator<int, kSentinel, Tag>;
const auto end = Iterator{};
#if __cplusplus >= 202002L
static_assert(std::forward_iterator<Iterator>);
#endif
// There are two chains: 0->1->3 and 4->2.
const int next[] = {1, 3, kSentinel, kSentinel, 2};
{
Iterator it(0, next);
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 0);
++it;
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 1);
++it;
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 3);
++it;
ASSERT_TRUE(it == end);
}
{
Iterator it(1, next);
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 1);
++it;
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 3);
++it;
ASSERT_TRUE(it == end);
}
{
Iterator it(2, next);
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 2);
++it;
ASSERT_TRUE(it == end);
}
{
Iterator it(3, next);
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 3);
++it;
ASSERT_TRUE(it == end);
}
{
Iterator it(4, next);
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 4);
++it;
ASSERT_FALSE(it == end);
EXPECT_EQ(*it, 2);
++it;
ASSERT_TRUE(it == end);
}
}
TEST(IntegerRangeTest, AssignToVectorOfIntType) {
static const int kRangeSize = 100;
IntegerRange<TestIndex> range(TestIndex(0), TestIndex(kRangeSize));
std::vector<TestIndex> vector_from_range(range.begin(), range.end());
ASSERT_EQ(kRangeSize, vector_from_range.size());
for (int i = 0; i < kRangeSize; ++i) {
EXPECT_EQ(TestIndex(i), vector_from_range[i]);
}
}
TEST(ReverseTest, EmptyVector) {
std::vector<int> test_vector;
bool went_inside = false;
for ([[maybe_unused]] const int value : Reverse(test_vector)) {
went_inside = true;
}
EXPECT_FALSE(went_inside);
}
TEST(ReverseTest, ReverseOfAVector) {
const int kSize = 10000;
std::vector<int> test_vector;
for (int i = 0; i < kSize; ++i) {
test_vector.push_back(5 * i + 5);
}
int index = 0;
for (int value : Reverse(test_vector)) {
EXPECT_EQ(test_vector[kSize - 1 - index], value);
index++;
}
// Same with references.
index = 0;
for (const int& value : Reverse(test_vector)) {
EXPECT_EQ(test_vector[kSize - 1 - index], value);
index++;
}
}
} // namespace
} // namespace util

10
ortools/graph/k_shortest_paths.h
View File

@@ -25,6 +25,16 @@
// Loopless path: path not going through the same node more than once. Also
// called simple path.
//
// The implementations do not support multigraphs, i.e. graphs with several
// arcs between the same source and destination nodes. One way to work around
// this limitation is to create dummy nodes between the source and destination
// nodes, with one of the edges carrying the weight and the other having a zero
// weight. This transformation slightly increases the size of the graph.
// If you have n edges between the nodes s and t, with the weights w_i, do the
// following: create n - 1 nodes (d_i for i from 2 to n), create n - 1 edges
// between s and d_i with weight w_i, create n - 1 edges between d_i and t with
// weight 0.
//
//
// Design choices
// ==============

36
ortools/graph/k_shortest_paths_test.cc
View File

@@ -205,7 +205,7 @@ TEST(KShortestPathsYenTest, ReturnsTheRightNumberOfPaths) {
// This test verifies that the algorithm returns the shortest path from the
// candidate paths produced at each spur.
TEST(DISABLED_KShortestPathsYenTest, ShortestPathSelectedFromCandidates) {
TEST(KShortestPathsYenTest, ShortestPathSelectedFromCandidates) {
// Topology:
//
// 0 ---- 3 ---- 6 Arcs length
@@ -247,20 +247,30 @@ TEST(DISABLED_KShortestPathsYenTest, ShortestPathSelectedFromCandidates) {
const KShortestPaths<StaticGraph<>> paths =
YenKShortestPaths(graph, lengths, /*source=*/0,
/*destination=*/6, /*k=*/10);
/*destination=*/6, /*k=*/14);
EXPECT_THAT(paths.paths, ElementsAre(std::vector<int>{0, 2, 6}, //
std::vector<int>{0, 3, 6},
std::vector<int>{0, 2, 1, 3, 6},
std::vector<int>{0, 3, 1, 2, 6},
std::vector<int>{0, 2, 7, 3, 6},
std::vector<int>{0, 3, 7, 2, 6},
std::vector<int>{0, 2, 7, 5, 1, 3, 6},
std::vector<int>{0, 3, 7, 5, 1, 2, 6},
std::vector<int>{0, 2, 4, 5, 1, 3, 6},
std::vector<int>{0, 3, 7, 5, 4, 2, 6}));
EXPECT_THAT(paths.distances,
ElementsAre(200, 200, 400, 400, 400, 400, 600, 600, 600, 600));
ElementsAre(200, 200, //
400, 400, 400, 400, //
600, 600, 600, 600, 600, 600, 600, 600));
EXPECT_THAT(
paths.paths,
testing::UnorderedElementsAre(
// 200
std::vector<int>{0, 2, 6}, std::vector<int>{0, 3, 6},
// 400
std::vector<int>{0, 2, 1, 3, 6}, std::vector<int>{0, 3, 1, 2, 6},
std::vector<int>{0, 2, 7, 3, 6}, std::vector<int>{0, 3, 7, 2, 6},
// 600
std::vector<int>{0, 2, 7, 5, 1, 3, 6},
std::vector<int>{0, 3, 7, 5, 1, 2, 6},
std::vector<int>{0, 2, 4, 5, 1, 3, 6},
std::vector<int>{0, 3, 7, 5, 4, 2, 6},
std::vector<int>{0, 2, 4, 5, 7, 3, 6},
std::vector<int>{0, 2, 8, 5, 1, 3, 6},
std::vector<int>{0, 3, 7, 5, 8, 2, 6},
std::vector<int>{0, 2, 8, 5, 7, 3, 6}));
}
namespace internal {

518
ortools/sat/2d_orthogonal_packing_test.cc Normal file
View File

@@ -0,0 +1,518 @@
// Copyright 2010-2025 Google LLC
// 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 "ortools/sat/2d_orthogonal_packing.h"
#include <algorithm>
#include <cstdint>
#include <limits>
#include <utility>
#include <vector>
#include "absl/log/check.h"
#include "absl/random/bit_gen_ref.h"
#include "absl/random/distributions.h"
#include "absl/random/random.h"
#include "absl/strings/str_cat.h"
#include "absl/strings/str_join.h"
#include "absl/types/span.h"
#include "benchmark/benchmark.h"
#include "gtest/gtest.h"
#include "ortools/algorithms/binary_search.h"
#include "ortools/base/gmock.h"
#include "ortools/sat/2d_orthogonal_packing_testing.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/integer_base.h"
#include "ortools/sat/synchronization.h"
namespace operations_research {
namespace sat {
namespace {
// Alternative way of computing Dff.LowestInverse().
template <typename DffClass>
IntegerValue ComputeDffInverse(const DffClass& dff, IntegerValue max,
IntegerValue value) {
DCHECK_EQ(dff(0), 0);
if (value <= 0) return 0;
return BinarySearch<IntegerValue>(
max, 0, [&dff, value](IntegerValue x) { return dff(x) >= value; });
}
template <typename DffClass, typename... Args>
void TestMaximalDff(absl::BitGenRef random, int64_t num_values_to_check,
int64_t max, Args&&... args) {
DffClass dff(max, std::forward<Args>(args)...);
num_values_to_check = std::min(num_values_to_check, max);
const int64_t step_size = max / num_values_to_check;
for (int64_t i = 0; i < max; i += step_size) {
int64_t value_to_check;
if (step_size > 1) {
value_to_check =
absl::Uniform(random, i, std::min(i + step_size - 1, max));
} else {
value_to_check = i;
}
for (int64_t j = 0; j < max; j += step_size) {
int64_t value_to_check2;
if (step_size > 1) {
value_to_check2 =
absl::Uniform(random, j, std::min(j + step_size - 1, max));
} else {
value_to_check2 = j;
}
const IntegerValue f = dff(value_to_check);
const IntegerValue f2 = dff(value_to_check2);
// f is nondecreasing
if (f != f2) {
CHECK_EQ(f < f2, value_to_check < value_to_check2);
}
// f is superadditive, i.e., f(x) + f(y) <= f(x + y)
if (value_to_check + value_to_check2 <= max) {
CHECK_LE(f + f2, dff(value_to_check + value_to_check2));
}
// f is symmetric, i.e., f(x) + f(C - x) = f(C)
CHECK_EQ(dff(value_to_check) + dff(max - value_to_check), dff(max));
CHECK_EQ(dff(value_to_check2) + dff(max - value_to_check2), dff(max));
// Inverse works
CHECK_EQ(dff(dff.LowestInverse(f)), f);
// Lowest inverse is indeed the lowest
CHECK_LE(dff.LowestInverse(f), value_to_check);
if (dff.LowestInverse(f) > 0) {
CHECK_NE(dff(dff.LowestInverse(f) - 1), f);
}
// Inverse works outside domain
if (value_to_check <= dff(max)) {
CHECK_GE(dff(dff.LowestInverse(value_to_check)), value_to_check);
if (dff.LowestInverse(value_to_check) > 0) {
CHECK_LT(dff(dff.LowestInverse(value_to_check) - 1), value_to_check);
}
CHECK_EQ(dff.LowestInverse(value_to_check),
ComputeDffInverse(dff, max, value_to_check));
}
}
}
// f(0) = 0
CHECK_EQ(dff(0), 0);
}
TEST(DualFeasibilityFunctionTest, Dff2IsMaximal) {
absl::BitGen random;
for (int k = 1; k < 50; k++) {
TestMaximalDff<RoundingDualFeasibleFunction>(
random, 100, 100 + absl::Uniform(random, 0, 1), k);
}
for (int k = 100; 2 * k <= std::numeric_limits<uint16_t>::max(); k += 200) {
TestMaximalDff<RoundingDualFeasibleFunction>(random, 200, 2 * k, k);
}
}
TEST(DualFeasibilityFunctionTest, DffPowerOfTwo) {
absl::BitGen random;
for (int k = 0; k < 61; k++) {
TestMaximalDff<RoundingDualFeasibleFunctionPowerOfTwo>(
random, 100, std::numeric_limits<int64_t>::max() / 2, k);
}
}
TEST(DualFeasibilityFunctionTest, Dff0IsMaximal) {
absl::BitGen random;
for (int k = 1; k < 50; k++) {
TestMaximalDff<DualFeasibleFunctionF0>(random, 100, 100, k);
}
for (int k = 100; 2 * k <= std::numeric_limits<uint16_t>::max(); k += 200) {
TestMaximalDff<DualFeasibleFunctionF0>(random, 200, 2 * k, k);
}
}
TEST(DualFeasibilityFunctionTest, Composed) {
absl::BitGen random;
for (int k_f0 = 1; k_f0 < 50; k_f0++) {
for (int k_f2 = 2; k_f2 < 50; k_f2++) {
TestMaximalDff<DFFComposedF2F0>(random, 100, 100, k_f0, k_f2);
}
}
}
using DetectorStatus = OrthogonalPackingResult::Status;
struct OppProblem {
std::vector<IntegerValue> items_x_sizes;
std::vector<IntegerValue> items_y_sizes;
std::pair<IntegerValue, IntegerValue> bb_sizes;
template <typename Sink>
friend void AbslStringify(Sink& sink, const OppProblem& p) {
absl::Format(&sink,
"items_x_sizes={%s}, items_y_sizes={%s}, bb_sizes={%i, %i}",
absl::StrJoin(p.items_x_sizes, ", "),
absl::StrJoin(p.items_y_sizes, ", "), p.bb_sizes.first.value(),
p.bb_sizes.second.value());
}
};
OppProblem CreateFeasibleOppProblem(absl::BitGenRef random, int max_size) {
std::vector<RectangleInRange> problem = MakeItemsFromRectangles(
GenerateNonConflictingRectangles(
absl::Uniform(random, max_size - 1, max_size), random),
0, random);
OppProblem result;
Rectangle bounding_box;
bounding_box = {.x_min = std::numeric_limits<IntegerValue>::max(),
.x_max = std::numeric_limits<IntegerValue>::min(),
.y_min = std::numeric_limits<IntegerValue>::max(),
.y_max = std::numeric_limits<IntegerValue>::min()};
std::vector<IntegerValue>& items_x_sizes = result.items_x_sizes;
std::vector<IntegerValue>& items_y_sizes = result.items_y_sizes;
for (const auto& item : problem) {
items_x_sizes.push_back(item.x_size);
items_y_sizes.push_back(item.y_size);
bounding_box.x_min = std::min(bounding_box.x_min, item.bounding_area.x_min);
bounding_box.x_max = std::max(bounding_box.x_max, item.bounding_area.x_max);
bounding_box.y_min = std::min(bounding_box.y_min, item.bounding_area.y_min);
bounding_box.y_max = std::max(bounding_box.y_max, item.bounding_area.y_max);
}
result.bb_sizes = {bounding_box.SizeX(), bounding_box.SizeY()};
return result;
}
OppProblem CreateRandomOppProblem(absl::BitGenRef random, int size) {
OppProblem result;
std::vector<IntegerValue>& items_x_sizes = result.items_x_sizes;
std::vector<IntegerValue>& items_y_sizes = result.items_y_sizes;
const int num_items = absl::Uniform(random, 1, 20);
items_x_sizes.clear();
items_y_sizes.clear();
IntegerValue area = 0;
for (int i = 0; i < num_items; ++i) {
const IntegerValue x_size = absl::Uniform(random, 1, size);
const IntegerValue y_size = absl::Uniform(random, 1, size);
items_x_sizes.push_back(x_size);
items_y_sizes.push_back(y_size);
area += x_size * y_size;
}
const IntegerValue box_x_size = absl::Uniform(random, size, 4 * size);
const IntegerValue box_y_size =
std::max(IntegerValue(size), (area + box_x_size - 1) / box_x_size);
result.bb_sizes = {box_x_size, box_y_size};
return result;
}
TEST(DualFeasibilityTest, NoConflictWhenItDoesNotExist) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
constexpr int num_runs = 400;
for (int k = 0; k < num_runs; k++) {
auto problem = CreateFeasibleOppProblem(random, 30);
CHECK(opp_solver
.TestFeasibility(problem.items_x_sizes, problem.items_y_sizes,
problem.bb_sizes)
.GetResult() != DetectorStatus::INFEASIBLE)
<< "problem: " << absl::StrCat(problem);
}
}
DetectorStatus NaiveCheckPairwiseFeasibility(
absl::Span<const IntegerValue> sizes_x,
absl::Span<const IntegerValue> sizes_y,
const std::pair<IntegerValue, IntegerValue>& bounding_box_size) {
for (int i = 0; i < sizes_x.size(); i++) {
for (int j = i + 1; j < sizes_x.size(); j++) {
if (sizes_x[i] + sizes_x[j] > bounding_box_size.first &&
sizes_y[i] + sizes_y[j] > bounding_box_size.second) {
return DetectorStatus::INFEASIBLE;
}
}
}
return DetectorStatus::UNKNOWN;
}
DetectorStatus NaiveCheckFeasibilityWithDualFunction(
absl::Span<const IntegerValue> sizes_x,
absl::Span<const IntegerValue> sizes_y,
const std::pair<IntegerValue, IntegerValue>& bounding_box_size) {
const IntegerValue bb_area =
bounding_box_size.first * bounding_box_size.second;
for (IntegerValue k = 0; 2 * k <= bounding_box_size.first; k++) {
DualFeasibleFunctionF0 dff0_x(bounding_box_size.first, k);
for (IntegerValue l = 0; 2 * l <= bounding_box_size.second; l++) {
DualFeasibleFunctionF0 dff0_y(bounding_box_size.second, l);
IntegerValue area = 0;
for (int i = 0; i < sizes_x.size(); i++) {
area += dff0_x(sizes_x[i]) * dff0_y(sizes_y[i]);
}
if (area > bb_area) {
return DetectorStatus::INFEASIBLE;
}
}
}
return DetectorStatus::UNKNOWN;
}
TEST(DualFeasibilityTest, Random) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
constexpr int num_runs = 400;
constexpr int size = 20;
for (int k = 0; k < num_runs; k++) {
const OppProblem problem = CreateRandomOppProblem(random, size);
const auto naive_result = NaiveCheckFeasibilityWithDualFunction(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes);
const auto naive_pairwise = NaiveCheckPairwiseFeasibility(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes);
const auto result = opp_solver.TestFeasibility(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes,
OrthogonalPackingOptions{.use_pairwise = true,
.use_dff_f0 = true,
.use_dff_f2 = false,
.brute_force_threshold = 0});
CHECK_EQ(result.GetResult() == DetectorStatus::INFEASIBLE,
naive_result == DetectorStatus::INFEASIBLE ||
naive_pairwise == DetectorStatus::INFEASIBLE);
CHECK_EQ(result.GetItemsParticipatingOnConflict().size() == 2,
naive_pairwise == DetectorStatus::INFEASIBLE);
}
}
// Try f_2^k(f_0^l(x)) for all values of k and l.
DetectorStatus NaiveFeasibilityWithDualFunction2(
absl::Span<const IntegerValue> sizes_x,
absl::Span<const IntegerValue> sizes_y,
std::pair<IntegerValue, IntegerValue> bounding_box_size) {
for (IntegerValue l = 0; 2 * l <= bounding_box_size.first; l++) {
DualFeasibleFunctionF0 dff0(bounding_box_size.first, l);
for (IntegerValue k = 1; 2 * k < bounding_box_size.first; k++) {
const RoundingDualFeasibleFunction dff2(bounding_box_size.first, k);
const IntegerValue c_k = bounding_box_size.first / k;
const IntegerValue bb_area = 2 * c_k * bounding_box_size.second;
IntegerValue area = 0;
for (int i = 0; i < sizes_x.size(); i++) {
// First apply f_0
IntegerValue x_size = dff0(sizes_x[i]);
// Now apply f_2
if (2 * x_size > bounding_box_size.first) {
x_size = 2 * (c_k - (bounding_box_size.first - x_size) / k);
} else if (2 * x_size == bounding_box_size.first) {
x_size = c_k;
} else {
x_size = 2 * (x_size / k);
}
CHECK_EQ(x_size, dff2(dff0(sizes_x[i])));
IntegerValue y_size = sizes_y[i];
area += x_size * y_size;
}
if (area > bb_area) {
return DetectorStatus::INFEASIBLE;
}
}
}
return DetectorStatus::UNKNOWN;
}
TEST(DualFeasibility2Test, Random) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
constexpr int num_runs = 40000;
const int size = absl::Uniform(random, 10, 30);
for (int k = 0; k < num_runs; k++) {
const OppProblem problem = CreateRandomOppProblem(random, size);
const DetectorStatus naive_result1 = NaiveFeasibilityWithDualFunction2(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes);
const DetectorStatus naive_result2 = NaiveFeasibilityWithDualFunction2(
problem.items_y_sizes, problem.items_x_sizes,
{problem.bb_sizes.second, problem.bb_sizes.first});
const auto result = opp_solver.TestFeasibility(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes,
OrthogonalPackingOptions{.use_pairwise = false,
.use_dff_f0 = true,
.use_dff_f2 = true,
.brute_force_threshold = 0});
CHECK_EQ(naive_result1 == DetectorStatus::INFEASIBLE ||
naive_result2 == DetectorStatus::INFEASIBLE,
result.GetResult() == DetectorStatus::INFEASIBLE)
<< " naive result x: " << (naive_result1 == DetectorStatus::INFEASIBLE)
<< " Naive result y: " << (naive_result2 == DetectorStatus::INFEASIBLE)
<< " Result: " << (result.GetResult() == DetectorStatus::INFEASIBLE)
<< " problem:" << absl::StrCat(problem);
}
}
TEST(OrthogonalPackingTest, SlackDoesNotChangeFeasibility) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
constexpr int num_runs = 400;
constexpr int size = 20;
for (int k = 0; k < num_runs; k++) {
OppProblem problem = CreateRandomOppProblem(random, size);
// Add one more item since `CreateRandomOppProblem()` does not generate
// trivially infeasible problems.
problem.items_x_sizes.push_back(absl::Uniform(random, 1, size));
problem.items_y_sizes.push_back(absl::Uniform(random, 1, size));
auto result = opp_solver.TestFeasibility(
problem.items_x_sizes, problem.items_y_sizes, problem.bb_sizes);
if (result.GetResult() != DetectorStatus::INFEASIBLE) {
continue;
}
const std::vector<OrthogonalPackingResult::Item>&
items_participating_on_conflict =
result.GetItemsParticipatingOnConflict();
for (int i = 0; i < items_participating_on_conflict.size(); ++i) {
if (absl::Bernoulli(random, 0.5)) {
result.TryUseSlackToReduceItemSize(
i, OrthogonalPackingResult::Coord::kCoordX, 0);
result.TryUseSlackToReduceItemSize(
i, OrthogonalPackingResult::Coord::kCoordY, 0);
} else {
result.TryUseSlackToReduceItemSize(
i, OrthogonalPackingResult::Coord::kCoordY, 0);
result.TryUseSlackToReduceItemSize(
i, OrthogonalPackingResult::Coord::kCoordX, 0);
}
}
OppProblem modified_problem;
modified_problem.bb_sizes = problem.bb_sizes;
for (const auto& item : result.GetItemsParticipatingOnConflict()) {
modified_problem.items_x_sizes.push_back(item.size_x);
modified_problem.items_y_sizes.push_back(item.size_y);
}
EXPECT_TRUE(opp_solver
.TestFeasibility(modified_problem.items_x_sizes,
modified_problem.items_y_sizes,
modified_problem.bb_sizes)
.GetResult() == DetectorStatus::INFEASIBLE)
<< "problem: " << absl::StrCat(problem);
}
}
void BM_OrthogonalPackingInfeasibilityDetector(benchmark::State& state) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
std::vector<OppProblem> problems;
for (int i = 0; i < 10; ++i) {
problems.push_back(CreateFeasibleOppProblem(random, state.range(0)));
}
int index = 0;
for (auto s : state) {
const auto& problem = problems[index];
CHECK(opp_solver
.TestFeasibility(problem.items_x_sizes, problem.items_y_sizes,
problem.bb_sizes)
.GetResult() != DetectorStatus::INFEASIBLE);
++index;
if (index == 10) {
index = 0;
}
}
}
BENCHMARK(BM_OrthogonalPackingInfeasibilityDetector)
->Arg(5)
->Arg(10)
->Arg(20)
->Arg(30)
->Arg(40)
->Arg(80)
->Arg(100)
->Arg(200)
->Arg(1000)
->Arg(10000);
MATCHER_P3(ItemIs, index, size_x, size_y, "") {
return arg.index == index && arg.size_x == size_x && arg.size_y == size_y;
}
TEST(OrthogonalPacking, UseSlack) {
using Item = OrthogonalPackingResult::Item;
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
auto result = opp_solver.TestFeasibility(
{10, 10, 10}, {10, 10, 10}, {11, 20},
OrthogonalPackingOptions{// Detect only trivial conflicts
.use_pairwise = false,
.use_dff_f0 = false,
.use_dff_f2 = false,
.brute_force_threshold = 0});
CHECK(result.GetResult() == DetectorStatus::INFEASIBLE);
EXPECT_THAT(result.GetItemsParticipatingOnConflict(),
testing::UnorderedElementsAre(
ItemIs(0, 10, 10), ItemIs(1, 10, 10), ItemIs(2, 10, 10)));
int position_of_index_zero =
std::find_if(result.GetItemsParticipatingOnConflict().begin(),
result.GetItemsParticipatingOnConflict().end(),
[](const Item& item) { return item.index == 0; }) -
result.GetItemsParticipatingOnConflict().begin();
result.TryUseSlackToReduceItemSize(
position_of_index_zero, OrthogonalPackingResult::Coord::kCoordX, 9);
EXPECT_THAT(result.GetItemsParticipatingOnConflict(),
testing::Contains(ItemIs(0, 9, 10)));
result.TryUseSlackToReduceItemSize(position_of_index_zero,
OrthogonalPackingResult::Coord::kCoordX);
// 2*10 + 10*10 + 10*10 = 220 = 11 * 20. So (2, 10) would fit.
EXPECT_THAT(result.GetItemsParticipatingOnConflict(),
testing::Contains(ItemIs(0, 3, 10)));
auto result2 = opp_solver.TestFeasibility(
{10, 10, 10}, {11, 10, 10}, {11, 20},
OrthogonalPackingOptions{// Detect only trivial conflicts
.use_pairwise = false,
.use_dff_f0 = false,
.use_dff_f2 = false,
.brute_force_threshold = 0});
position_of_index_zero =
std::find_if(result2.GetItemsParticipatingOnConflict().begin(),
result2.GetItemsParticipatingOnConflict().end(),
[](const Item& item) { return item.index == 0; }) -
result2.GetItemsParticipatingOnConflict().begin();
result2.TryUseSlackToReduceItemSize(position_of_index_zero,
OrthogonalPackingResult::Coord::kCoordX);
// 2*11 + 10*10 + 10*10 = 222 > 11 * 20 = 220. So (2, 11) does not fit.
EXPECT_THAT(result2.GetItemsParticipatingOnConflict(),
testing::Contains(ItemIs(0, 2, 11)));
}
TEST(OrthogonalPacking, InvertDFF) {
absl::BitGen random;
SharedStatistics stats;
OrthogonalPackingInfeasibilityDetector opp_solver(random, &stats);
auto result = opp_solver.TestFeasibility(
{4, 4, 8, 8}, {6, 6, 5, 5}, {13, 10},
OrthogonalPackingOptions{.use_pairwise = false,
.use_dff_f0 = false,
.use_dff_f2 = true,
.brute_force_threshold = 0});
CHECK(result.GetResult() == DetectorStatus::INFEASIBLE);
EXPECT_THAT(result.GetItemsParticipatingOnConflict(),
testing::UnorderedElementsAre(ItemIs(0, 3, 6), ItemIs(1, 3, 6),
ItemIs(2, 8, 5), ItemIs(3, 8, 5)));
}
} // namespace
} // namespace sat
} // namespace operations_research

158
ortools/sat/BUILD.bazel
View File

@@ -219,6 +219,21 @@ cc_library(
],
)
cc_test(
name = "cp_model_utils_test",
size = "small",
srcs = ["cp_model_utils_test.cc"],
deps = [
":cp_model_cc_proto",
":cp_model_utils",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/base:stl_util",
"//ortools/port:proto_utils",
"@abseil-cpp//absl/container:flat_hash_set",
],
)
cc_library(
name = "synchronization",
srcs = ["synchronization.cc"],
@@ -265,6 +280,24 @@ cc_library(
],
)
cc_test(
name = "synchronization_test",
size = "small",
srcs = ["synchronization_test.cc"],
deps = [
":cp_model_cc_proto",
":integer_base",
":model",
":synchronization",
":util",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/util:random_engine",
"@abseil-cpp//absl/time",
"@abseil-cpp//absl/types:span",
],
)
cc_library(
name = "cp_model_checker",
srcs = ["cp_model_checker.cc"],
@@ -709,6 +742,27 @@ cc_library(
],
)
cc_test(
name = "cp_model_solver_test",
size = "medium",
srcs = ["cp_model_solver_test.cc"],
deps = [
":cp_model_cc_proto",
":cp_model_checker",
":cp_model_solver",
":cp_model_test_utils",
":lp_utils",
":model",
":sat_parameters_cc_proto",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/linear_solver:linear_solver_cc_proto",
"//ortools/util:logging",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/strings",
],
)
cc_library(
name = "cp_model_mapping",
hdrs = ["cp_model_mapping.h"],
@@ -1042,6 +1096,36 @@ cc_library(
],
)
cc_test(
name = "cp_model_presolve_test",
size = "small",
srcs = ["cp_model_presolve_test.cc"],
tags = ["noautofuzz"],
deps = [
":cp_model_cc_proto",
":cp_model_checker",
":cp_model_presolve",
":cp_model_solver",
":cp_model_utils",
":lp_utils",
":model",
":presolve_context",
":sat_parameters_cc_proto",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/linear_solver:linear_solver_cc_proto",
"//ortools/lp_data",
"//ortools/lp_data:lp_parser",
"//ortools/lp_data:proto_utils",
"//ortools/port:proto_utils",
"//ortools/util:logging",
"//ortools/util:sorted_interval_list",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/random",
"@abseil-cpp//absl/random:bit_gen_ref",
],
)
cc_test(
name = "cp_model_presolve_random_test",
size = "medium",
@@ -2373,32 +2457,6 @@ cc_library(
],
)
cc_test(
name = "boolean_problem_test",
size = "small",
srcs = [
"boolean_problem_test.cc",
],
deps = [
":boolean_problem",
":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/strings",
],
)
cc_library(
name = "linear_relaxation",
srcs = ["linear_relaxation.cc"],
@@ -2780,6 +2838,7 @@ cc_library(
":cuts",
":integer",
":integer_base",
":intervals",
":linear_constraint",
":linear_constraint_manager",
":model",
@@ -2795,7 +2854,6 @@ cc_library(
"@abseil-cpp//absl/base:core_headers",
"@abseil-cpp//absl/container:btree",
"@abseil-cpp//absl/container:flat_hash_map",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/strings",
"@abseil-cpp//absl/types:span",
@@ -3312,6 +3370,27 @@ cc_library(
],
)
cc_test(
name = "2d_orthogonal_packing_test",
srcs = ["2d_orthogonal_packing_test.cc"],
deps = [
":2d_orthogonal_packing",
":2d_orthogonal_packing_testing",
":diffn_util",
":integer_base",
":synchronization",
"//ortools/algorithms:binary_search",
"//ortools/base:gmock_main",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/random",
"@abseil-cpp//absl/random:bit_gen_ref",
"@abseil-cpp//absl/random:distributions",
"@abseil-cpp//absl/strings",
"@abseil-cpp//absl/types:span",
"@com_google_benchmark//:benchmark",
],
)
cc_library(
name = "2d_try_edge_propagator",
srcs = ["2d_try_edge_propagator.cc"],
@@ -3762,6 +3841,31 @@ cc_library(
],
)
cc_test(
name = "opb_reader_test",
size = "small",
srcs = [
"opb_reader_test.cc",
],
deps = [
":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/strings",
],
)
cc_binary(
name = "sat_runner",
srcs = [

7926
ortools/sat/cp_model_presolve_test.cc Normal file
View File

File diff suppressed because it is too large Load Diff

4592
ortools/sat/cp_model_solver_test.cc Normal file
View File

File diff suppressed because it is too large Load Diff

361
ortools/sat/cp_model_utils_test.cc Normal file
View File

@@ -0,0 +1,361 @@
// Copyright 2010-2025 Google LLC
// 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 "ortools/sat/cp_model_utils.h"
#include <stdint.h>
#include <string>
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "gtest/gtest.h"
#include "ortools/base/gmock.h"
#include "ortools/base/parse_test_proto.h"
#include "ortools/base/stl_util.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/cp_model.pb.h"
namespace operations_research {
namespace sat {
namespace {
using ::google::protobuf::contrib::parse_proto::ParseTestProto;
using ::testing::UnorderedElementsAre;
TEST(LinearExpressionGcdTest, Empty) {
LinearExpressionProto expr;
EXPECT_EQ(LinearExpressionGcd(expr), 0);
}
TEST(LinearExpressionGcdTest, BasicCases1) {
LinearExpressionProto expr;
expr.set_offset(2);
expr.add_coeffs(4);
EXPECT_EQ(LinearExpressionGcd(expr), 2);
}
TEST(LinearExpressionGcdTest, BasicCases2) {
LinearExpressionProto expr;
expr.set_offset(5);
expr.add_coeffs(10);
EXPECT_EQ(LinearExpressionGcd(expr), 5);
}
TEST(LinearExpressionGcdTest, BasicCases3) {
LinearExpressionProto expr;
expr.set_offset(9);
expr.add_coeffs(12);
expr.add_coeffs(24);
EXPECT_EQ(LinearExpressionGcd(expr), 3);
}
TEST(AddReferencesUsedByConstraintTest, Literals) {
ConstraintProto ct;
ct.add_enforcement_literal(1);
auto* arg = ct.mutable_bool_and();
arg->add_literals(-10);
arg->add_literals(+10);
arg->add_literals(-20);
const IndexReferences references = GetReferencesUsedByConstraint(ct);
EXPECT_THAT(references.literals, UnorderedElementsAre(-10, +10, -20));
}
TEST(AddReferencesUsedByConstraintTest, IntegerConstraint) {
ConstraintProto ct;
auto* arg = ct.mutable_int_prod();
arg->mutable_target()->add_vars(7);
arg->mutable_target()->add_coeffs(2);
auto* term = arg->add_exprs();
term->add_vars(8);
term->add_coeffs(2);
term = arg->add_exprs();
term->add_vars(8);
term->add_coeffs(3);
term = arg->add_exprs();
term->add_vars(10);
term->add_coeffs(-2);
const IndexReferences references = GetReferencesUsedByConstraint(ct);
EXPECT_THAT(references.variables, UnorderedElementsAre(7, 8, 8, 10));
}
TEST(AddReferencesUsedByConstraintTest, LinearMaxConstraint) {
ConstraintProto ct;
auto* arg = ct.mutable_lin_max();
arg->mutable_target()->add_vars(7);
arg->add_exprs();
arg->add_exprs();
arg->mutable_exprs(0)->add_vars(8);
arg->mutable_exprs(0)->add_vars(9);
arg->mutable_exprs(1)->add_vars(9);
arg->mutable_exprs(1)->add_vars(10);
const IndexReferences references = GetReferencesUsedByConstraint(ct);
EXPECT_THAT(references.variables, UnorderedElementsAre(7, 8, 9, 9, 10));
}
TEST(AddReferencesUsedByConstraintTest, LinearConstraint) {
ConstraintProto ct;
auto* arg = ct.mutable_linear();
arg->add_vars(0);
arg->add_vars(1);
arg->add_vars(2);
const IndexReferences references = GetReferencesUsedByConstraint(ct);
EXPECT_THAT(references.variables, UnorderedElementsAre(0, 1, 2));
}
TEST(UsedIntervalTest, Intervals) {
ConstraintProto ct;
auto* arg = ct.mutable_no_overlap();
arg->add_intervals(0);
arg->add_intervals(1);
arg->add_intervals(2);
EXPECT_THAT(UsedIntervals(ct), UnorderedElementsAre(0, 1, 2));
}
TEST(UsedVariablesTest, BasicTest) {
ConstraintProto ct;
ct.add_enforcement_literal(NegatedRef(7));
auto* arg = ct.mutable_linear();
arg->add_vars(0);
arg->add_vars(1);
arg->add_vars(NegatedRef(2));
EXPECT_THAT(UsedVariables(ct), testing::ElementsAre(0, 1, 2, 7));
}
TEST(UsedVariablesTest, ConstraintWithMultipleEnforcement) {
ConstraintProto ct;
ct.add_enforcement_literal(NegatedRef(7));
ct.add_enforcement_literal(NegatedRef(18));
auto* arg = ct.mutable_linear();
arg->add_vars(0);
arg->add_vars(1);
arg->add_vars(NegatedRef(2));
EXPECT_THAT(UsedVariables(ct), testing::ElementsAre(0, 1, 2, 7, 18));
}
TEST(SetToNegatedLinearExpressionTest, BasicTest) {
LinearExpressionProto expr;
expr.set_offset(5);
expr.add_vars(1);
expr.add_coeffs(2);
expr.add_vars(-1);
expr.add_coeffs(-3);
LinearExpressionProto negated_expr;
SetToNegatedLinearExpression(expr, &negated_expr);
EXPECT_THAT(negated_expr.vars(), testing::ElementsAre(-2, 0));
EXPECT_THAT(negated_expr.coeffs(), testing::ElementsAre(2, -3));
EXPECT_EQ(-5, negated_expr.offset());
LinearExpressionProto expr2;
expr2.set_offset(3);
expr2.add_vars(2);
expr2.add_coeffs(3);
expr2.add_vars(-2);
expr2.add_coeffs(-4);
SetToNegatedLinearExpression(expr2, &negated_expr);
EXPECT_THAT(negated_expr.vars(), testing::ElementsAre(-3, 1));
EXPECT_THAT(negated_expr.coeffs(), testing::ElementsAre(3, -4));
EXPECT_EQ(-3, negated_expr.offset());
}
void Random(ConstraintProto ct) {
// The behavior of both functions differ on the enforcement_literal, so
// we clear it. TODO(user): make the behavior identical.
ct.clear_enforcement_literal();
absl::flat_hash_set<int> expected;
{
const IndexReferences references = GetReferencesUsedByConstraint(ct);
expected.insert(references.variables.begin(), references.variables.end());
expected.insert(references.literals.begin(), references.literals.end());
}
absl::flat_hash_set<int> var_and_literals;
ApplyToAllVariableIndices(
[&var_and_literals](int* ref) { var_and_literals.insert(*ref); }, &ct);
ApplyToAllLiteralIndices(
[&var_and_literals](int* ref) { var_and_literals.insert(*ref); }, &ct);
EXPECT_EQ(var_and_literals, expected) << ProtobufDebugString(ct);
std::vector<int> intervals;
ApplyToAllIntervalIndices(
[&intervals](int* ref) { intervals.push_back(*ref); }, &ct);
gtl::STLSortAndRemoveDuplicates(&intervals);
EXPECT_EQ(intervals, UsedIntervals(ct)) << ProtobufDebugString(ct);
}
TEST(ConstraintCaseNameTest, TestFewCases) {
EXPECT_EQ("kBoolOr",
ConstraintCaseName(ConstraintProto::ConstraintCase::kBoolOr));
EXPECT_EQ("kLinear",
ConstraintCaseName(ConstraintProto::ConstraintCase::kLinear));
EXPECT_EQ("kEmpty", ConstraintCaseName(
ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET));
}
TEST(ComputeInnerObjectiveTest, SimpleExample) {
const CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 5 ] }
variables { domain: [ 0, 5 ] }
objective {
vars: [ 0, 1 ]
coeffs: [ 2, 3 ]
offset: 3
scaling_factor: 1.5
}
)pb");
const std::vector<int64_t> solution = {2, 3};
EXPECT_EQ(ComputeInnerObjective(model_proto.objective(), solution), 13);
EXPECT_EQ(ScaleObjectiveValue(model_proto.objective(), 13), (13 + 3) * 1.5);
EXPECT_EQ(UnscaleObjectiveValue(model_proto.objective(), (13 + 3) * 1.5), 13);
}
TEST(GetRefFromExpressionTest, BasicAPI) {
LinearExpressionProto expr;
EXPECT_FALSE(ExpressionContainsSingleRef(expr));
expr.set_offset(1);
EXPECT_FALSE(ExpressionContainsSingleRef(expr));
expr.set_offset(0);
expr.add_vars(2);
expr.add_coeffs(1);
EXPECT_TRUE(ExpressionContainsSingleRef(expr));
EXPECT_EQ(2, GetSingleRefFromExpression(expr));
expr.set_coeffs(0, -1);
EXPECT_TRUE(ExpressionContainsSingleRef(expr));
EXPECT_EQ(-3, GetSingleRefFromExpression(expr));
expr.set_coeffs(0, 2);
EXPECT_FALSE(ExpressionContainsSingleRef(expr));
expr.set_coeffs(0, 1);
expr.add_vars(3);
expr.add_coeffs(-1);
EXPECT_FALSE(ExpressionContainsSingleRef(expr));
}
TEST(AddLinearExpressionToLinearConstraintTest, BasicApi) {
LinearConstraintProto linear;
linear.add_vars(1);
linear.add_coeffs(-1);
linear.add_domain(2);
linear.add_domain(4);
LinearExpressionProto expr;
expr.add_vars(2);
expr.add_coeffs(2);
expr.add_vars(3);
expr.add_coeffs(5);
expr.set_offset(1);
AddLinearExpressionToLinearConstraint(expr, -7, &linear);
const LinearConstraintProto expected_linear_constraint = ParseTestProto(R"pb(
vars: [ 1, 2, 3 ]
coeffs: [ -1, -14, -35 ]
domain: [ 9, 11 ]
)pb");
EXPECT_THAT(linear, testing::EqualsProto(expected_linear_constraint));
}
TEST(AddWeightedLiteralToLinearConstraintTest, BasicApi) {
LinearConstraintProto linear;
linear.add_vars(1);
linear.add_coeffs(-1);
linear.add_domain(2);
linear.add_domain(4);
int64_t offset = 0;
AddWeightedLiteralToLinearConstraint(0, 4, &linear, &offset);
const LinearConstraintProto expected_linear_constraint_1 = ParseTestProto(
R"pb(
vars: [ 1, 0 ]
coeffs: [ -1, 4 ]
domain: [ 2, 4 ]
)pb");
EXPECT_THAT(linear, testing::EqualsProto(expected_linear_constraint_1));
EXPECT_EQ(offset, 0);
AddWeightedLiteralToLinearConstraint(-3, 5, &linear, &offset);
const LinearConstraintProto expected_linear_constraint_2 =
ParseTestProto(R"pb(
vars: [ 1, 0, 2 ]
coeffs: [ -1, 4, -5 ]
domain: [ 2, 4 ]
)pb");
EXPECT_THAT(linear, testing::EqualsProto(expected_linear_constraint_2));
EXPECT_EQ(offset, 5);
}
TEST(SafeAddLinearExpressionToLinearConstraintTest, BasicApi) {
LinearConstraintProto linear;
linear.add_vars(1);
linear.add_coeffs(-1);
linear.add_domain(2);
linear.add_domain(4);
LinearExpressionProto expr;
expr.add_vars(2);
expr.add_coeffs(2);
expr.add_vars(3);
expr.add_coeffs(5);
expr.set_offset(1);
EXPECT_TRUE(SafeAddLinearExpressionToLinearConstraint(expr, -7, &linear));
LinearExpressionProto large_coeff;
large_coeff.add_vars(0);
large_coeff.add_coeffs(1e10);
EXPECT_FALSE(
SafeAddLinearExpressionToLinearConstraint(large_coeff, 1e10, &linear));
LinearExpressionProto large_offset;
large_offset.set_offset(1e10);
EXPECT_FALSE(
SafeAddLinearExpressionToLinearConstraint(large_offset, 1e10, &linear));
}
// Fingerprint must be stable. So we can use golden values.
TEST(FingerprintTest, BasicApi) {
const LinearExpressionProto lin = ParseTestProto(R"pb(
vars: [ 1, 2, 3 ]
coeffs: [ -1, -14, -35 ]
offset: 11
)pb");
EXPECT_EQ(uint64_t{0x871AE5CE74BFBE37},
FingerprintExpression(lin, kDefaultFingerprintSeed));
EXPECT_EQ(uint64_t{0x3E7E7DEAEF2AB62C},
FingerprintRepeatedField(lin.vars(), kDefaultFingerprintSeed));
EXPECT_EQ(uint64_t{0x85715ADBDFD6F8AD},
FingerprintSingleField(lin.offset(), kDefaultFingerprintSeed));
}
TEST(ConvertCpModelProtoToCnfTest, BasicExample) {
const CpModelProto model_proto = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
constraints { bool_or { literals: [ 0, 1, 2 ] } }
constraints { bool_or { literals: [ -1, -2 ] } }
constraints { bool_or { literals: [ -1, -2 ] } }
constraints {
enforcement_literal: [ 0, 1 ]
bool_and { literals: [ -1, -2 ] }
}
)pb");
const std::string expected = R"(p cnf 3 5
1 2 3 0
-1 -2 0
-1 -2 0
-1 -2 -1 0
-1 -2 -2 0
)";
std::string cnf;
EXPECT_TRUE(ConvertCpModelProtoToCnf(model_proto, &cnf));
EXPECT_EQ(expected, cnf);
}
} // namespace
} // namespace sat
} // namespace operations_research

66
ortools/sat/opb_reader.h
View File

@@ -50,6 +50,10 @@ class OpbReader {
// Returns the number of variables in the problem.
int num_variables() const { return num_variables_; }
// Returns true if the model is supported. A model is not supported if it
// contains an integer that does not fit in int64_t.
bool model_is_supported() const { return model_is_supported_; }
// Loads the given opb filename into the given problem.
// Returns true on success.
bool LoadAndValidate(const std::string& filename, CpModelProto* model) {
@@ -58,6 +62,7 @@ class OpbReader {
num_variables_ = 0;
int num_lines = 0;
model_is_supported_ = true;
// Read constraints line by line (1 constraint per line).
// We process into a temporary structure to support non linear constraints
@@ -65,6 +70,10 @@ class OpbReader {
for (const std::string& line : FileLines(filename)) {
++num_lines;
ProcessNewLine(line);
if (!model_is_supported_) {
LOG(ERROR) << "Unsupported model: '" << filename << "'";
return false;
}
}
if (num_lines == 0) {
LOG(ERROR) << "File '" << filename << "' is empty or can't be read.";
@@ -110,7 +119,7 @@ class OpbReader {
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
// Since the problem name is not stored in the opb format, we infer it from
// the file name.
static std::string ExtractProblemName(const std::string& filename) {
const int found = filename.find_last_of('/');
@@ -132,21 +141,20 @@ class OpbReader {
const std::string& word = words[i];
if (word.empty() || word[0] == ';') continue;
if (word[0] == 'x') {
int index;
CHECK(absl::SimpleAtoi(word.substr(1), &index));
const int index = ParseIndex(word.substr(1));
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));
const int index = ParseIndex(word.substr(2));
num_variables_ = std::max(num_variables_, index);
objective_.back().literals.push_back(
NegatedRef(PbLiteralToCpModelLiteral(index)));
} else {
int64_t coefficient;
CHECK(absl::SimpleAtoi(word, &coefficient));
objective_.push_back({coefficient, {}});
// Note that coefficient always appear before the variable/variables.
PbTerm term;
if (!ParseInt64Into(word, &term.coeff)) return;
objective_.emplace_back(std::move(term));
}
}
@@ -165,40 +173,35 @@ class OpbReader {
const std::string& word = words[i];
CHECK(!word.empty());
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;
if (!ParseInt64Into(word.substr(1, word.size() - 2),
&constraint.soft_cost)) {
return;
}
} else if (word == ">=") {
CHECK_LT(i + 1, words.size());
int64_t rhs;
CHECK(absl::SimpleAtoi(words[i + 1], &rhs));
constraint.type = GE_OPERATION;
constraint.rhs = rhs;
if (!ParseInt64Into(words[i + 1], &constraint.rhs)) return;
break;
} else if (word == "=") {
CHECK_LT(i + 1, words.size());
int64_t rhs;
CHECK(absl::SimpleAtoi(words[i + 1], &rhs));
constraint.type = EQ_OPERATION;
constraint.rhs = rhs;
if (!ParseInt64Into(words[i + 1], &constraint.rhs)) return;
break;
} else if (word[0] == 'x') {
int index;
CHECK(absl::SimpleAtoi(word.substr(1), &index));
const int index = ParseIndex(word.substr(1));
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));
const int index = ParseIndex(word.substr(2));
num_variables_ = std::max(num_variables_, index);
constraint.terms.back().literals.push_back(
NegatedRef(PbLiteralToCpModelLiteral(index)));
} else {
// Note that coefficient always appear before the variable/variables.
int64_t coefficient;
CHECK(absl::SimpleAtoi(word, &coefficient));
constraint.terms.push_back({coefficient, {}});
PbTerm term;
if (!ParseInt64Into(word, &term.coeff)) return;
constraint.terms.emplace_back(std::move(term));
}
}
@@ -257,6 +260,20 @@ class OpbReader {
return pb_literal > 0 ? pb_literal - 1 : -pb_literal;
}
bool ParseInt64Into(const std::string& word, int64_t* value) {
if (!absl::SimpleAtoi(word, value)) {
model_is_supported_ = false;
return false;
}
return true;
}
static int ParseIndex(const std::string& word) {
int index;
CHECK(absl::SimpleAtoi(word, &index));
return index;
}
int GetVariable(const PbTerm& term, CpModelProto* model) {
CHECK(!term.literals.empty());
if (term.literals.size() == 1) {
@@ -346,6 +363,7 @@ class OpbReader {
std::vector<PbTerm> objective_;
std::vector<PbConstraint> constraints_;
absl::flat_hash_map<absl::Span<const int>, int> product_to_var_;
bool model_is_supported_ = true;
};
} // namespace sat

17
ortools/sat/boolean_problem_test.cc → ortools/sat/opb_reader_test.cc
View File

@@ -11,7 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/boolean_problem.h"
#include "ortools/sat/opb_reader.h"
#include <memory>
#include <string>
@@ -28,7 +28,6 @@
#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"
@@ -98,6 +97,20 @@ TEST(LoadAndValidateBooleanProblemTest, ZeroCoefficients) {
EXPECT_FALSE(reader.LoadAndValidate(filename, &problem));
}
TEST(LoadAndValidateBooleanProblemTest, IntegerOverflow) {
std::string file =
"min: 1 x1 1 x2 ;\n"
"1 x1 2 x2 >= 1 ;\n"
"1 x1 123456789123456789123456789 x2 >= 1 ;\n";
CpModelProto problem;
OpbReader reader;
const std::string filename =
file::JoinPath(::testing::TempDir(), "file2.opb");
CHECK_OK(file::SetContents(filename, file, file::Defaults()));
EXPECT_FALSE(reader.LoadAndValidate(filename, &problem));
EXPECT_FALSE(reader.model_is_supported());
}
void FindSymmetries(
absl::string_view file,
std::vector<std::unique_ptr<SparsePermutation>>* generators) {

7
ortools/sat/sat_solver.h
View File

@@ -147,9 +147,6 @@ class SatSolver {
// return true.
bool ModelIsUnsat() const { return model_is_unsat_; }
// TODO(user): remove this function.
bool IsModelUnsat() const { return model_is_unsat_; } // DEPRECATED
// Adds and registers the given propagator with the sat solver. Note that
// during propagation, they will be called in the order they were added.
void AddPropagator(SatPropagator* propagator);
@@ -338,7 +335,7 @@ class SatSolver {
// Helper functions to get the correct status when one of the functions above
// returns false.
Status UnsatStatus() const {
return IsModelUnsat() ? INFEASIBLE : ASSUMPTIONS_UNSAT;
return ModelIsUnsat() ? INFEASIBLE : ASSUMPTIONS_UNSAT;
}
// Extract the current problem clauses. The Output type must support the two
@@ -349,7 +346,7 @@ class SatSolver {
// TODO(user): also copy the removable clauses?
template <typename Output>
void ExtractClauses(Output* out) {
CHECK(!IsModelUnsat());
CHECK(!ModelIsUnsat());
Backtrack(0);
if (!FinishPropagation()) return;

2
ortools/sat/simplification.cc
View File

@@ -820,7 +820,7 @@ void SatPresolver::RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x) {
}
Literal SatPresolver::FindLiteralWithShortestOccurrenceList(
const std::vector<Literal>& clause) {
absl::Span<const Literal> clause) {
DCHECK(!clause.empty());
Literal result = clause.front();
int best_size = literal_to_clause_sizes_[result];

2
ortools/sat/simplification.h
View File

@@ -257,7 +257,7 @@ class SatPresolver {
// Finds the literal from the clause that occur the less in the clause
// database.
Literal FindLiteralWithShortestOccurrenceList(
const std::vector<Literal>& clause);
absl::Span<const Literal> clause);
LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
const std::vector<Literal>& clause, Literal to_exclude);

1133
ortools/sat/synchronization_test.cc Normal file
View File

File diff suppressed because it is too large Load Diff

4
ortools/set_cover/set_cover_model.cc
View File

@@ -428,7 +428,7 @@ SparseRowView SetCoverModel::ComputeSparseRowViewSlice(SubsetIndex begin_subset,
}
std::vector<SparseRowView> SetCoverModel::CutSparseRowViewInSlices(
const std::vector<SubsetIndex>& partition_points) {
absl::Span<const SubsetIndex> partition_points) {
std::vector<SparseRowView> row_views;
row_views.reserve(partition_points.size());
SubsetIndex begin_subset(0);
@@ -441,7 +441,7 @@ std::vector<SparseRowView> SetCoverModel::CutSparseRowViewInSlices(
}
SparseRowView SetCoverModel::ReduceSparseRowViewSlices(
const std::vector<SparseRowView>& slices) {
absl::Span<const SparseRowView> slices) {
SparseRowView result_rows;
// This is not a ReduceTree. This will be done later through parallelism.
result_rows.reserve(num_elements_);

5
ortools/set_cover/set_cover_model.h
View File

@@ -20,6 +20,7 @@
#include "absl/log/check.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/base/strong_int.h"
#include "ortools/base/strong_vector.h"
#include "ortools/set_cover/base_types.h"
@@ -250,13 +251,13 @@ class SetCoverModel {
// Returns a vector of row views, each corresponding to a partition of the
// problem. The partitions are defined by the given partition points.
std::vector<SparseRowView> CutSparseRowViewInSlices(
const std::vector<SubsetIndex>& partition_points);
absl::Span<const SubsetIndex> partition_points);
// Returns the union of the rows of the given row views.
// The returned view is valid only as long as the given row views are valid.
// The indices in the rows are sorted.
SparseRowView ReduceSparseRowViewSlices(
const std::vector<SparseRowView>& row_slices);
absl::Span<const SparseRowView> row_slices);
// Returns true if the problem is feasible, i.e. if the subsets cover all
// the elements. Could be const, but it updates the feasibility_duration_