WIP: LP Justifications #72
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Are you using soplex still? It's causing build issues... |
|
Got rid of soplex - will see if that helps |
|
I've had to hack HiGHS to get it to build for me, because I don't understand CMake. I'm fairly sure I know what the problem is, though (or at least one of the problems). Looks like you're storing a constraint state of an |
|
OK so this is enough hackery to get among_TEST to build on my machine and to run cleanly, although it'll fail to verify some proofs: |
|
Basically, your problem is that |
|
I've turned Zoom on in case you want to discuss |
|
Looks like commenting things out works, but a simple conversion to a shared_ptr isn't enough. I'm a bit confused by the last and current logic, as well: do you actually need two variables here? Anyway, this seems to work, at least until it encounters a failing test: diff --git a/gcs/innards/proofs/lp_justifier.cc b/gcs/innards/proofs/lp_justifier.cc
index 9f8aa42..2a1ab47 100644
--- a/gcs/innards/proofs/lp_justifier.cc
+++ b/gcs/innards/proofs/lp_justifier.cc
@@ -9,18 +9,21 @@
#include <sstream>
// TODO: Remove later
+#include <iostream>
#include <iomanip>
//
using std::iota;
using std::make_optional;
using std::make_pair;
+using std::make_shared;
using std::map;
using std::max;
using std::move;
using std::nullopt;
using std::optional;
using std::pair;
+using std::shared_ptr;
using std::stringstream;
using std::to_string;
using std::tuple;
@@ -32,10 +35,6 @@ using namespace gcs::lp_innards;
namespace
{
- // Dirty GPT code
-#include "Highs.h" // Include the HiGHS header
-#include <iostream>
-
void printHighsLP(const HighsLp & lp)
{
// Print start_ initializer
@@ -246,7 +245,7 @@ struct LPJustifier::Imp
auto pass_and_solve_model(const WeightedPseudoBooleanLessEqual & inference,
HighsModel & restricted_model, vector<double> rhs_updated, vector<long> new_row_num, vector<long> old_row_num,
- optional<HighsBasis> & optional_last_basis, optional<HighsBasis> & optional_current_basis) -> const HighsSolution
+ shared_ptr<HighsBasis> & optional_basis) -> const HighsSolution
{
HighsStatus return_status;
bool inferring_contradiction = inference.lhs.terms.empty() && inference.rhs <= -1_i;
@@ -297,24 +296,24 @@ struct LPJustifier::Imp
const HighsLp & lp = this->highs.getLp();
this->highs.setBasis();
- if (optional_last_basis) {
+ if (optional_basis) {
// Use the basis
- // this->highs.setBasis(*optional_current_basis);
+ this->highs.setBasis(*optional_basis);
}
// Now solve the model
return_status = this->highs.run();
// Save the basis for next time
- if (optional_last_basis) {
- auto new_basis = this->highs.getBasis();
- for (unsigned int row = 0; row < new_basis.row_status.size(); ++row) {
- optional_last_basis->row_status[old_row_num[row]] = new_basis.row_status[row];
- }
- }
- else {
- optional_last_basis = highs.getBasis();
- }
+// if (optional_last_basis) {
+// auto new_basis = this->highs.getBasis();
+// for (unsigned int row = 0; row < new_basis.row_status.size(); ++row) {
+// optional_last_basis->row_status[old_row_num[row]] = new_basis.row_status[row];
+// }
+// }
+// else {
+ optional_basis = make_shared<HighsBasis>(highs.getBasis());
+// }
// Check it worked
const HighsModelStatus & model_status = this->highs.getModelStatus();
@@ -481,7 +480,7 @@ void LPJustifier::initialise_with_vars(State & state, vector<IntegerVariableID>
_imp->model.lp_.a_matrix_.value_ = value;
_imp->model.lp_.setMatrixDimensions();
- optional<HighsBasis> optional_last_basis = nullopt;
+ shared_ptr<HighsBasis> optional_last_basis = nullptr;
_imp->last_basis_handle = state.add_constraint_state(optional_last_basis);
}
@@ -530,8 +529,7 @@ auto LPJustifier::compute_justification(const State & state, ProofLogger & logge
auto restricted_model = _imp->model;
auto rhs_updated = _imp->constraints_rhs;
- auto & optional_last_basis = any_cast<optional<HighsBasis> &>(state.get_constraint_state(_imp->last_basis_handle));
- optional<HighsBasis> optional_current_basis = optional_last_basis ? make_optional(HighsBasis{}) : nullopt;
+ auto & optional_basis = any_cast<shared_ptr<HighsBasis> &>(state.get_constraint_state(_imp->last_basis_handle));
vector<HighsInt> mask;
vector<long> new_row_num(restricted_model.lp_.num_row_, 0);
@@ -563,13 +561,11 @@ auto LPJustifier::compute_justification(const State & state, ProofLogger & logge
create(to_delete, mask.data(), restricted_model.lp_.num_row_);
restricted_model.lp_.deleteRows(to_delete);
- if (optional_current_basis) {
+ if (optional_basis) {
// Set the current basis based on the last basis, excluding deleted rows
- optional_current_basis->col_status = optional_last_basis->col_status;
- optional_current_basis->row_status = optional_last_basis->row_status;
- for (unsigned int row = 0; row < optional_current_basis->row_status.size(); ++row) {
+ for (unsigned int row = 0; row < optional_basis->row_status.size(); ++row) {
if (mask[row] == 1)
- optional_current_basis->row_status[row] = HighsBasisStatus::kNonbasic;
+ optional_basis->row_status[row] = HighsBasisStatus::kNonbasic;
}
}
@@ -584,14 +580,14 @@ auto LPJustifier::compute_justification(const State & state, ProofLogger & logge
HighsSolution solution_already;
// Compute solution already, even if the justification isn't called
if (compute_bounds)
- solution_already = _imp->pass_and_solve_model(inference, restricted_model, rhs_updated, new_row_num, old_row_num, optional_last_basis, optional_current_basis);
+ solution_already = _imp->pass_and_solve_model(inference, restricted_model, rhs_updated, new_row_num, old_row_num, optional_basis);
- return [&state = state, &logger, inference, &imp = _imp, &optional_last_basis, &optional_current_basis,
+ return [&state = state, &logger, inference, &imp = _imp, &optional_basis,
restricted_model = move(restricted_model), rhs_updated, new_row_num, old_row_num, compute_bounds, solution_already = move(solution_already)](const Reason &) {
HighsSolution solution;
HighsModel restr_model = move(restricted_model);
if (! compute_bounds)
- solution = imp->pass_and_solve_model(inference, restr_model, rhs_updated, new_row_num, old_row_num, optional_last_basis, optional_current_basis);
+ solution = imp->pass_and_solve_model(inference, restr_model, rhs_updated, new_row_num, old_row_num, optional_basis);
else
solution = solution_already;
|
|
Although the "restore on backtrack" logic for that is probably wrong, so actually no not that, and I guess you do need two variables. Still, the |
|
Hrm this is interesting. If I do the following instead: diff --git a/gcs/innards/proofs/lp_justifier.cc b/gcs/innards/proofs/lp_justifier.cc
index 9f8aa42..90048a9 100644
--- a/gcs/innards/proofs/lp_justifier.cc
+++ b/gcs/innards/proofs/lp_justifier.cc
@@ -9,18 +9,21 @@
#include <sstream>
// TODO: Remove later
+#include <iostream>
#include <iomanip>
//
using std::iota;
using std::make_optional;
using std::make_pair;
+using std::make_shared;
using std::map;
using std::max;
using std::move;
using std::nullopt;
using std::optional;
using std::pair;
+using std::shared_ptr;
using std::stringstream;
using std::to_string;
using std::tuple;
@@ -32,10 +35,6 @@ using namespace gcs::lp_innards;
namespace
{
- // Dirty GPT code
-#include "Highs.h" // Include the HiGHS header
-#include <iostream>
-
void printHighsLP(const HighsLp & lp)
{
// Print start_ initializer
@@ -309,7 +308,7 @@ struct LPJustifier::Imp
if (optional_last_basis) {
auto new_basis = this->highs.getBasis();
for (unsigned int row = 0; row < new_basis.row_status.size(); ++row) {
- optional_last_basis->row_status[old_row_num[row]] = new_basis.row_status[row];
+ optional_last_basis->row_status.at(old_row_num.at(row)) = new_basis.row_status.at(row);
}
}
else {
@@ -481,7 +480,7 @@ void LPJustifier::initialise_with_vars(State & state, vector<IntegerVariableID>
_imp->model.lp_.a_matrix_.value_ = value;
_imp->model.lp_.setMatrixDimensions();
- optional<HighsBasis> optional_last_basis = nullopt;
+ ConstraintState optional_last_basis = optional<HighsBasis>{};
_imp->last_basis_handle = state.add_constraint_state(optional_last_basis);
}
@@ -530,7 +529,7 @@ auto LPJustifier::compute_justification(const State & state, ProofLogger & logge
auto restricted_model = _imp->model;
auto rhs_updated = _imp->constraints_rhs;
- auto & optional_last_basis = any_cast<optional<HighsBasis> &>(state.get_constraint_state(_imp->last_basis_handle));
+ optional<HighsBasis> & optional_last_basis = any_cast<optional<HighsBasis> &>(state.get_constraint_state(_imp->last_basis_handle));
optional<HighsBasis> optional_current_basis = optional_last_basis ? make_optional(HighsBasis{}) : nullopt;
vector<HighsInt> mask;then I get which suggests your basis has changed size maybe? |
|
Hmm, right. I think what I'll do is take out the basis stuff for now and make sure everything is working as it should, see if I can do GCC and among with passing proofs. The paper is probably at least submittable with a slow implementation, but not a broken one. If I have extra time I'll see if I can re-add the hot starts. |
|
Sounds sensible to me. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
At the moment
among_test.ccis catastrophically broken and really can't figure out what I'm screwing up