90 lines
3.6 KiB
C++
90 lines
3.6 KiB
C++
// 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/sat_sweeping.h"
|
|
|
|
#include <array>
|
|
#include <utility>
|
|
|
|
#include "absl/types/span.h"
|
|
#include "gtest/gtest.h"
|
|
#include "ortools/base/gmock.h"
|
|
#include "ortools/sat/cp_model_utils.h"
|
|
#include "ortools/sat/model.h"
|
|
#include "ortools/sat/sat_base.h"
|
|
#include "ortools/sat/sat_inprocessing.h"
|
|
#include "ortools/sat/sat_solver.h"
|
|
#include "ortools/sat/util.h"
|
|
#include "ortools/util/time_limit.h"
|
|
|
|
namespace operations_research {
|
|
namespace sat {
|
|
namespace {
|
|
|
|
using ::testing::ElementsAre;
|
|
|
|
TEST(SatSweepingTest, FullSatSweepingOneProblem) {
|
|
static constexpr std::array<int, 3> kClausesArray[] = {
|
|
{9, -3, 15}, {-8, 19, -19}, {1, -6, -20}, {-7, 8, 2},
|
|
{2, 14, -14}, {3, 14, 19}, {10, -9, -6}, {2, -17, 18},
|
|
{10, 4, -12}, {9, 2, -15}, {1, 14, 17}, {-15, 11, 10},
|
|
{17, -19, -8}, {12, 19, 8}, {10, -10, -14}, {3, 17, -9},
|
|
{-7, -17, 4}, {-7, 10, -15}, {5, 1, 19}, {15, -18, -17},
|
|
{3, -13, -20}, {10, 16, -8}, {12, -11, -9}, {-11, 12, 18},
|
|
{11, -19, 13}, {9, -1, -20}, {18, -20, 12}, {12, 1, 10},
|
|
{16, 18, -18}, {18, -20, -10}, {-18, 15, 14}, {-18, 6, -20},
|
|
{0, -14, -17}, {0, -11, -18}, {-18, 7, 12}, {-8, 3, 15},
|
|
{17, 19, 1}, {-20, -1, 3}, {-19, 1, -9}, {-9, -16, -15},
|
|
{-2, 11, 8}, {4, 18, 5}, {-8, -5, -13}, {-18, 19, -6},
|
|
{4, -18, 11}, {1, 4, 18}, {-5, -8, -11}, {-20, -17, 10},
|
|
{-18, -14, -16}, {-3, -18, -7}, {-11, 19, 16}, {-1, -15, -13},
|
|
{8, -5, 10}, {-17, -7, -1}, {-6, -1, -16}, {-3, -15, -19},
|
|
{16, 13, 10}, {-17, 11, 12}, {15, 11, -2}, {13, 9, -16},
|
|
{15, -9, -7}, {-8, -15, 1}, {-19, -10, 0}, {11, -15, -20},
|
|
{12, -10, 8}, {16, 6, 17}, {19, 14, -2}, {-6, -7, -1},
|
|
{13, 10, 14}, {17, 12, -9}, {-4, -12, -2}, {-13, -5, -9},
|
|
{-2, -5, -8}, {12, -4, -11}, {-5, -10, 18},
|
|
};
|
|
constexpr absl::Span<const std::array<int, 3>> kClauses(kClausesArray);
|
|
|
|
CompactVectorVector<int, Literal> clauses;
|
|
for (const std::array<int, 3>& clause : kClauses) {
|
|
clauses.Add({});
|
|
for (int literal : clause) {
|
|
if (literal >= 0) {
|
|
clauses.AppendToLastVector(Literal(BooleanVariable(literal), true));
|
|
} else {
|
|
const BooleanVariable var(PositiveRef(literal));
|
|
clauses.AppendToLastVector(Literal(var, false));
|
|
}
|
|
}
|
|
}
|
|
|
|
TimeLimit time_limit;
|
|
const SatSweepingResult result = DoFullSatSweeping(
|
|
std::move(clauses), &time_limit,
|
|
[](Model* m) { m->GetOrCreate<Inprocessing>()->InprocessingRound(); });
|
|
|
|
// There is only one possible correct sweep result for this model. Check it.
|
|
EXPECT_EQ(result.status, SatSolver::FEASIBLE);
|
|
EXPECT_THAT(result.binary_clauses,
|
|
testing::Contains(testing::Pair(Literal(+12), Literal(+9))));
|
|
EXPECT_THAT(result.binary_clauses,
|
|
testing::Contains(testing::Pair(Literal(+17), Literal(+7))));
|
|
EXPECT_THAT(result.unary_clauses, ElementsAre(Literal(-18)));
|
|
}
|
|
|
|
} // namespace
|
|
} // namespace sat
|
|
} // namespace operations_research
|