Incremental lp solver.

libsolutil/BooleanLP.cpp

@@ -233,42 +233,41 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 		else
 			resizeAndSet(lpState.variableNames, index, name);
 
+	// TODO keep a cache as a member that is never reset.
+	// TODO We can also keep the split unconditionals across push/pop
+	// We only need to be careful to update the number of variables.
+
+	std::vector<std::pair<size_t, LPSolver>> lpSolvers;
+
 	// TODO We start afresh here. If we want this to reuse the existing results
 	// from previous invocations of the boolean solver, we still have to use
 	// a cache.
 	// The current optimization is only for CDCL.
-	m_lpSolver.setState(lpState);
+	lpSolvers.emplace_back(0, LPSolver{});
+	lpSolvers.back().second.setState(lpState);
 
 	//cout << "Boolean variables:" << joinHumanReadable(booleanVariables) << endl;
 	//cout << "Running LP solver on fixed constraints." << endl;
-	if (m_lpSolver.check().first == LPResult::Infeasible)
+	if (lpSolvers.back().second.check().first == LPResult::Infeasible)
 	{
 		cout << "----->>>>> unsatisfiable" << endl;
 		return {CheckResult::UNSATISFIABLE, {}};
 	}
 
-	set<size_t> previousConditionalConstraints;
+	auto theorySolver = [&](size_t _trailSize, map<size_t, bool> const& _newBooleanAssignment) -> optional<Clause>
-	auto theorySolver = [&](size_t /*_decisionLevel*/, map<size_t, bool> const& _booleanAssignment) -> optional<Clause>
 	{
-		SolvingState lpStateToCheck = lpState;
+		lpSolvers.emplace_back(_trailSize, LPSolver(lpSolvers.back().second));
-		set<size_t> conditionalConstraints;
+
-		for (auto&& [constraintIndex, value]: _booleanAssignment)
+		for (auto&& [constraintIndex, value]: _newBooleanAssignment)
 		{
 			if (!value || !state().conditionalConstraints.count(constraintIndex))
 				continue;
-			conditionalConstraints.emplace(constraintIndex);
-		}
-		set<size_t> constraintsToRemove = previousConditionalConstraints - conditionalConstraints;
-		vector<Constraint> constraintsToAdd;
-		for (size_t constraintIndex: conditionalConstraints - previousConditionalConstraints)
-		{
 			// "reason" is already stored for those constraints.
 			Constraint const& constraint = state().conditionalConstraints.at(constraintIndex);
 			solAssert(constraint.reasons.size() == 1 && *constraint.reasons.begin() == constraintIndex);
-			constraintsToAdd.emplace_back(constraint);
+			lpSolvers.back().second.addConstraint(constraint);
 		}
-		auto&& [result, modelOrReason] = m_lpSolver.check(constraintsToRemove, move(constraintsToAdd));
+		auto&& [result, modelOrReason] = lpSolvers.back().second.check();
-		previousConditionalConstraints = move(conditionalConstraints);
 		// We can only really use the result "infeasible". Everything else should be "sat".
 		if (result == LPResult::Infeasible)
 		{
@@ -281,7 +280,11 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 		else
 			return nullopt;
 	};
-	auto backtrackNotify = [](size_t /*_decisionLevel*/) {};
+	auto backtrackNotify = [&](size_t _trailSize)
+	{
+		while (lpSolvers.back().first > _trailSize)
+			lpSolvers.pop_back();
+	};
 
 	auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve();
 	if (!optionalModel)

libsolutil/BooleanLP.h

@@ -122,10 +122,6 @@ private:
 
 	/// Stack of state, to allow for push()/pop().
 	std::vector<State> m_state{{State{}}};
-	// TODO this is only here so that it can keep its cache.
-	// It might be better to just have the cache here.
-	// Although its stote is only the cache in the end...
-	LPSolver m_lpSolver{false};
 };
 
 

libsolutil/CDCL.cpp

