Skip to content

Instantly share code, notes, and snippets.

@danlark1

danlark1/sat_killers.h

Last active Mar 13, 2020
Embed
What would you like to do?
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);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.