cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Make magic squares work.

Browse Source
This commit is contained in:
chriseth 2021-09-25 18:54:52 +02:00
parent 1252235e88
commit d7106287e8
3 changed files with 67 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
libsolutil/BooleanLP.cpp
View File

@ -247,8 +247,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> 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<string>{});
@ -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<CheckResult, map<string, rational>> 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<string, rational> 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<CheckResult, map<string, rational>> 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<CheckResult, map<string, rational>> 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)

6
libsolutil/LP.cpp
View File

@ -230,7 +230,7 @@ vector<rational> solutionVector(Tableau const& _tableau)
/// Tries for a number of iterations and then gives up.
pair<LPResult, Tableau> simplexEq(Tableau _tableau)
{
size_t const iterations = min<size_t>(60, 50 + _tableau.objective.size() * 2);
size_t const iterations = min<size_t>(120, 50 + _tableau.objective.size() * 2);
for (size_t step = 0; step <= iterations; ++step)
{
optional<size_t> pivotColumn = findPivotColumn(_tableau);
@ -277,7 +277,9 @@ pair<LPResult, Tableau> 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<rational> optimum = solutionVector(_tableau);

64
test/libsolutil/BooleanLP.cpp
View File

@ -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<Expression> vars;
for (size_t i = 0; i < 9; i++)
vars.push_back(variable(string{static_cast<char>('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<Expression> vars;
// for (size_t i = 0; i < 16; i++)
// vars.push_back(variable(string{static_cast<char>('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();
}