Shortest path constraint by waneck · Pull Request #9 · proletariatgames/vertexy

waneck · 2022-06-16T19:38:42Z

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.

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

waneck · 2022-06-16T19:43:49Z

+		if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask) || reachabilitySource != m_reachabilitySources.end())
+		{
+			vector<int> path;
+			// so this is a bit confusing, bear with me:


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

waneck · 2022-06-16T19:50:58Z

+	m_queuedVertexChanges.insert(vertexIndex);
+	auto reachability = determineValidity(m_edgeChangeDb, vertexIndex);
+
+	// TODO understand why uncommenting both of these make everything run much, much slower


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)

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.

waneck · 2022-06-16T19:54:49Z

+		return;
+	}
+
+	m_processingVertices = true;


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

waneck · 2022-06-16T19:58:35Z

+		// Reachable from a possible source
+		DefinitelyUnreachable,
+		// Unreachable from any possible source
+		DefinitelyInvalid,


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

waneck · 2022-06-16T19:59:08Z

 	}

-	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; }


That was a bug that can happen if lastHistoryIdx ends up being negative because we rewound everything

waneck · 2022-06-16T19:59:34Z

+namespace Vertexy
+{
+template<typename InElementType>
+struct TTimestampAndValue


I just realized I didn't apply all the changes you commented, Ogles. I'll do that now

waneck · 2022-06-16T19:59:53Z

-	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);


Whoops I need to uncomment all of these

waneck · 2022-06-16T20:01:13Z

 			if (printVerbose && MAZE_REFRESH_RATE > 0 && (solver.getStats().stepCount % MAZE_REFRESH_RATE) == 0)
 			{
 				print(stepDatas[0], stepEdgeDatas[0], solver);
+				VERTEXY_LOG("step door data");


I forgot to delete these. Will do

dogles · 2022-06-17T12:55:23Z

+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?");


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.

dogles · 2022-06-17T12:58:42Z

+static constexpr int CLOSED_EDGE_FLOW = 1;
+static constexpr bool USE_RAMAL_REPS_BATCHING = true;
+
+ITopologySearchConstraint::ITopologySearchConstraint(


Can you rename this to TopologyConnectionConstraint or something like that? (At least get rid of the I since it's not an interface)

dogles · 2022-06-17T13:01:55Z

+		hash_map<int, TBacktrackableValue<SolverTimestamp>>* validTimestamp;
+		if (found == m_lastValidTimestamp.end())
+		{
+			m_lastValidTimestamp[toCommitDest.first] = hash_map<int, TBacktrackableValue<SolverTimestamp>>();


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.

dogles · 2022-06-17T13:10:19Z

+	m_queuedVertexChanges.insert(vertexIndex);
+	auto reachability = determineValidity(m_edgeChangeDb, vertexIndex);
+
+	// TODO understand why uncommenting both of these make everything run much, much slower


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.

dogles · 2022-06-17T13:11:24Z

+	{
+		// vertexIndex became unreachable in the max graph
+		VarID var = m_sourceGraphData->get(vertexIndex);
+		//sanityCheckUnreachable(db, vertexIndex);


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).

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

Oh man maybe that's why we are getting so many backtracks!?

I'll make some tests

dogles · 2022-06-17T14:39:56Z

+			//	vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector<int>{cell_Doors[step - 1]})}
+			//);
+
+			solver.makeGraphConstraint<IffConstraint>(grid,


These two branches are equivalent

dogles · 2022-06-17T14:44:04Z

+			vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector<int>{cell_Doors[step - 1]})}
+		);
+
+		// if stepDoor != reachable, tile can't be a door


"tile can't be a key"

dogles · 2022-06-17T14:46:47Z

+
 		// If we don't have all the keys at this step...
 		if (step < NUM_KEYS)
 		{


I believe the constraint after this line is redundant if TEST_SHORTEST_PATH is on

dogles · 2022-06-17T14:47:16Z

+		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);


can move this line out of the branch

dogles · 2022-06-17T14:58:37Z

+		}
+		else if (src.maxReachability->isReachable(vertex))
+		{
+			return EValidityDetermination::PossiblyValid;


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.

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

prolecengelhard and others added 18 commits April 12, 2022 13:38

creating the base class

9a72fb5

and adapting ReachabilityConstraint to it

redid it with virtual functions

6e73ba3

I think this is better OOP than having a "which derived class am I" variable in the base class.

removed redundant function

537e7ac

implemented isValidDistance

5f34fe1

added db to callback

cb43719

adding db to addSource

077bd4b

moved the explainers down to the ReachabilityConstraint

460175f

about to attempt to restructure the maze

b96a1de

working on greater than and less than

84c01a8

Merge branch 'main' into shortest-path-constraint

0364754

still trying to figure out the constraints

61add3f

made a simpler test and renamed a function

1073622

Fixes so that the ReachabilityConstraint works again

388e7c6

Merge branch 'main' into shortest-path-constraint-v2

4145f24

Introduce the split between Valid vs Reachable

07f0414

This will make it easy to identify when we should call the reachability explainer, and when we should call the new validity explainer

Working shortest path constraint

4944159

The explainer is still the default explainer at this point

Initial explainInvalid implementation

092f5c0

Working greater than explainer

fdc4d2a

Also general code cleanup

waneck requested review from ViolinLloyd and dogles June 16, 2022 19:38

waneck commented Jun 16, 2022

View reviewed changes

dogles reviewed Jun 17, 2022

View reviewed changes

PR feedback, part one

80ae90e

Uh oh!

Conversation

waneck commented Jun 16, 2022

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants