sat_killers.h

size_t CalcScore(const Problem& p, const std::vector<size_t>& hint) {
  MPSolver solver("solving_all_cases", absl::GetFlag(FLAGS_scan_mip_solver_type));
  const double infinity = solver.infinity();
  std::vector<MPVariable*> books_vars;
  std::vector<size_t> books_vars_hints(15000);
  std::vector<MPVariable*> clauses_vars;
  for (size_t i = 0; i < 15000; ++i) {
    books_vars.push_back(solver.MakeBoolVar(absl::StrCat("x_", i)));
  }
  std::vector<std::pair<const MPVariable*, double>> hinting;
  for (const size_t ind : hint) {
    // Top variable is a true, bottom is false.
    if (ind % 2 == 1) {
      books_vars_hints[ind / 2] = 0;
      hinting.emplace_back(books_vars[ind / 2], 0.0);
    } else {
      books_vars_hints[ind / 2] = 1;
      hinting.emplace_back(books_vars[ind / 2], 1.0);
    }
  }
  for (size_t i = 0; i < 63600; ++i) {
    clauses_vars.push_back(solver.MakeBoolVar(absl::StrCat("y_", i)));
  }
  size_t iter = 0;
  // Print max 3SAT. var is a library for the book.
  for (const auto& [book, var] : p.counters) {
    int num_neg = 0;
    for (const auto ind : var) {
      if (ind % 2 == 1) {
        ++num_neg;
      }
    }
    MPConstraint* const constraint = solver.MakeRowConstraint(-infinity, num_neg, absl::StrCat("c_", iter));
    constraint->SetCoefficient(clauses_vars[iter], 1.0);
    int value = 0;
    for (const auto ind : var) {
      if (ind % 2 == 1) {
        if (books_vars_hints[ind / 2] == 1) {
          value += 1;
        }
        constraint->SetCoefficient(books_vars[ind / 2], 1.0);
      } else {
        if (books_vars_hints[ind / 2] == 1) {
          value -= 1;
        }
        constraint->SetCoefficient(books_vars[ind / 2], -1.0);
      }
    }
    if (value + 1 <= num_neg) {
      hinting.emplace_back(clauses_vars[iter], 1.0);
    } else {
      hinting.emplace_back(clauses_vars[iter], 0.0);
    }
    ++iter;
  }

  solver.SetHint(hinting);
  MPObjective* const objective = solver.MutableObjective();
  for (size_t i = 0; i < 63600; ++i) {
    objective->SetCoefficient(clauses_vars[i], 1.0);
  }
  objective->SetMaximization();
  solver.SuppressOutput();
  solver.SetTimeLimit(absl::GetFlag(FLAGS_lp_timeout));
  auto start = absl::Now();
  const MPSolver::ResultStatus result_status = solver.Solve();
  auto finish = absl::Now();
  std::cerr << "Objective " << static_cast<size_t>(objective->Value()) << std::endl;
  std::cerr << "Processed " << finish - start << std::endl;
  if (result_status != MPSolver::OPTIMAL) {
    std::cerr << "The problem does not have an optimal solution!" << std::endl;
  } else {
    std::cerr << "IT IS OPTIMAL, WOW!" << std::endl;
  }
  std::vector<size_t> v;
  for (size_t i = 0; i < 15000; ++i) {
    if (books_vars[i]->solution_value() == 1.0) {
      v.push_back(i * 2);
    } else {
      v.push_back(i * 2 + 1);
    }
  }
  std::vector<std::vector<bool>> mask;
  for (const size_t ind : v) {
    auto& back = mask.emplace_back();
    for (size_t j = 0; j < p.libraries[ind].books_indices.size(); ++j) {
      back.push_back(true);
    }
  }
  PrintScoreAndResult(p, mask);
}