#include <cstdint>
#include <cstdlib>
#include <numeric>
#include <string>
#include <vector>
#include "absl/base/log_severity.h"
#include "absl/flags/flag.h"
#include "absl/log/check.h"
#include "absl/log/globals.h"
#include "absl/log/log.h"
#include "absl/strings/str_format.h"
#include "ortools/base/init_google.h"
#include "ortools/sat/cp_model.h"
ABSL_FLAG(int, size, 50, "Size of the problem.");
ABSL_FLAG(std::string, params, "log_search_progress:true,num_search_workers:8",
"Sat parameters.");
namespace operations_research {
namespace sat {
void MagicSequence(int size) {
CHECK_GE(size, 1);
CpModelBuilder cp_model;
std::vector<std::vector<BoolVar>> var_domains(size);
for (int i = 0; i < size; ++i) {
for (int j = 0; j < size; ++j) {
var_domains[i].push_back(cp_model.NewBoolVar());
}
}
for (int i = 0; i < size; ++i) {
cp_model.AddEquality(LinearExpr::Sum(var_domains[i]), 1);
}
std::vector<int64_t> values(size);
std::iota(values.begin(), values.end(), 0); std::vector<BoolVar> vars_equal_to_j;
for (int j = 0; j < size; ++j) {
vars_equal_to_j.clear();
for (int i = 0; i < size; ++i) {
vars_equal_to_j.push_back(var_domains[i][j]);
}
cp_model.AddEquality(LinearExpr::WeightedSum(var_domains[j], values),
LinearExpr::Sum(vars_equal_to_j));
}
const CpSolverResponse response =
SolveWithParameters(cp_model.Build(), absl::GetFlag(FLAGS_params));
if (response.status() == CpSolverStatus::OPTIMAL ||
response.status() == CpSolverStatus::FEASIBLE) {
std::string output = "[";
for (int i = 0; i < size; ++i) {
if (i != 0) {
output.append(", ");
}
for (int j = 0; j < size; ++j) {
if (SolutionBooleanValue(response, var_domains[i][j])) {
absl::StrAppendFormat(&output, "%d", j);
break;
}
}
}
output.append("]");
LOG(INFO) << "Solution = " << output;
}
}
} }
int main(int argc, char** argv) {
absl::SetStderrThreshold(absl::LogSeverityAtLeast::kInfo);
InitGoogle(argv[0], &argc, &argv, true);
operations_research::sat::MagicSequence(absl::GetFlag(FLAGS_size));
return EXIT_SUCCESS;
}