From d7106287e8045b0ff05becb5966b863e56301b84 Mon Sep 17 00:00:00 2001 From: chriseth Date: Sat, 25 Sep 2021 18:54:52 +0200 Subject: [PATCH] Make magic squares work. --- libsolutil/BooleanLP.cpp | 34 ++++++++++--------- libsolutil/LP.cpp | 6 ++-- test/libsolutil/BooleanLP.cpp | 64 ++++++++++++++++++++++++----------- 3 files changed, 67 insertions(+), 37 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 6edef8123..20dc27004 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -247,8 +247,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) pair> BooleanLPSolver::check(vector const& _expressionsToEvaluate) { - cout << "Solving boolean constraint system" << endl; - cout << toString() << endl; +// cout << "Solving boolean constraint system" << endl; +// cout << toString() << endl; +// cout << "--------------" << endl; if (m_state.back().infeasible) return make_pair(CheckResult::UNSATISFIABLE, vector{}); @@ -554,27 +555,25 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi // TODO as input we do not need the full solving state, only the bounds +// (and the variable names) pair> BooleanLPSolver::runDPLL(SolvingState& _solvingState, DPLL _dpll) { - //cout << "Running dpll on" << endl << toString(_solvingState.bounds) << "\n" << toString(_dpll) << endl; + //cout << "Running dpll on" << endl << toString(_solvingState.bounds) << "\nwith clauses\n" << toString(_dpll) << endl; + // Simplify clauses with only one literal. + // TODO Maybe this could already analyze clauses and add bounds? auto&& [simplifyResult, booleanModel] = _dpll.simplify(); if (!simplifyResult) return {CheckResult::UNSATISFIABLE, {}}; - cout << "Simplified to" << endl << toString(_solvingState.bounds) << "\n" << toString(_dpll) << endl; +// cout << "Simplified to" << endl << toString(_solvingState.bounds) << "\nwith clauses\n" << toString(_dpll) << endl; +// cout << "----------" << endl; CheckResult result = CheckResult::UNKNOWN; map model; - // TODO we really should do the below, and probably even before and after each boolean decision. - // It is very likely that we have some complicated boolean condition in the program, but - // the unconditional things are already unsatisfiable. - // TODO could run this check already even though not all variables are assigned - // and return unsat if it is already unsat. - if (_dpll.clauses.empty()) { - cout << "Invoking LP..." << endl; + //cout << "Invoking LP..." << endl; _solvingState.constraints.clear(); for (size_t c: _dpll.constraints) _solvingState.constraints.emplace_back(constraint(c)); @@ -589,19 +588,22 @@ pair> BooleanLPSolver::runDPLL(SolvingState& switch (lpResult) { case LPResult::Infeasible: +// cout << "Infeasible." << endl; result = CheckResult::UNSATISFIABLE; break; case LPResult::Feasible: + case LPResult::Unbounded: +// cout << "Feasible." << endl; // TODO this is actually wrong, but difficult to test otherwise. result = CheckResult::SATISFIABLE; break; case LPResult::Unknown: - case LPResult::Unbounded: +// cout << "Unknown." << endl; result = CheckResult::UNKNOWN; break; } } - else + if (result != CheckResult::UNSATISFIABLE && !_dpll.clauses.empty()) { size_t varIndex = _dpll.findUnassignedVariable(); @@ -609,18 +611,18 @@ pair> BooleanLPSolver::runDPLL(SolvingState& if (_dpll.setVariable(varIndex, true)) { booleanModel[varIndex] = true; - cout << "Trying " << variableName(varIndex) << " = true\n"; + //cout << "Trying " << variableName(varIndex) << " = true\n"; tie(result, model) = runDPLL(_solvingState, move(_dpll)); // TODO actually we should also handle UNKNOWN here. } // TODO it will never be "satisfiable" if (result != CheckResult::SATISFIABLE) { - cout << "Trying " << variableName(varIndex) << " = false\n"; + //cout << "Trying " << variableName(varIndex) << " = false\n"; if (!copy.setVariable(varIndex, false)) return {CheckResult::UNSATISFIABLE, {}}; booleanModel[varIndex] = false; - /*auto&& [result, model] = */runDPLL(_solvingState, move(copy)); + tie(result, model) = runDPLL(_solvingState, move(copy)); } } if (result == CheckResult::SATISFIABLE) diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 41f1f5d34..43c2e83b0 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -230,7 +230,7 @@ vector solutionVector(Tableau const& _tableau) /// Tries for a number of iterations and then gives up. pair simplexEq(Tableau _tableau) { - size_t const iterations = min(60, 50 + _tableau.objective.size() * 2); + size_t const iterations = min(120, 50 + _tableau.objective.size() * 2); for (size_t step = 0; step <= iterations; ++step) { optional pivotColumn = findPivotColumn(_tableau); @@ -277,7 +277,9 @@ pair simplexPhaseI(Tableau _tableau) LPResult result; tie(result, _tableau) = simplexEq(move(_tableau)); - solAssert(result == LPResult::Feasible || result == LPResult::Unbounded, ""); + solAssert(result != LPResult::Infeasible, ""); + if (result == LPResult::Unknown) + return make_pair(LPResult::Unknown, Tableau{}); vector optimum = solutionVector(_tableau); diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp index a1de4ec07..1b05cf600 100644 --- a/test/libsolutil/BooleanLP.cpp +++ b/test/libsolutil/BooleanLP.cpp @@ -254,30 +254,56 @@ BOOST_AUTO_TEST_CASE(boolean_complex) infeasible(); } -BOOST_AUTO_TEST_CASE(magic_square) +BOOST_AUTO_TEST_CASE(magic_square_3) { vector vars; for (size_t i = 0; i < 9; i++) vars.push_back(variable(string{static_cast('a' + i)})); + Expression sum = variable("sum"); for (Expression const& var: vars) solver.addAssertion(1 <= var && var <= 9); - // If we assert all to be mutually distinct, the problems gets too large. for (size_t i = 0; i < 9; i++) - for (size_t j = i + 7; j < 9; j++) + for (size_t j = i + 1; j < 9; j++) solver.addAssertion(vars[i] != vars[j]); - for (size_t i = 0; i < 4; i++) - solver.addAssertion(vars[i] != vars[i + 1]); for (size_t i = 0; i < 3; i++) - solver.addAssertion(vars[i] + vars[i + 3] + vars[i + 6] == 15); + solver.addAssertion(vars[i] + vars[i + 3] + vars[i + 6] == sum); for (size_t i = 0; i < 9; i += 3) - solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] == 15); + solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] == sum); + solver.addAssertion(vars[0] + vars[4] + vars[8] == sum); + solver.addAssertion(vars[2] + vars[4] + vars[6] == sum); feasible({ - {vars[0], "1"}, {vars[1], "0"}, {vars[2], "5"}, - {vars[3], "1"}, {vars[4], "0"}, {vars[5], "5"}, - {vars[6], "1"}, {vars[7], "0"}, {vars[8], "5"} + {sum, "15"}, + {vars[0], "8"}, {vars[1], "3"}, {vars[2], "4"}, + {vars[3], "1"}, {vars[4], "5"}, {vars[5], "9"}, + {vars[6], "6"}, {vars[7], "7"}, {vars[8], "2"} }); } +// This still takes too long. +// +//BOOST_AUTO_TEST_CASE(magic_square_4) +//{ +// vector vars; +// for (size_t i = 0; i < 16; i++) +// vars.push_back(variable(string{static_cast('a' + i)})); +// for (Expression const& var: vars) +// solver.addAssertion(1 <= var && var <= 16); +// for (size_t i = 0; i < 16; i++) +// for (size_t j = i + 1; j < 16; j++) +// solver.addAssertion(vars[i] != vars[j]); +// for (size_t i = 0; i < 4; i++) +// solver.addAssertion(vars[i] + vars[i + 4] + vars[i + 8] + vars[i + 12] == 34); +// for (size_t i = 0; i < 16; i += 4) +// solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] + vars[i + 3] == 34); +// solver.addAssertion(vars[0] + vars[5] + vars[10] + vars[15] == 34); +// solver.addAssertion(vars[3] + vars[6] + vars[9] + vars[12] == 34); +// feasible({ +// {vars[0], "9"}, {vars[1], "5"}, {vars[2], "1"}, +// {vars[3], "4"}, {vars[4], "3"}, {vars[5], "8"}, +// {vars[6], "2"}, {vars[7], "7"}, {vars[8], "6"} +// }); +//} + BOOST_AUTO_TEST_CASE(boolean_complex_2) { Expression x = variable("x"); @@ -285,16 +311,16 @@ BOOST_AUTO_TEST_CASE(boolean_complex_2) Expression a = booleanVariable("a"); Expression b = booleanVariable("b"); solver.addAssertion(x != 20); - feasible({{x, "19"}}); + feasible({{x, "21"}}); solver.addAssertion(x <= 5 || (x > 7 && x != 8)); - solver.addAssertion(a = (x == 9)); - feasible({{a, "1"}, {b, "0"}, {x, "5"}}); -// solver.addAssertion(!a || (x == 10)); -// solver.addAssertion(b == !a); -// solver.addAssertion(b == (x < 200)); -// feasible({{a, "1"}, {b, "0"}, {x, "5"}}); -// solver.addAssertion(a && b); -// infeasible(); + solver.addAssertion(a == (x == 9)); + feasible({{a, "0"}, {b, "unknown"}, {x, "21"}}); + solver.addAssertion(!a || (x == 10)); + solver.addAssertion(b == !a); + solver.addAssertion(b == (x < 200)); + feasible({{a, "0"}, {b, "1"}, {x, "199"}}); + solver.addAssertion(a && b); + infeasible(); }