From 29be0d23f631c2089e87cece01d3f53d7560aa55 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 23 Feb 2022 19:04:08 +0100
Subject: [PATCH] Enable magic squares 4

---
 libsolutil/CDCL.cpp           |  2 ++
 test/libsolutil/BooleanLP.cpp | 49 ++++++++++++++++++-----------------
 2 files changed, 27 insertions(+), 24 deletions(-)

diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index a2ba3ba29..f72b53e05 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -79,6 +79,8 @@ optional<CDCL::Model> CDCL::solve()
 		{
 			if (auto variable = nextDecisionVariable())
 			{
+				cout << "Level " << currentDecisionLevel() << " - ";
+				cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
 				m_decisionPoints.emplace_back(m_assignmentTrail.size());
 //				cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;
 				enqueue(Literal{false, *variable}, nullptr);
diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp
index 2bfd1c0f8..eae7b2818 100644
--- a/test/libsolutil/BooleanLP.cpp
+++ b/test/libsolutil/BooleanLP.cpp
@@ -279,30 +279,31 @@ BOOST_AUTO_TEST_CASE(magic_square_3)
 	});
 }
 
-// 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(magic_square_4)
+{
+	vector<Expression> vars;
+	for (size_t i = 0; i < 16; 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 <= 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] == sum);
+	for (size_t i = 0; i < 16; i += 4)
+		solver.addAssertion(vars[i] + vars[i + 1] + vars[i + 2] + vars[i + 3] == sum);
+	solver.addAssertion(vars[0] + vars[5] + vars[10] + vars[15] == sum);
+	solver.addAssertion(vars[3] + vars[6] + vars[9] + vars[12] == sum);
+	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"}
+	});
+}
+
+// Magic squares 5 takes almost 2 minutes.
 
 BOOST_AUTO_TEST_CASE(boolean_complex_2)
 {