Do not copy tableau state during push and pop #532
Conversation
wu-haoze
commented
Feb 20, 2022
•
wu-haoze
commented
- Add assertions in SmtCore that all case splits applying during push and pop contain only bound updates.
- Due to this assertion, copying of the tableau state is no longer necessary. In particular, when backtracking, we just need to restore the variable bounds from the previous level and the other tableau state do not need to change.
- Copying of the entire tableau state is used only for precision restoration.
- Remove the VariableWatcher::notifyVariableValue() function, but instead get the variable assignment directly from the Tableau.
| for ( unsigned i = 0; i < _n - _m; ++i ) | ||
| { | ||
| unsigned variable = _nonBasicIndexToVariable[i]; | ||
| updateVariableToComplyWithLowerBoundUpdate( variable, |
There was a problem hiding this comment.
@guykatzz If I don't do this update, the Tableau invariant can be broken (some non-basic variable will go out of bound). Are there better solution than this?
The alternative would be to not call updateVariableToComplyWithLowerBoundUpdate() when _boundsValid is false in the "tightenLower/UpperBounds methods". But doing that seems to result in invariant being broken elsewhere.
I also tried throw InfeasibleQueryException() in those tightenbounds method once the bounds become invalid. But that is also problematic, because now this exception could be thrown in "popSplit()" method..
There was a problem hiding this comment.
I guess an alternative would be to store the variables' assignment as part of the stored state? And then have another invariant that says that a stored state is valid, as far as the NB assignments are concerned?
But why do you want to change this? I don't think it's that expensive, performance wise
There was a problem hiding this comment.
Ah ok. I think I'll keep the current solution.
src/engine/DnCWorker.cpp
Outdated
| @@ -49,7 +50,8 @@ DnCWorker::DnCWorker( WorkerQueue *workload, std::shared_ptr<IEngine> engine, | |||
|
|
|||
| // Obtain the current state of the engine | |||
| _initialState = std::make_shared<EngineState>(); | |||
| _engine->storeState( *_initialState, true ); | |||
| _engine->storeState( *_initialState, | |||
| TableauStateStorageLevel::STORE_ALL_TABLEAU_STATE ); | |||
| { | ||
| constraint->registerTableau( _tableau ); | ||
| } | ||
|
|
| return ( _gurobi == nullptr ) ? | ||
| _assignment.exists( variable ) | ||
| : _gurobi->existsAssignment( Stringf( "x%u", variable ) ); | ||
| if ( _gurobi == nullptr && _tableau != nullptr ) |
There was a problem hiding this comment.
This is intended to give preference to Gurobi, right? So lets reorder:
if ( gurobi exists )
return gurobi value;
if ( tableu exists )
return tableu value
fail
There was a problem hiding this comment.
Done. Yeah this reads much better..
| for ( unsigned i = 0; i < _n - _m; ++i ) | ||
| { | ||
| unsigned variable = _nonBasicIndexToVariable[i]; | ||
| updateVariableToComplyWithLowerBoundUpdate( variable, |
There was a problem hiding this comment.
I guess an alternative would be to store the variables' assignment as part of the stored state? And then have another invariant that says that a stored state is valid, as far as the NB assignments are concerned?
But why do you want to change this? I don't think it's that expensive, performance wise