@@ -71,7 +71,13 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		optional<Clause> conflictClause = propagate();
 		if (!conflictClause && m_theorySolver)
 		{
-			conflictClause = m_theorySolver(currentDecisionLevel(), m_assignments);
+			size_t lastTrailSizeCall = m_assignemntTrailSizesWeCalledSolverFor.empty() ? 0 : m_assignemntTrailSizesWeCalledSolverFor.back();
+
+			std::map<size_t, bool> newAssignments;
+			for (size_t i = lastTrailSizeCall; i < m_assignmentTrail.size(); ++i)
+				newAssignments[m_assignmentTrail[i].variable] = m_assignmentTrail[i].positive;
+			conflictClause = m_theorySolver(m_assignmentTrail.size(), newAssignments);
+			m_assignemntTrailSizesWeCalledSolverFor.emplace_back(m_assignmentTrail.size());
 //			if (conflictClause)
 //				cout << "Theory gave us conflict: " << toString(*conflictClause) << endl;
 		}
@@ -90,6 +96,10 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 			}
 			auto&& [learntClause, backtrackLevel] = analyze(move(*conflictClause));
 			cancelUntil(backtrackLevel);
+			while (!m_assignemntTrailSizesWeCalledSolverFor.empty() && m_assignemntTrailSizesWeCalledSolverFor.back() > m_assignmentTrail.size())
+				m_assignemntTrailSizesWeCalledSolverFor.pop_back();
+			if (m_backtrackNotify)
+				m_backtrackNotify(m_assignemntTrailSizesWeCalledSolverFor.empty() ? 0 : m_assignemntTrailSizesWeCalledSolverFor.back());
 			solAssert(!learntClause.empty());
 			solAssert(!isAssigned(learntClause.front()));
 //			for (size_t i = 1; i < learntClause.size(); i++)
@@ -325,8 +335,7 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 	}
 	m_decisionPoints.resize(_backtrackLevel);
 	m_assignmentQueuePointer = m_assignmentTrail.size();
-	if (m_backtrackNotify)
+
-		m_backtrackNotify(currentDecisionLevel());
 	solAssert(currentDecisionLevel() == _backtrackLevel);
 }
 

libsolutil/CDCL.h

@@ -161,6 +161,8 @@ private:
 	std::vector<size_t> m_decisionPoints;
 	/// Index into assignmentTrail: All assignments starting there have not yet been propagated.
 	size_t m_assignmentQueuePointer = 0;
+
+	std::vector<size_t> m_assignemntTrailSizesWeCalledSolverFor;
 };
 
 

libsolutil/LP.cpp

