From 4235933124312dfceb82a361d80cbd3942650122 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 23 Mar 2022 22:47:57 +0100 Subject: [PATCH] simplify. --- libsolutil/BooleanLP.cpp | 9 +++--- libsolutil/LP.cpp | 66 ++++++++++++++++++++++++++-------------- libsolutil/LP.h | 9 +++--- 3 files changed, 53 insertions(+), 31 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index c6a430505..974d6fd0a 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -244,11 +244,10 @@ pair> BooleanLPSolver::check(vector cons // a cache. // The current optimization is only for CDCL. 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 (lpSolvers.back().second.check().first == LPResult::Infeasible) + if ( + lpSolvers.back().second.setState(lpState) == LPResult::Infeasible || + lpSolvers.back().second.check().first == LPResult::Infeasible + ) { cout << "----->>>>> unsatisfiable" << endl; return {CheckResult::UNSATISFIABLE, {}}; diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index cde137b90..4e9999d92 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -586,9 +586,8 @@ string SolvingState::toString() const return result; } -pair> SolvingStateSimplifier::simplify() +pair, ReasonSet>> SolvingStateSimplifier::simplify() { - do { m_changed = false; @@ -605,7 +604,7 @@ pair> SolvingStateSimplifier::simplify() } while (m_changed); - return {LPResult::Unknown, move(m_model)}; + return {LPResult::Unknown, move(m_fixedVariables)}; } optional SolvingStateSimplifier::removeFixedVariables() @@ -623,7 +622,8 @@ optional SolvingStateSimplifier::removeFixedVariables() if (upper != lower) continue; set reasons = bounds.lowerReasons + bounds.upperReasons; - m_model[m_state.variableNames.at(index)] = lower; + m_fixedVariables[index] = lower; + //cout << "Fixed " << m_state.variableNames.at(index) << " to " << ::toString(lower) << endl; m_state.bounds[index] = {}; m_changed = true; @@ -723,7 +723,7 @@ void SolvingStateSimplifier::removeEmptyColumns() solAssert(!bounds.upper || bounds.upper >= 0); if (bounds.lower && bounds.upper) solAssert(*bounds.lower <= *bounds.upper); - m_model[m_state.variableNames.at(i)] = + m_fixedVariables[i] = bounds.upper ? *bounds.upper : *bounds.lower; @@ -795,25 +795,22 @@ LPSolver::LPSolver(bool) { } -void LPSolver::setState(SolvingState _state) +LPResult LPSolver::setState(SolvingState _state) { //cout << "Set state:\n" << _state.toString() << endl; m_state = move(_state); m_subProblems.clear(); - normalizeRowLengths(m_state); - m_subProblemsPerVariable.resize(m_state.variableNames.size(), static_cast(-1)); m_subProblemsPerConstraint.resize(m_state.constraints.size(), static_cast(-1)); - // TODO we should simplify, otherwise we get big problems with constanst that are used everywhere. - - // 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. - - // 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. - + normalizeRowLengths(m_state); + auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(m_state).simplify(); + if (result == LPResult::Infeasible) + return result; + // We do not need to store reasons because at this point, we do not have any reasons yet. + // We can add this and just need to store the reasons together with the variables. + m_fixedVariables = std::get(modelOrReasonSet); //cout << "Splitting..." << endl; ProblemSplitter splitter(m_state); @@ -833,15 +830,26 @@ void LPSolver::setState(SolvingState _state) //cout << m_subProblems.back()->state.toString() << endl; } //cout << "Done splitting." << endl; + return LPResult::Unknown; } -void LPSolver::addConstraint(Constraint const& _constraint) +void LPSolver::addConstraint(Constraint _constraint) { //cout << "Adding constraint " << endl; set touchedProblems; for (auto const& [index, entry]: _constraint.data.enumerateTail()) - if (entry && m_subProblemsPerVariable[index] != static_cast(-1)) - touchedProblems.emplace(m_subProblemsPerVariable[index]); + if (entry) + { + if (m_fixedVariables.count(index)) + { + // This can directly lead to a conflict. We will check it later during the + // simplify run on the split problems. + _constraint.data[0] -= _constraint.data[index] * m_fixedVariables.at(index); + _constraint.data[index] = {}; + } + else if (m_subProblemsPerVariable[index] != static_cast(-1)) + touchedProblems.emplace(m_subProblemsPerVariable[index]); + } if (touchedProblems.empty()) { //cout << "Creating new sub problem." << endl; @@ -861,15 +869,29 @@ pair> LPSolver::check() //cout << "Checking" << endl; for (auto&& [index, problem]: m_subProblems | ranges::views::enumerate) { - if (!problem || !problem->dirty) + if (!problem) + continue; + if (!problem->dirty) { - //cout << "not dirty" << endl; + solAssert(problem->result != LPResult::Infeasible); continue; } + //cout << "Updating sub problem" << endl; SolvingState state = stateFromSubProblem(index); normalizeRowLengths(state); - // TODO could also call simplify + + // The simplify run is important because it detects conflicts + // due to fixed variables. + auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(state).simplify(); + if (result == LPResult::Infeasible) + { + problem->result = LPResult::Infeasible; + problem->model = {}; + problem->dirty = false; + // TODO we could use the improved reason set above. + return {LPResult::Infeasible, reasonSetForSubProblem(*problem)}; + } //cout << state.toString() << endl; if (auto conflict = boundsToConstraints(state)) diff --git a/libsolutil/LP.h b/libsolutil/LP.h index 7bb3a1528..4734be649 100644 --- a/libsolutil/LP.h +++ b/libsolutil/LP.h @@ -119,7 +119,7 @@ public: SolvingStateSimplifier(SolvingState& _state): m_state(_state) {} - std::pair> simplify(); + std::pair, ReasonSet>> simplify(); private: /// Remove variables that have equal lower and upper bound. @@ -138,7 +138,7 @@ private: bool m_changed = false; SolvingState& m_state; - Model m_model; + std::map m_fixedVariables; }; /** @@ -180,8 +180,8 @@ class LPSolver public: explicit LPSolver(bool _supportModels = true); - void setState(SolvingState _state); - void addConstraint(Constraint const& _constraint); + LPResult setState(SolvingState _state); + void addConstraint(Constraint _constraint); std::pair> check(); private: @@ -202,6 +202,7 @@ private: SolvingState stateFromSubProblem(size_t _index) const; ReasonSet reasonSetForSubProblem(SubProblem const& _subProblem); + std::map m_fixedVariables; std::vector> m_subProblems; std::vector m_subProblemsPerVariable; std::vector m_subProblemsPerConstraint;