-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Shortest path constraint #9
base: main
Are you sure you want to change the base?
Conversation
and adapting ReachabilityConstraint to it
I think this is better OOP than having a "which derived class am I" variable in the base class.
This will make it easy to identify when we should call the reachability explainer, and when we should call the new validity explainer
The explainer is still the default explainer at this point
Also general code cleanup
if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask) || reachabilitySource != m_reachabilitySources.end()) | ||
{ | ||
vector<int> path; | ||
// so this is a bit confusing, bear with me: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hopefully the comments below make it easier to understand what's going on in here. Perhaps it would be more clear if I made two separate versions of this function, one for when it's a GreaterThan op, and another for when it's a LessThan
m_queuedVertexChanges.insert(vertexIndex); | ||
auto reachability = determineValidity(m_edgeChangeDb, vertexIndex); | ||
|
||
// TODO understand why uncommenting both of these make everything run much, much slower |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, so this is my biggest pet peeve with this code.
There are two separate issues here:
- If I try to constrain DefinitelyValid vertices as requireValid (as we do on the ReachabilityConstraint), the performance drops considerably, and sometimes it returns UNSAT. If I instead only constrain if it can be valid (so we avoid the edgeChangeFailure case), it won't return UNSAT but it runs much, much slowly
- The solver will keep constraining these variables, which doesn't make much sense in this case, since we are keeping it as mostly a representation of what is valid and is not. The code below, on the PossiblyValid part, is definitely wrong, but what I was trying to achieve was to ensure that if a vertex is possibly valid, it should be possible to both be invalid AND valid, so it can't be contrained. So what I wanted was some kind of "unconstrain" variable. I guess it doesn't make sense to allow that, and I think I understand why (the whole point of the solver being of constraining variables vs unconstraining them). Anyway, I think that this issue is what is causing the above issue, and what makes sometimes it still return UNSAT (I've only seen it happen if I constrain greater than to a big number in the maze, like 20)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
re: your second point, my expectation is that for "possibly valid" you wouldn't constrain the variable at all. It'll either get constrained later: either due to edges and/or sources becoming known, some other constraint, or the solver making a random decision on it. All three are "fine" in the sense that if that leads to a conflict, the conflict analysis will allow the solver to learn whether the vertex needs to actually be (in)valid validity.
return; | ||
} | ||
|
||
m_processingVertices = true; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We are using this variable as a way to not set values in the timestamps to commit at this point. That's because we are running the onVertexChanged WHILE we are changing all the Ramal graphs. At that point, since determineValidity
will go through all sources, it might send bad data to commit - ie data that will later become invalidated once we change that ramal graph. So I added m_queuedVertexChanges
, and wanted to move this code out of here and later when we have a consistent view. However, when doing that, the code ran much, much slowly - it turns out we benefit a lot from detecting the edge change failures before updating all graphs. So we are still running this here, and then later on, we run determineValidity
once again on all queuedVertexChanges
// Reachable from a possible source | ||
DefinitelyUnreachable, | ||
// Unreachable from any possible source | ||
DefinitelyInvalid, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So now we have this differentiation between unreachable and invalid. This helps us know what explainer to run - if a single value is invalid, we run the invalid explainer - otherwise, we run the reachability one
@@ -99,7 +99,7 @@ class BacktrackingDigraphTopology : public TDigraphTopologyBase<BacktrackingDigr | |||
} | |||
} | |||
|
|||
inline bool isPartiallyRewound() const { return m_lastHistoryIdx < m_history.size() - 1; } | |||
inline bool isPartiallyRewound() const { return (m_lastHistoryIdx < 0 && m_history.size() > 0) || m_lastHistoryIdx < m_history.size() - 1; } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That was a bug that can happen if lastHistoryIdx ends up being negative because we rewound everything
namespace Vertexy | ||
{ | ||
template<typename InElementType> | ||
struct TTimestampAndValue |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I just realized I didn't apply all the changes you commented, Ogles. I'll do that now
Suite.AddTest("NQueens-AllDifferent", []() { return NQueensSolvers::solveUsingAllDifferent(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); | ||
Suite.AddTest("NQueens-Table", []() { return NQueensSolvers::solveUsingTable(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); | ||
Suite.AddTest("NQueens-Graph", []() { return NQueensSolvers::solveUsingGraph(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); | ||
//Suite.AddTest("ValueBitset", test_ValueBitset); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Whoops I need to uncomment all of these
@@ -474,6 +623,17 @@ int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printV | |||
if (printVerbose && MAZE_REFRESH_RATE > 0 && (solver.getStats().stepCount % MAZE_REFRESH_RATE) == 0) | |||
{ | |||
print(stepDatas[0], stepEdgeDatas[0], solver); | |||
VERTEXY_LOG("step door data"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I forgot to delete these. Will do
vector<Literal> Vertexy::ShortestPathConstraint::explainInvalid(const NarrowingExplanationParams& params) | ||
{ | ||
// if we are here, it means that the path was reachable, but we marked it as invalid because of the distance constraint | ||
vxy_assert_msg(m_variableToSourceVertexIndex.find(params.propagatedVariable) != m_variableToSourceVertexIndex.end(), "Not a vertex variable?"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would recommend making this a vxy_sanity_msg
- I tend to put the expensive asserts (involving search) there to keep the Development build semi-fast.
static constexpr int CLOSED_EDGE_FLOW = 1; | ||
static constexpr bool USE_RAMAL_REPS_BATCHING = true; | ||
|
||
ITopologySearchConstraint::ITopologySearchConstraint( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you rename this to TopologyConnectionConstraint
or something like that? (At least get rid of the I
since it's not an interface)
hash_map<int, TBacktrackableValue<SolverTimestamp>>* validTimestamp; | ||
if (found == m_lastValidTimestamp.end()) | ||
{ | ||
m_lastValidTimestamp[toCommitDest.first] = hash_map<int, TBacktrackableValue<SolverTimestamp>>(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Slightly more efficient pattern: validTimestmap = m_lastValidTimestamp.insert({toCommitDest.first, {}}).first;
insert()
returns a pair<iterator, bool>
. The iterator points to the element, and the bool indicates whether the key is new or not.
m_queuedVertexChanges.insert(vertexIndex); | ||
auto reachability = determineValidity(m_edgeChangeDb, vertexIndex); | ||
|
||
// TODO understand why uncommenting both of these make everything run much, much slower |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
re: your second point, my expectation is that for "possibly valid" you wouldn't constrain the variable at all. It'll either get constrained later: either due to edges and/or sources becoming known, some other constraint, or the solver making a random decision on it. All three are "fine" in the sense that if that leads to a conflict, the conflict analysis will allow the solver to learn whether the vertex needs to actually be (in)valid validity.
{ | ||
// vertexIndex became unreachable in the max graph | ||
VarID var = m_sourceGraphData->get(vertexIndex); | ||
//sanityCheckUnreachable(db, vertexIndex); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm guessing these are commented out because the sanityCheck only checks reachability. Might be worth adding one that checks reachability+distance, just to ensure nothing is getting out of sync (I found these asserts helpful in original reachability constraint).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In this code in particular, adding a sanity check will break very frequently because we are still processing the RamalReps, so they aren't all updated at this point. I'll move that to the code we do after all of them are updated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh man maybe that's why we are getting so many backtracks!?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll make some tests
// vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector<int>{cell_Doors[step - 1]})} | ||
//); | ||
|
||
solver.makeGraphConstraint<IffConstraint>(grid, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These two branches are equivalent
vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector<int>{cell_Doors[step - 1]})} | ||
); | ||
|
||
// if stepDoor != reachable, tile can't be a door |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"tile can't be a key"
GraphRelationClause(selfTile, cell_Wall) | ||
); | ||
} | ||
|
||
// If we don't have all the keys at this step... | ||
if (step < NUM_KEYS) | ||
{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I believe the constraint after this line is redundant if TEST_SHORTEST_PATH is on
if (TEST_SHORTEST_PATH) | ||
{ | ||
solver.makeConstraint<ShortestPathConstraint>(stepDoorData, step_Origin, step_Reachable, stepEdgeData, edge_Solid, EConstraintOperator::LessThan, shortestPathDistance); | ||
solver.makeConstraint<ReachabilityConstraint>(stepData, step_Origin, step_Reachable, stepEdgeData, edge_Solid); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
can move this line out of the branch
} | ||
else if (src.maxReachability->isReachable(vertex)) | ||
{ | ||
return EValidityDetermination::PossiblyValid; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was going to say that we could return DefinitelyValid here if the maxReachability distance is > requiredDistance and the source is definite, since maxReachability distance will only increase (since edges only get removed from it).
But I guess that's not correct, because edges might get removed that make this totally unreachable.
This makes me consider whether we should treat unreachable in this constraint as "infinitely far away". My reasoning is that 1) that might sometimes be desired behavior, 2) it will be able to more tightly constrain variables that way, and 3) you can always add an additional ReachabilityConstraint to ensure that it's both reachable AND > distance.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That makes sense. It would only help the greater than case, and I can't think of a case where unreachable is what we want, though
Please consider this mostly a proof-of-concept for now. The code is working, but I have some questions, which I will detail in the comments below.
There are also a couple of optimization opportunities that are called out in the code. Also note that because the code moved around so much, I tried recreating the git history in a way that you can more easily compare between what was changed in the original reachability constraint.