@@ -357,6 +357,7 @@ pair<LPResult, vector<rational>> simplex(vector<Constraint> _constraints, Linear
 	bool hasEquations = false;
 	tie(tableau.data, hasEquations) = toEquationalForm(_constraints);
 	tableau.objective.resize(tableau.data.at(0).size());
+	//cout << "Running simplex on " << tableau.objective.size() << " x " << tableau.data.size() << endl;
 
 	if (hasEquations || needsPhaseI(tableau))
 	{
@@ -796,10 +797,9 @@ LPSolver::LPSolver(bool)
 
 void LPSolver::setState(SolvingState _state)
 {
-	cout << "Set state:\n" << _state.toString() << endl;
+	//cout << "Set state:\n" << _state.toString() << endl;
 	m_state = move(_state);
 	m_subProblems.clear();
-	m_subProblemsPerConstraintReason = {};
 
 	normalizeRowLengths(m_state);
 
@@ -811,12 +811,16 @@ void LPSolver::setState(SolvingState _state)
 	// TODO we could simplify, but then we need the option to answer 'infeasible' here.
 	// TODO assert that none of the constraints here have a reason set.
 
-	cout << "Splitting..." << endl;
+	// TODO if we eliminate variables, we should store their values and their reasons.
+	// If new constraints come in, the eliminated variables have to be substituted.
+
+
+	//cout << "Splitting..." << endl;
 	ProblemSplitter splitter(m_state);
 	while (splitter)
 	{
 		auto&& [variables, constraints] = splitter.next();
-		m_subProblems.emplace_back(make_unique<SubProblem>());
+		m_subProblems.emplace_back(SubProblem());
 		solAssert(m_subProblems.back()->dirty);
 		for (auto&& [i, included]: variables | ranges::views::enumerate)
 			if (included)
@@ -825,111 +829,36 @@ void LPSolver::setState(SolvingState _state)
 			if (included)
 				m_subProblemsPerConstraint[i] = m_subProblems.size() - 1;
 		//cout << "Adding new sub problem with " << m_subProblems.back()->variables.size() << " vars and " << m_subProblems.back()->constraints.size() << " constraints\n" << endl;
-		// We do not need t ofill m_subProblemsPerConstraintReason because we do not assume
-		// these constraints to have reasons, so they cannot be removed.
-		// TODO we cauld assert that
 		//cout << "-------------------- Split out" << endl;
 		//cout << m_subProblems.back()->state.toString() << endl;
 	}
-	cout << "Updating..." << endl;
+	//cout << "Done splitting." << endl;
-	updateSubProblems();
 }
 
-pair<LPResult, variant<Model, ReasonSet>> LPSolver::check(
+void LPSolver::addConstraint(Constraint const& _constraint)
-	std::set<size_t> const& _constraintsToRemove,
-	std::vector<Constraint> constraintsToAdd
-)
 {
-	set<size_t> subproblemsToUpdate;
-	for (size_t constraintReason: _constraintsToRemove)
-	{
-		//cout << "Removing constraint " << constraintReason << endl;
-		SubProblem& problem = *m_subProblems[m_subProblemsPerConstraintReason.at(constraintReason)];
-		problem.dirty = true;
-		cxx20::erase_if(
-			problem.removableConstraints,
-			[constraintReason](Constraint const& _constraint) {
-				if (_constraint.reasons.count(constraintReason))
-				{
-					solAssert(_constraint.reasons.size() == 1);
-					return true;
-				}
-				else
-					return false;
-			}
-		);
-	}
-
-	for (Constraint& constraint: constraintsToAdd)
-	{
 	//cout << "Adding constraint " << endl;
-		solAssert(constraint.reasons.size() == 1);
 	set<size_t> touchedProblems;
-		for (auto const& [index, entry]: constraint.data.enumerateTail())
+	for (auto const& [index, entry]: _constraint.data.enumerateTail())
 		if (entry && m_subProblemsPerVariable[index] != static_cast<size_t>(-1))
 			touchedProblems.emplace(m_subProblemsPerVariable[index]);
 	if (touchedProblems.empty())
 	{
 		//cout << "Creating new sub problem." << endl;
-			m_subProblems.emplace_back(make_unique<SubProblem>());
+		// TODO we could find an empty spot for the pointer.
+		m_subProblems.emplace_back(SubProblem());
 		solAssert(m_subProblems.back()->dirty);
 		touchedProblems.emplace(m_subProblems.size() - 1);
 	}
 	for (size_t problemToErase: touchedProblems | ranges::views::tail | ranges::views::reverse)
 		combineSubProblems(*touchedProblems.begin(), problemToErase);
-		addConstraintToSubProblem(*touchedProblems.begin(), move(constraint));
+	addConstraintToSubProblem(*touchedProblems.begin(), _constraint);
-	}
+	//cout << "done" << endl;
-
-	// TODO here, we split again and also remove empty problems.
-
-	// TODO here, we can try to split again.
-	// If we split here, then we maybe don't need to split in setState.
-
-	updateSubProblems();
-
-	for (unique_ptr<SubProblem> const& problem: m_subProblems)
-		if (problem && problem->result == LPResult::Infeasible)
-			return {LPResult::Infeasible, reasonSetForSubProblem(*problem)};
-
-	return {LPResult::Unknown, Model{}};
 }
 
-void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
+pair<LPResult, variant<Model, ReasonSet>> LPSolver::check()
-{
-	m_subProblems[_combineInto]->dirty = true;
-
-	for (size_t& item: m_subProblemsPerVariable)
-		if (item == _combineFrom)
-			item = _combineInto;
-	for (size_t& item: m_subProblemsPerConstraint)
-		if (item == _combineFrom)
-			item = _combineInto;
-	for (auto& item: m_subProblemsPerConstraintReason)
-		if (item.second == _combineFrom)
-			item.second = _combineInto;
-
-	m_subProblems[_combineFrom].reset();
-}
-
-void LPSolver::addConstraintToSubProblem(size_t _subProblem, Constraint _constraint)
-{
-	for (auto const& [index, entry]: _constraint.data.enumerateTail())
-		if (entry)
-		{
-			solAssert(m_subProblemsPerVariable[index] == static_cast<size_t>(-1) || m_subProblemsPerVariable[index] == _subProblem);
-			m_subProblemsPerVariable[index] = _subProblem;
-		}
-	solAssert(!_constraint.reasons.empty());
-	{
-		solAssert(_constraint.reasons.size() == 1);
-		m_subProblemsPerConstraintReason[*_constraint.reasons.begin()] = _subProblem;
-	}
-	m_subProblems[_subProblem]->dirty = true;
-	m_subProblems[_subProblem]->removableConstraints.emplace_back(move(_constraint));
-}
-
-void LPSolver::updateSubProblems()
 {
+	//cout << "Checking" << endl;
 	for (auto&& [index, problem]: m_subProblems | ranges::views::enumerate)
 	{
 		if (!problem || !problem->dirty)
@@ -947,11 +876,14 @@ void LPSolver::updateSubProblems()
 		{
 			problem->result = LPResult::Infeasible;
 			problem->model = {};
+			problem->dirty = false;
+			return {LPResult::Infeasible, reasonSetForSubProblem(*problem)};
 		}
 		else if (state.constraints.empty())
 		{
 			problem->result = LPResult::Feasible;
 			problem->model = {};
+			problem->dirty = false;
 		}
 		else
 		{
@@ -960,11 +892,39 @@ void LPSolver::updateSubProblems()
 			objectives.resize(state.variableNames.size(), rational(bigint(1)));
 			// TODO the model relies on the variable numbering.
 			tie(problem->result, problem->model) = simplex(state.constraints, move(objectives));
-		}
 			problem->dirty = false;
 			if (problem->result == LPResult::Infeasible)
-			break;
+				return {LPResult::Infeasible, reasonSetForSubProblem(*problem)};
 		}
+	}
+
+	return {LPResult::Unknown, Model{}};
+}
+
+void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
+{
+	m_subProblems[_combineInto]->dirty = true;
+
+	for (size_t& item: m_subProblemsPerVariable)
+		if (item == _combineFrom)
+			item = _combineInto;
+	for (size_t& item: m_subProblemsPerConstraint)
+		if (item == _combineFrom)
+			item = _combineInto;
+
+	m_subProblems[_combineFrom].reset();
+}
+
+void LPSolver::addConstraintToSubProblem(size_t _subProblem, Constraint _constraint)
+{
+	for (auto const& [index, entry]: _constraint.data.enumerateTail())
+		if (entry)
+		{
+			solAssert(m_subProblemsPerVariable[index] == static_cast<size_t>(-1) || m_subProblemsPerVariable[index] == _subProblem);
+			m_subProblemsPerVariable[index] = _subProblem;
+		}
+	m_subProblems[_subProblem]->dirty = true;
+	m_subProblems[_subProblem]->removableConstraints.emplace_back(move(_constraint));
 }
 
 SolvingState LPSolver::stateFromSubProblem(size_t _index) const

libsolutil/LP.h

@@ -181,12 +181,8 @@ public:
 	explicit LPSolver(bool _supportModels = true);
 
 	void setState(SolvingState _state);
-	/// Modifies the state by removing constraints (identified by their "reason"),
+	void addConstraint(Constraint const& _constraint);
-	/// adding constraints and then checks for feasibility.
+	std::pair<LPResult, std::variant<Model, ReasonSet>> check();
-	std::pair<LPResult, std::variant<Model, ReasonSet>> check(
-		std::set<size_t> const& _constraintsToRemove = {},
-		std::vector<Constraint> constraintsToAdd = {}
-	);
 
 private:
 	void combineSubProblems(size_t _combineInto, size_t _combineFrom);
@@ -196,6 +192,7 @@ private:
 	SolvingState m_state;
 	struct SubProblem
 	{
+		// TODO now we could actually put the constraints here again.
 		std::vector<Constraint> removableConstraints;
 		bool dirty = true;
 		LPResult result = LPResult::Unknown;
@@ -205,12 +202,9 @@ private:
 	SolvingState stateFromSubProblem(size_t _index) const;
 	ReasonSet reasonSetForSubProblem(SubProblem const& _subProblem);
 
-	// TODO we could also use optional
+	std::vector<std::optional<SubProblem>> m_subProblems;
-	std::vector<std::unique_ptr<SubProblem>> m_subProblems;
 	std::vector<size_t> m_subProblemsPerVariable;
 	std::vector<size_t> m_subProblemsPerConstraint;
-	/// The key of this is a constraint reason, not an index in the state.
-	std::map<size_t, size_t> m_subProblemsPerConstraintReason;
 	/// TODO also store the first infeasible subproblem?
 	/// TODO still retain the cache?
 };