Shortest path constraint

vertexy/src/private/variable/SolverVariableDatabase.cpp

@@ -9,6 +9,50 @@
 
 using namespace Vertexy;
 
+//
+// Default explanation function for a violated constraint. This will return a true explanation, but is not necessarily
+// the smallest explanation possible, especially for constraints involving more than 2 variables.
+//
+vector<Literal> IVariableDatabase::defaultExplainer(const NarrowingExplanationParams& params)
+{
+	// Find all dependent variables for this constraint that were previously narrowed, and add their (inverted) value to the list.
+	// The clause will look like:
+	// (Arg1 != Arg1Values OR Arg2 != Arg2Values OR [...] OR PropagatedVariable == PropagatedValues)
+	const vector<VarID>& constraintVars = params.solver->getVariablesForConstraint(params.constraint);
+	vector<Literal> clauses;
+	clauses.reserve(constraintVars.size());
+
+	bool foundPropagated = false;
+	for (int i = 0; i < constraintVars.size(); ++i)
+	{
+		VarID arg = constraintVars[i];
+		clauses.push_back(Literal(arg, params.database->getPotentialValues(arg)));
+		clauses.back().values.invert();
+
+		if (arg == params.propagatedVariable)
+		{
+			foundPropagated = true;
+			clauses.back().values.pad(params.propagatedValues.size(), false);
+			clauses.back().values.include(params.propagatedValues);
+		}
+	}
+
+	vxy_assert(foundPropagated);
+	return clauses;
+}
+
+int IVariableDatabase::getMinimumPossibleDomainValue(VarID varID) const
+{
+	vxy_assert(varID.isValid());
+	return getSolver()->getDomain(varID).getValueForIndex(getMinimumPossibleValue(varID));
+}
+
+int IVariableDatabase::getMaximumPossibleDomainValue(VarID varID) const
+{
+	vxy_assert(varID.isValid());
+	return getSolver()->getDomain(varID).getValueForIndex(getMaximumPossibleValue(varID));
+}
+
 SolverVariableDatabase::SolverVariableDatabase(ConstraintSolver* inSolver)
 	: IVariableDatabase()
 	, m_solver(inSolver)

vertexy/src/public/ConstraintTypes.h

@@ -39,7 +39,8 @@ enum class EConstraintType : uint8_t
 	Offset,
 	Table,
 	Reachability,
-	Sum
+	Sum,
+	ShortestPath
 };
 
 // If set, VariableDBs will cache the state of each variable (solved/unsolved/contradiction), only updating when

vertexy/src/public/constraints/ReachabilityConstraint.h

@@ -1,6 +1,7 @@
 // Copyright Proletariat, Inc. All Rights Reserved.
 #pragma once
 #include "ConstraintTypes.h"
+#include "TopologySearchConstraint.h"
 #include "IBacktrackingSolverConstraint.h"
 #include "IConstraint.h"
 #include "SignedClause.h"
@@ -22,7 +23,7 @@ namespace Vertexy
  *  Any variable that is definitely one of SourceValues is considered a reachability source.
  *  Any variable that is definitely on of NeedReachableValues is considered a destination that must remain reachable from AT LEAST one source.
  */
