From 7cfc2f6a12aa037d42db35ce4f5ec5c8cc8f78e9 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 23 Mar 2022 21:25:57 +0100 Subject: [PATCH] Incremental lp solver. --- libsolutil/BooleanLP.cpp | 37 ++++----- libsolutil/BooleanLP.h | 4 - libsolutil/CDCL.cpp | 15 +++- libsolutil/CDCL.h | 2 + libsolutil/LP.cpp | 160 +++++++++++++++------------------------ libsolutil/LP.h | 14 +--- 6 files changed, 98 insertions(+), 134 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 11d0da6a9..c6a430505 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -233,42 +233,41 @@ pair> BooleanLPSolver::check(vector 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> 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 previousConditionalConstraints; - auto theorySolver = [&](size_t /*_decisionLevel*/, map const& _booleanAssignment) -> optional + auto theorySolver = [&](size_t _trailSize, map const& _newBooleanAssignment) -> optional { - SolvingState lpStateToCheck = lpState; - set conditionalConstraints; - for (auto&& [constraintIndex, value]: _booleanAssignment) + lpSolvers.emplace_back(_trailSize, LPSolver(lpSolvers.back().second)); + + for (auto&& [constraintIndex, value]: _newBooleanAssignment) { if (!value || !state().conditionalConstraints.count(constraintIndex)) continue; - conditionalConstraints.emplace(constraintIndex); - } - set constraintsToRemove = previousConditionalConstraints - conditionalConstraints; - vector 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)); - previousConditionalConstraints = move(conditionalConstraints); + auto&& [result, modelOrReason] = lpSolvers.back().second.check(); // We can only really use the result "infeasible". Everything else should be "sat". if (result == LPResult::Infeasible) { @@ -281,7 +280,11 @@ pair> BooleanLPSolver::check(vector 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) diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index c207657b0..879431d31 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -122,10 +122,6 @@ private: /// Stack of state, to allow for push()/pop(). std::vector 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}; }; diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index 25c730b52..ad79a11b0 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -71,7 +71,13 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol optional conflictClause = propagate(); if (!conflictClause && m_theorySolver) { - conflictClause = m_theorySolver(currentDecisionLevel(), m_assignments); + size_t lastTrailSizeCall = m_assignemntTrailSizesWeCalledSolverFor.empty() ? 0 : m_assignemntTrailSizesWeCalledSolverFor.back(); + + std::map 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); } diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index da8837eb6..39e45f5f0 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -161,6 +161,8 @@ private: std::vector m_decisionPoints; /// Index into assignmentTrail: All assignments starting there have not yet been propagated. size_t m_assignmentQueuePointer = 0; + + std::vector m_assignemntTrailSizesWeCalledSolverFor; }; diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 75eb2ac80..cde137b90 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -357,6 +357,7 @@ pair> simplex(vector _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()); + 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; - updateSubProblems(); + //cout << "Done splitting." << endl; } -pair> LPSolver::check( - std::set const& _constraintsToRemove, - std::vector constraintsToAdd -) -{ - set 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 touchedProblems; - for (auto const& [index, entry]: constraint.data.enumerateTail()) - if (entry && m_subProblemsPerVariable[index] != static_cast(-1)) - touchedProblems.emplace(m_subProblemsPerVariable[index]); - if (touchedProblems.empty()) - { - //cout << "Creating new sub problem." << endl; - m_subProblems.emplace_back(make_unique()); - 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)); - } - - // 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 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) -{ - 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) +void LPSolver::addConstraint(Constraint const& _constraint) { + //cout << "Adding constraint " << endl; + set touchedProblems; for (auto const& [index, entry]: _constraint.data.enumerateTail()) - if (entry) - { - solAssert(m_subProblemsPerVariable[index] == static_cast(-1) || m_subProblemsPerVariable[index] == _subProblem); - m_subProblemsPerVariable[index] = _subProblem; - } - solAssert(!_constraint.reasons.empty()); + if (entry && m_subProblemsPerVariable[index] != static_cast(-1)) + touchedProblems.emplace(m_subProblemsPerVariable[index]); + if (touchedProblems.empty()) { - solAssert(_constraint.reasons.size() == 1); - m_subProblemsPerConstraintReason[*_constraint.reasons.begin()] = _subProblem; + //cout << "Creating new sub problem." << endl; + // 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); } - m_subProblems[_subProblem]->dirty = true; - m_subProblems[_subProblem]->removableConstraints.emplace_back(move(_constraint)); + for (size_t problemToErase: touchedProblems | ranges::views::tail | ranges::views::reverse) + combineSubProblems(*touchedProblems.begin(), problemToErase); + addConstraintToSubProblem(*touchedProblems.begin(), _constraint); + //cout << "done" << endl; } -void LPSolver::updateSubProblems() +pair> LPSolver::check() { + //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) + return {LPResult::Infeasible, reasonSetForSubProblem(*problem)}; } - problem->dirty = false; - if (problem->result == LPResult::Infeasible) - break; } + + 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(-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 diff --git a/libsolutil/LP.h b/libsolutil/LP.h index abbaf89b6..7bb3a1528 100644 --- a/libsolutil/LP.h +++ b/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"), - /// adding constraints and then checks for feasibility. - std::pair> check( - std::set const& _constraintsToRemove = {}, - std::vector constraintsToAdd = {} - ); + void addConstraint(Constraint const& _constraint); + std::pair> check(); 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 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> m_subProblems; + std::vector> m_subProblems; std::vector m_subProblemsPerVariable; std::vector m_subProblemsPerConstraint; - /// The key of this is a constraint reason, not an index in the state. - std::map m_subProblemsPerConstraintReason; /// TODO also store the first infeasible subproblem? /// TODO still retain the cache? };