2025-01-10 11:35:44 +01:00
|
|
|
// Copyright 2010-2025 Google LLC
|
2018-11-24 19:34:08 +01:00
|
|
|
// 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.
|
|
|
|
|
|
|
|
|
|
// Costas Array Problem
|
|
|
|
|
//
|
|
|
|
|
// Finds an NxN matrix of 0s and 1s, with only one 1 per row,
|
|
|
|
|
// and one 1 per column, such that all displacement vectors
|
|
|
|
|
// between each pair of 1s are distinct.
|
|
|
|
|
//
|
|
|
|
|
// This example contains two separate implementations. CostasHard()
|
|
|
|
|
// uses hard constraints, whereas CostasSoft() uses a minimizer to
|
|
|
|
|
// minimize the number of duplicates.
|
2021-01-14 10:48:19 +01:00
|
|
|
|
2021-04-02 14:58:16 +02:00
|
|
|
#include <cstdint>
|
2018-11-24 19:34:08 +01:00
|
|
|
#include <ctime>
|
|
|
|
|
#include <set>
|
2022-03-25 10:07:27 +01:00
|
|
|
#include <string>
|
2018-11-24 19:34:08 +01:00
|
|
|
#include <utility>
|
2022-09-09 16:49:24 +02:00
|
|
|
#include <vector>
|
2018-11-24 19:34:08 +01:00
|
|
|
|
2025-02-25 16:03:40 +01:00
|
|
|
#include "absl/base/log_severity.h"
|
2021-01-14 10:48:19 +01:00
|
|
|
#include "absl/flags/flag.h"
|
2025-02-25 16:03:40 +01:00
|
|
|
#include "absl/log/globals.h"
|
2025-03-04 21:10:09 +01:00
|
|
|
#include "absl/log/log.h"
|
2018-11-28 10:37:45 +01:00
|
|
|
#include "absl/strings/str_cat.h"
|
|
|
|
|
#include "absl/strings/str_format.h"
|
2023-12-03 16:59:16 +01:00
|
|
|
#include "absl/types/span.h"
|
2022-02-25 09:47:52 +01:00
|
|
|
#include "ortools/base/init_google.h"
|
2023-08-24 17:14:58 +02:00
|
|
|
#include "ortools/base/types.h"
|
2018-11-24 19:34:08 +01:00
|
|
|
#include "ortools/sat/cp_model.h"
|
|
|
|
|
#include "ortools/sat/model.h"
|
|
|
|
|
|
2020-10-23 11:50:14 +02:00
|
|
|
ABSL_FLAG(int, minsize, 0, "Minimum problem size.");
|
|
|
|
|
ABSL_FLAG(int, maxsize, 0, "Maximum problem size.");
|
|
|
|
|
ABSL_FLAG(int, model, 1,
|
|
|
|
|
"Model type: 1 integer variables hard, 2 boolean variables, 3 "
|
|
|
|
|
"boolean_variable soft");
|
|
|
|
|
ABSL_FLAG(std::string, params, "", "Sat parameters.");
|
2018-11-24 19:34:08 +01:00
|
|
|
|
|
|
|
|
namespace operations_research {
|
|
|
|
|
namespace sat {
|
|
|
|
|
|
|
|
|
|
// Checks that all pairwise distances are unique and returns all violators
|
2023-12-03 16:59:16 +01:00
|
|
|
void CheckConstraintViolators(absl::Span<const int64_t> vars,
|
2020-10-29 14:25:39 +01:00
|
|
|
std::vector<int>* const violators) {
|
2018-11-24 19:34:08 +01:00
|
|
|
int dim = vars.size();
|
|
|
|
|
|
|
|
|
|
// Check that all indices are unique
|
|
|
|
|
for (int i = 0; i < dim; ++i) {
|
|
|
|
|
for (int k = i + 1; k < dim; ++k) {
|
|
|
|
|
if (vars[i] == vars[k]) {
|
|
|
|
|
violators->push_back(i);
|
|
|
|
|
violators->push_back(k);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Check that all differences are unique for each level
|
|
|
|
|
for (int level = 1; level < dim; ++level) {
|
|
|
|
|
for (int i = 0; i < dim - level; ++i) {
|
|
|
|
|
const int difference = vars[i + level] - vars[i];
|
|
|
|
|
|
|
|
|
|
for (int k = i + 1; k < dim - level; ++k) {
|
|
|
|
|
if (difference == vars[k + level] - vars[k]) {
|
|
|
|
|
violators->push_back(k + level);
|
|
|
|
|
violators->push_back(k);
|
|
|
|
|
violators->push_back(i + level);
|
|
|
|
|
violators->push_back(i);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Check that all pairwise differences are unique
|
2024-03-25 11:59:02 +01:00
|
|
|
bool CheckCostas(absl::Span<const int64_t> vars) {
|
2018-11-24 19:34:08 +01:00
|
|
|
std::vector<int> violators;
|
|
|
|
|
|
|
|
|
|
CheckConstraintViolators(vars, &violators);
|
|
|
|
|
|
|
|
|
|
return violators.empty();
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Computes a Costas Array.
|
|
|
|
|
void CostasHard(const int dim) {
|
|
|
|
|
CpModelBuilder cp_model;
|
|
|
|
|
|
|
|
|
|
// create the variables
|
|
|
|
|
std::vector<IntVar> vars;
|
|
|
|
|
Domain domain(1, dim);
|
|
|
|
|
for (int i = 0; i < dim; ++i) {
|
2020-10-22 23:36:58 +02:00
|
|
|
vars.push_back(
|
|
|
|
|
cp_model.NewIntVar(domain).WithName(absl::StrCat("var_", i)));
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
cp_model.AddAllDifferent(vars);
|
|
|
|
|
|
|
|
|
|
// Check that the pairwise difference is unique
|
|
|
|
|
for (int i = 1; i < dim; ++i) {
|
|
|
|
|
std::vector<IntVar> subset;
|
2021-01-14 10:48:19 +01:00
|
|
|
Domain difference_domain(-dim, dim);
|
2018-11-24 19:34:08 +01:00
|
|
|
|
|
|
|
|
for (int j = 0; j < dim - i; ++j) {
|
2021-01-14 10:48:19 +01:00
|
|
|
IntVar diff = cp_model.NewIntVar(difference_domain);
|
|
|
|
|
subset.push_back(diff);
|
2021-12-09 15:29:49 +01:00
|
|
|
cp_model.AddEquality(diff, vars[j + i] - vars[j]);
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
cp_model.AddAllDifferent(subset);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
Model model;
|
2020-10-21 00:21:54 +02:00
|
|
|
if (!absl::GetFlag(FLAGS_params).empty()) {
|
|
|
|
|
model.Add(NewSatParameters(absl::GetFlag(FLAGS_params)));
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
2019-05-15 20:19:00 +02:00
|
|
|
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
|
2018-11-24 19:34:08 +01:00
|
|
|
|
2021-01-14 10:48:19 +01:00
|
|
|
if (response.status() == CpSolverStatus::OPTIMAL) {
|
2021-04-02 14:58:16 +02:00
|
|
|
std::vector<int64_t> costas_matrix;
|
2018-11-24 19:34:08 +01:00
|
|
|
std::string output;
|
|
|
|
|
|
|
|
|
|
for (int n = 0; n < dim; ++n) {
|
2021-04-02 14:58:16 +02:00
|
|
|
const int64_t v = SolutionIntegerValue(response, vars[n]);
|
2018-11-24 19:34:08 +01:00
|
|
|
costas_matrix.push_back(v);
|
|
|
|
|
absl::StrAppendFormat(&output, "%3lld", v);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
LOG(INFO) << output << " (" << response.wall_time() << " s)";
|
|
|
|
|
|
|
|
|
|
CHECK(CheckCostas(costas_matrix))
|
|
|
|
|
<< ": Solution is not a valid Costas Matrix.";
|
|
|
|
|
} else {
|
|
|
|
|
LOG(INFO) << "No solution found.";
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Computes a Costas Array.
|
|
|
|
|
void CostasBool(const int dim) {
|
|
|
|
|
CpModelBuilder cp_model;
|
|
|
|
|
|
|
|
|
|
// create the variables
|
2021-01-14 10:48:19 +01:00
|
|
|
std::vector<std::vector<BoolVar>> vars(dim);
|
|
|
|
|
std::vector<std::vector<BoolVar>> transposed_vars(dim);
|
2018-11-24 19:34:08 +01:00
|
|
|
for (int i = 0; i < dim; ++i) {
|
|
|
|
|
for (int j = 0; j < dim; ++j) {
|
|
|
|
|
const BoolVar var = cp_model.NewBoolVar();
|
|
|
|
|
vars[i].push_back(var);
|
|
|
|
|
transposed_vars[j].push_back(var);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
for (int i = 0; i < dim; ++i) {
|
2021-12-08 16:29:40 +01:00
|
|
|
cp_model.AddEquality(LinearExpr::Sum(vars[i]), 1);
|
|
|
|
|
cp_model.AddEquality(LinearExpr::Sum(transposed_vars[i]), 1);
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Check that the pairwise difference is unique
|
|
|
|
|
for (int step = 1; step < dim; ++step) {
|
|
|
|
|
for (int diff = 1; diff < dim - 1; ++diff) {
|
|
|
|
|
std::vector<BoolVar> positive_diffs;
|
|
|
|
|
std::vector<BoolVar> negative_diffs;
|
|
|
|
|
for (int var = 0; var < dim - step; ++var) {
|
|
|
|
|
for (int value = 0; value < dim - diff; ++value) {
|
|
|
|
|
const BoolVar pos = cp_model.NewBoolVar();
|
|
|
|
|
const BoolVar neg = cp_model.NewBoolVar();
|
|
|
|
|
positive_diffs.push_back(pos);
|
|
|
|
|
negative_diffs.push_back(neg);
|
2023-12-15 14:10:44 +01:00
|
|
|
cp_model.AddBoolOr(
|
|
|
|
|
{~vars[var][value], ~vars[var + step][value + diff], pos});
|
|
|
|
|
cp_model.AddBoolOr(
|
|
|
|
|
{~vars[var][value + diff], ~vars[var + step][value], neg});
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
}
|
2021-12-08 16:29:40 +01:00
|
|
|
cp_model.AddLessOrEqual(LinearExpr::Sum(positive_diffs), 1);
|
|
|
|
|
cp_model.AddLessOrEqual(LinearExpr::Sum(negative_diffs), 1);
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
Model model;
|
2020-10-21 00:21:54 +02:00
|
|
|
if (!absl::GetFlag(FLAGS_params).empty()) {
|
|
|
|
|
model.Add(NewSatParameters(absl::GetFlag(FLAGS_params)));
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
2019-05-15 20:19:00 +02:00
|
|
|
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
|
2018-11-24 19:34:08 +01:00
|
|
|
|
2020-09-20 09:04:28 +02:00
|
|
|
if (response.status() == CpSolverStatus::OPTIMAL) {
|
2021-04-02 14:58:16 +02:00
|
|
|
std::vector<int64_t> costas_matrix;
|
2018-11-24 19:34:08 +01:00
|
|
|
std::string output;
|
|
|
|
|
|
|
|
|
|
for (int n = 0; n < dim; ++n) {
|
|
|
|
|
for (int v = 0; v < dim; ++v) {
|
|
|
|
|
if (SolutionBooleanValue(response, vars[n][v])) {
|
|
|
|
|
costas_matrix.push_back(v + 1);
|
|
|
|
|
absl::StrAppendFormat(&output, "%3lld", v + 1);
|
|
|
|
|
break;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
LOG(INFO) << output << " (" << response.wall_time() << " s)";
|
|
|
|
|
|
|
|
|
|
CHECK(CheckCostas(costas_matrix))
|
|
|
|
|
<< ": Solution is not a valid Costas Matrix.";
|
|
|
|
|
} else {
|
|
|
|
|
LOG(INFO) << "No solution found.";
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Computes a Costas Array with a minimization objective.
|
|
|
|
|
void CostasBoolSoft(const int dim) {
|
|
|
|
|
CpModelBuilder cp_model;
|
|
|
|
|
|
|
|
|
|
// create the variables
|
2021-01-14 10:48:19 +01:00
|
|
|
std::vector<std::vector<BoolVar>> vars(dim);
|
|
|
|
|
std::vector<std::vector<BoolVar>> transposed_vars(dim);
|
2018-11-24 19:34:08 +01:00
|
|
|
for (int i = 0; i < dim; ++i) {
|
|
|
|
|
for (int j = 0; j < dim; ++j) {
|
|
|
|
|
const BoolVar var = cp_model.NewBoolVar();
|
|
|
|
|
vars[i].push_back(var);
|
|
|
|
|
transposed_vars[j].push_back(var);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
for (int i = 0; i < dim; ++i) {
|
2021-12-08 16:29:40 +01:00
|
|
|
cp_model.AddEquality(LinearExpr::Sum(vars[i]), 1);
|
|
|
|
|
cp_model.AddEquality(LinearExpr::Sum(transposed_vars[i]), 1);
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
std::vector<IntVar> all_violations;
|
|
|
|
|
// Check that the pairwise difference is unique
|
|
|
|
|
for (int step = 1; step < dim; ++step) {
|
|
|
|
|
for (int diff = 1; diff < dim - 1; ++diff) {
|
|
|
|
|
std::vector<BoolVar> positive_diffs;
|
|
|
|
|
std::vector<BoolVar> negative_diffs;
|
|
|
|
|
for (int var = 0; var < dim - step; ++var) {
|
|
|
|
|
for (int value = 0; value < dim - diff; ++value) {
|
|
|
|
|
const BoolVar pos = cp_model.NewBoolVar();
|
|
|
|
|
const BoolVar neg = cp_model.NewBoolVar();
|
|
|
|
|
positive_diffs.push_back(pos);
|
|
|
|
|
negative_diffs.push_back(neg);
|
2023-12-15 14:10:44 +01:00
|
|
|
cp_model.AddBoolOr(
|
|
|
|
|
{~vars[var][value], ~vars[var + step][value + diff], pos});
|
|
|
|
|
cp_model.AddBoolOr(
|
|
|
|
|
{~vars[var][value + diff], ~vars[var + step][value], neg});
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
const IntVar pos_var =
|
|
|
|
|
cp_model.NewIntVar(Domain(0, positive_diffs.size()));
|
|
|
|
|
const IntVar neg_var =
|
|
|
|
|
cp_model.NewIntVar(Domain(0, negative_diffs.size()));
|
2021-12-09 15:29:49 +01:00
|
|
|
cp_model.AddGreaterOrEqual(pos_var, LinearExpr::Sum(positive_diffs) - 1);
|
|
|
|
|
cp_model.AddGreaterOrEqual(neg_var, LinearExpr::Sum(negative_diffs) - 1);
|
2018-11-24 19:34:08 +01:00
|
|
|
all_violations.push_back(pos_var);
|
|
|
|
|
all_violations.push_back(neg_var);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
cp_model.Minimize(LinearExpr::Sum(all_violations));
|
|
|
|
|
|
|
|
|
|
Model model;
|
2020-10-21 00:21:54 +02:00
|
|
|
if (!absl::GetFlag(FLAGS_params).empty()) {
|
|
|
|
|
model.Add(NewSatParameters(absl::GetFlag(FLAGS_params)));
|
2018-11-24 19:34:08 +01:00
|
|
|
}
|
2019-05-15 20:19:00 +02:00
|
|
|
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
|
2018-11-24 19:34:08 +01:00
|
|
|
|
|
|
|
|
if (response.status() == CpSolverStatus::OPTIMAL) {
|
2021-04-02 14:58:16 +02:00
|
|
|
std::vector<int64_t> costas_matrix;
|
2018-11-24 19:34:08 +01:00
|
|
|
std::string output;
|
|
|
|
|
|
|
|
|
|
for (int n = 0; n < dim; ++n) {
|
|
|
|
|
for (int v = 0; v < dim; ++v) {
|
|
|
|
|
if (SolutionBooleanValue(response, vars[n][v])) {
|
|
|
|
|
costas_matrix.push_back(v + 1);
|
|
|
|
|
absl::StrAppendFormat(&output, "%3lld", v + 1);
|
|
|
|
|
break;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
LOG(INFO) << output << " (" << response.wall_time() << " s)";
|
|
|
|
|
|
|
|
|
|
CHECK(CheckCostas(costas_matrix))
|
|
|
|
|
<< ": Solution is not a valid Costas Matrix.";
|
|
|
|
|
} else {
|
|
|
|
|
LOG(INFO) << "No solution found.";
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
} // namespace sat
|
|
|
|
|
} // namespace operations_research
|
2018-11-24 19:34:08 +01:00
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
int main(int argc, char** argv) {
|
2025-02-25 16:03:40 +01:00
|
|
|
absl::SetStderrThreshold(absl::LogSeverityAtLeast::kInfo);
|
2022-02-25 09:47:52 +01:00
|
|
|
InitGoogle(argv[0], &argc, &argv, true);
|
2021-01-14 10:48:19 +01:00
|
|
|
|
2018-11-24 19:34:08 +01:00
|
|
|
int min = 1;
|
|
|
|
|
int max = 10;
|
|
|
|
|
|
2020-10-21 00:21:54 +02:00
|
|
|
if (absl::GetFlag(FLAGS_minsize) != 0) {
|
|
|
|
|
min = absl::GetFlag(FLAGS_minsize);
|
2018-11-24 19:34:08 +01:00
|
|
|
|
2020-10-21 00:21:54 +02:00
|
|
|
if (absl::GetFlag(FLAGS_maxsize) != 0) {
|
|
|
|
|
max = absl::GetFlag(FLAGS_maxsize);
|
2018-11-24 19:34:08 +01:00
|
|
|
} else {
|
|
|
|
|
max = min;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
for (int size = min; size <= max; ++size) {
|
|
|
|
|
LOG(INFO) << "Computing Costas Array for dim = " << size;
|
2020-10-21 00:21:54 +02:00
|
|
|
if (absl::GetFlag(FLAGS_model) == 1) {
|
2018-11-24 19:34:08 +01:00
|
|
|
operations_research::sat::CostasHard(size);
|
2020-10-21 00:21:54 +02:00
|
|
|
} else if (absl::GetFlag(FLAGS_model) == 2) {
|
2018-11-24 19:34:08 +01:00
|
|
|
operations_research::sat::CostasBool(size);
|
2020-10-21 00:21:54 +02:00
|
|
|
} else if (absl::GetFlag(FLAGS_model) == 3) {
|
2018-11-24 19:34:08 +01:00
|
|
|
operations_research::sat::CostasBoolSoft(size);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
return EXIT_SUCCESS;
|
|
|
|
|
}
|