-class ReachabilityConstraint : public IBacktrackingSolverConstraint
+class ReachabilityConstraint : public ITopologySearchConstraint
 {
 public:
 	ReachabilityConstraint(const ConstraintFactoryParams& params,
@@ -52,162 +53,14 @@ class ReachabilityConstraint : public IBacktrackingSolverConstraint
 	using Factory = ReachabilityFactory;
 
 	virtual EConstraintType getConstraintType() const override { return EConstraintType::Reachability; }
-	virtual vector<VarID> getConstrainingVariables() const override;
-	virtual bool initialize(IVariableDatabase* db) override;
-	virtual void reset(IVariableDatabase* db) override;
-	virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override;
-	virtual bool checkConflicting(IVariableDatabase* db) const override;
-	virtual bool propagate(IVariableDatabase* db) override;
-	virtual void backtrack(const IVariableDatabase* db, SolverDecisionLevel level) override;
-	virtual bool getGraphRelations(const vector<Literal>& literals, ConstraintGraphRelationInfo& outRelations) const override;
 
 protected:
-	vector<Literal> explainNoReachability(const NarrowingExplanationParams& params) const;
-	vector<Literal> explainRequiredSource(const NarrowingExplanationParams& params, VarID removedSource = VarID::INVALID);
 
-	enum class EReachabilityDetermination : uint8_t
-	{
-		DefinitelyReachable,
-		// Reachable from a definite source
-		PossiblyReachable,
-		// Reachable from a possible source
-		DefinitelyUnreachable,
-		// Unreachable from any possible source
-	};
-
-	EReachabilityDetermination determineReachability(const IVariableDatabase* db, int vertex);
-	bool processVertexVariableChange(IVariableDatabase* db, VarID variable);
-	void updateGraphsForEdgeChange(IVariableDatabase* db, VarID variable);
-	void onReachabilityChanged(int vertexIndex, VarID sourceVar, bool inMinGraph);
-	void sanityCheckUnreachable(IVariableDatabase* db, int vertexIndex);
-
-	void onExplanationGraphEdgeChange(bool edgeWasAdded, int from, int to);
-
-	void addSource(VarID source);
-	bool removeSource(IVariableDatabase* db, VarID source);
-
-	inline bool definitelyNeedsToReach(const IVariableDatabase* db, VarID var) const
-	{
-		return !db->getPotentialValues(var).anyPossible(m_notReachableMask);
-	}
-
-	inline bool definitelyIsSource(const IVariableDatabase* db, VarID var) const
-	{
-		return !db->getPotentialValues(var).anyPossible(m_notSourceMask);
-	}
-
-	inline bool definitelyNotSource(const IVariableDatabase* db, VarID var) const
-	{
-		return !db->getPotentialValues(var).anyPossible(m_sourceMask);
-	}
-
-	inline bool possiblyIsSource(const IVariableDatabase* db, VarID var)
-	{
-		return !definitelyNotSource(db, var);
-	}
-
-	inline bool possiblyOpenEdge(const IVariableDatabase* db, VarID var) const
-	{
-		return db->getPotentialValues(var).anyPossible(m_edgeOpenMask);
-	}
-
-	inline bool definitelyOpenEdge(const IVariableDatabase* db, VarID var) const
-	{
-		return !db->getPotentialValues(var).anyPossible(m_edgeBlockedMask);
-	}
-
-	inline bool definitelyClosedEdge(const IVariableDatabase* db, VarID var)
-	{
-		return !possiblyOpenEdge(db, var);
-	}
-
-	class EdgeWatcher : public IVariableWatchSink
-	{
-	public:
-		EdgeWatcher(ReachabilityConstraint& parent)
-			: m_parent(parent)
-		{
-		}
-
-		virtual IConstraint* asConstraint() override { return &m_parent; }
-		virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override;
-
-	protected:
-		ReachabilityConstraint& m_parent;
-	};
-
-	EdgeWatcher m_edgeWatcher;
-
-	shared_ptr<TTopologyVertexData<VarID>> m_sourceGraphData;
-	shared_ptr<ITopology> m_sourceGraph;
-	shared_ptr<TTopologyVertexData<VarID>> m_edgeGraphData;
-	shared_ptr<EdgeTopology> m_edgeGraph;
-
-	// Contains edges that DEFINITELY exist. Edges are only added to this graph.
-	shared_ptr<BacktrackingDigraphTopology> m_minGraph;
-	// Contains edges that POSSIBLY exist. Edges are only removed from this graph.
-	shared_ptr<BacktrackingDigraphTopology> m_maxGraph;
-	// Synchronized with MaxGraph. Used during explanations where we need to temporarily rewind graph state, but we don't
-	// want to propagate to the source reachability trees.
-	shared_ptr<BacktrackingDigraphTopology> m_explanationGraph;
-
-	ValueSet m_sourceMask;
-	ValueSet m_notSourceMask;
-
-	ValueSet m_requireReachableMask;
-	ValueSet m_notReachableMask;
-
-	ValueSet m_edgeBlockedMask;
-	ValueSet m_edgeOpenMask;
-
-	hash_map<VarID, WatcherHandle> m_vertexWatchHandles;
-	hash_map<VarID, WatcherHandle> m_edgeWatchHandles;
-
-	struct BacktrackData
-	{
-		SolverDecisionLevel level;
-		vector<VarID> reachabilitySourcesRemoved;
-	};
-
-	vector<BacktrackData> m_backtrackData;
-
-	using ESTreeType = ESTree<BacktrackingDigraphTopology>;
-	using RamalRepsType = RamalReps<BacktrackingDigraphTopology>;
-
-	struct ReachabilitySourceData
-	{
-		#if REACHABILITY_USE_RAMAL_REPS
-		shared_ptr<RamalRepsType> minReachability;
-		shared_ptr<RamalRepsType> maxReachability;
-		#else
-		shared_ptr<ESTreeType> minReachability;
-		shared_ptr<ESTreeType> maxReachability;
-		#endif
-		EventListenerHandle minReachabilityChangedHandle = INVALID_EVENT_LISTENER_HANDLE;
-		EventListenerHandle maxReachabilityChangedHandle = INVALID_EVENT_LISTENER_HANDLE;
-	};
-
-	vector<VarID> m_vertexProcessList;
-	vector<VarID> m_edgeProcessList;
-
-	vector<VarID> m_initialPotentialSources;
-	hash_map<VarID, ReachabilitySourceData> m_reachabilitySources;
-
-	hash_map<VarID, int> m_variableToSourceVertexIndex;
-	hash_map<VarID, int> m_variableToSourceEdgeIndex;
-
-	IVariableDatabase* m_edgeChangeDb = nullptr;
-	bool m_edgeChangeFailure = false;
-	bool m_inEdgeChange = false;
-	bool m_backtracking = false;
-	bool m_explainingSourceRequirement = false;
-	int m_totalNumEdges = 0;
+	virtual shared_ptr<RamalRepsType> makeTopology(const shared_ptr<BacktrackingDigraphTopology>& graph) const override;
+	virtual EventListenerHandle addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) override;
+	virtual EventListenerHandle addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) override;
 
-	DepthFirstSearchAlgorithm m_dfs;
-	mutable TMaxFlowMinCutAlgorithm<int> m_maxFlowAlgo;
-	vector<TFlowGraphEdge<int>> m_flowGraphEdges;
-	FlowGraphLookupMap m_flowGraphLookup;
-	RamalRepsEdgeDefinitions m_reachabilityEdgeLookup;
+	void onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph);
 };
 
 } // namespace Vertexy

vertexy/src/public/constraints/ShortestPathConstraint.h

@@ -0,0 +1,101 @@
+// Copyright Proletariat, Inc. All Rights Reserved.
+#pragma once
+#include "ConstraintTypes.h"
+#include "TopologySearchConstraint.h"
+#include "IConstraint.h"
+#include "SignedClause.h"
+#include "ds/ESTree.h"
+#include "ds/RamalReps.h"
+#include "topology/BacktrackingDigraphTopology.h"
+#include "topology/DigraphEdgeTopology.h"
+#include "topology/TopologyVertexData.h"
+#include "topology/algo/MaxFlowMinCut.h"
+#include "topology/algo/ShortestPath.h"
+#include "variable/IVariableDatabase.h"
+#include "constraints/ConstraintOperator.h"
+#include "ds/BacktrackableValue.h"
+
+#define REACHABILITY_USE_RAMAL_REPS 1
+
+namespace Vertexy
+{
+
+/** Constraint to ensure the shortest paths between source and destination nodes
+ *  All destination nodes must have at least 1 shortest path to at least 1 source node
+ *  this shortest path must have a relation with 'distance'
+ */
+class ShortestPathConstraint : public ITopologySearchConstraint
+{
+public:
+	ShortestPathConstraint(const ConstraintFactoryParams& params,
+		const shared_ptr<TTopologyVertexData<VarID>>& sourceGraphData,
+		const ValueSet& sourceMask,
+		const ValueSet& requireReachableMask,
+		const shared_ptr<TTopologyVertexData<VarID>>& edgeGraphData,
+		const ValueSet& edgeBlockedMask,
+		EConstraintOperator op,
+		VarID distance
+	);
+
+	struct ShortestPathFactory
+	{
+		static ShortestPathConstraint* construct(
+			const ConstraintFactoryParams& params,
+			// Graph of vertices where reachability is calculated
+			const shared_ptr<TTopologyVertexData<VarID>>& sourceGraphData,
+			// Values of vertices in SourceGraph that establish it as a reachability source
+			const vector<int>& sourceValues,
+			// Values of vertices in SourceGraph that establish it as needing to be reachable from a source
+			const vector<int>& needReachableValues,
+			// The variables for each edge of source graph
+			const shared_ptr<TTopologyVertexData<VarID>>& edgeGraphData,
+			// Values of vertices in the edge graph establishing that edge as "off"
+			const vector<int>& edgeBlockedValues,
+			// How to compare distance
+			EConstraintOperator op,
+			// The variable that stores the distance
+			VarID distance);
+	};
+
+	using Factory = ShortestPathFactory;
+
+	virtual EConstraintType getConstraintType() const override { return EConstraintType::ShortestPath; }
+	virtual void onInitialArcConsistency(IVariableDatabase* db) override;
+
+protected:
+
+	bool isValidDistance(const IVariableDatabase* db, int dist) const;
+
+	virtual bool isPossiblyValid(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) override;
+	virtual EValidityDetermination determineValidityHelper(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex, VarID srcVertex) override;
+	virtual shared_ptr<RamalRepsType> makeTopology(const shared_ptr<BacktrackingDigraphTopology>& graph) const override;
+	virtual EventListenerHandle addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) override;
+	virtual EventListenerHandle addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) override;
+	virtual vector<Literal> explainInvalid(const NarrowingExplanationParams& params) override;
+	virtual void createTempSourceData(ReachabilitySourceData& data, int vertexIndex) const override;
+	void onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph);
+	void backtrack(const IVariableDatabase* db, SolverDecisionLevel level) override;
+
+	EConstraintOperator m_op;
+	VarID m_distance;
+
+	// used to determine the path that is either too long or too short when explaning
+	ShortestPathAlgorithm m_shortestPathAlgo;
+
+	// used when m_op is LessThan/LessThanEq and records the last timestamp in which a vertex was deemed valid
+	hash_map<int, hash_map<int, TBacktrackableValue<SolverTimestamp>>> m_lastValidTimestamp;
+	hash_map<int, hash_map<int, SolverTimestamp>> m_validTimestampsToCommit;
+	hash_set<tuple<int, int>> m_alwaysForbiddenPaths;
+
+	hash_set<int> m_queuedVertexChanges;
+	bool m_processingVertices = false;
+
+	void commitValidTimestamps(const IVariableDatabase* db);
+	void onEdgeChangeFailure(const IVariableDatabase* db) override;
+	void onEdgeChangeSuccess(const IVariableDatabase* db) override;
+	void addTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex);
+	void removeTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex);
+	void processQueuedVertexChanges(IVariableDatabase* db) override;
+};
+
+} // namespace Vertexy