I have been trying to solve various magic square problems with SAT solvers, in particular the magic square of squares problem.
Here is one example of the problems I’m trying to solve: Assign distinct integers for a-f on this square. Make it so that all rows, columns and diagonals sum to the same number.
The problem is called the magic square of squares.
It is not known that a solution exists but as of today (2019-03-01) no one has proven it is impossible.
Christian Boyer maintains a website on the topic of magic squares, with a list of unsolved problems in this area. He is offering money and champagne prizes for solving some of the problems.
Despite my efforts, I was not able to find anything new :( No champagne for me. But at least I tried a method (SAT solving) that looks like nobody else tried to use, or if they did they did not document it. In this post, I will show you some details of my miserable failure.
I first heard of this problem by seeing a Numberphile video about magic squares on YouTube. In this video, Matt Parker fails to find a 3x3 magic square of squares and made the Parker square.
I had been dabbling with SAT solvers a bit and while watching that video I though to myself: “Would it not be possible to cast this problem as a boolean satisfiability problem?”.
I searched around and found Boyer’s website on the topic and read about prior efforts into solving these problems. I did not find any explicit mention of someone trying to use a SAT solver on this problem.
That was the point I got hooked in.
SAT stands for boolean SATisfiability problem. Explaining it in full would take many paragraphs, so I say go to the wikipedia page about SAT for detailed information if you would like to learn about it.
In one sentence: SAT is the problem of finding assignments to variables in a boolean formula so that the boolean formula evaluates to true.
SAT is an NP-complete problem. In general, SAT problems are not easy to solve.
Luckily for us, decades of research has gone into developing “SAT solvers” that can often solve large SAT problems anyway, even when the theory says it should not be easy. To solve magic square problems with a SAT solver, we have to turn the magic square problem as a boolean satisfiability problem.
I developed a crude Haskell program that would turn human-readable mathematical problems into SAT problems.
I want to show an example what kind of abstraction level I managed to achieve with this. This is my Haskell DSL for expressing bit-level problems and turning them into SAT problems.
exampleProblem :: Arith () exampleProblem = do -- Specify that we have two 16-bit integers. (unsigned) a <- int 16 "a" b <- int 16 "b" -- Specify that 'a' and 'b' variables are important. -- This just means when my program outputs results, it will only report on -- variables I specified to be the ones I care about. important a important b -- Multiply them together, store result in 'c' c <- mult a b -- Specify that 'a' and 'b' must not be 1. notEq a 1 notEq b 1 -- Specify that 'c' must be 24999 eq c 24999
The above program is trying to solve this problem: find the value of 16-bit integers, a and b, so that a*b=24999 and neither a or b is 1.
My Haskell program outputs a DIMACS file that is then fed to a dedicated SAT solver program. Once the SAT solver finishes (or returns UNSAT, i.e. there is no answer) then my program prints the values of variables I marked as important.
This is a pretty easy example and Lingeling found a solution
a = 641 and
b = 39 almost immediately.
I later learned after I got my first working version of this program working that the general approach of turning bit operations into SAT is called “bit-blasting”. I also used Tseytin transformation to keep the number of variables under control for large computations.
Trying to solve magic squares with SAT and bit-blasting
The approach that I used was this:
Write the magic square problem in terms of the Haskell DSL.
Choose upper bound on number of bits required to express the numbers in the magic square.
Run the Haskell program to generate DIMACS from the problem.
Feed the DIMACS to SAT solver and hope really hard it finds something.
My attempts at finding the 3x3 magic square I presented at the beginning of this post did not work. After about 16 bits the problem starts to take too long to solve even with the best SAT solvers of today.
If we relax the problem so that one or two entries are allowed to be non-squares, then there is this magic square found by Andrew Bremner:
+--------+-------+-------+ | 373^2 | 289^2 | 565^2 | +--------+-------+-------+ | 360721 | 425^2 | 23^2 | +--------+-------+-------+ | 205^2 | 527^2 | 222121| +--------+-------+-------+
The entry on left-middle and bottom-right are non-squares. My SAT solvers were easily able to replicate this, along with many of its rotations and symmetries and scales etc. It takes about 2-3 minutes with MapleSAT or Lingeling.
Unfortunately I could not find any other examples. If there are other magic squares like this, where 2 entries are not squares, I suspect their values are in general much larger. I would have found them otherwise. Indeed, Lee Morgenstern (a researcher who looks like has studied these problems for a while) proved that if a 3x3 magic square exists with all entries being squares, then all entries will be above 10^14..
I don’t know if there are proven lower bounds for squares that have only 7 or 8 squares in them.
I tried looking into different configurations where the two entries that are not squares are at various places inside the square. I found nothing :(
Let limit_v = ((2^11)-1)^2 = 4190209. Let limit_u = ((2^12)-1)^2 = 16769025.
There is no magic square of squares where bottom-right entry and top-left entry are non-squares and all entries are between 0 and limit_u.
There is no magic square of squares where bottom-right entry and top-right entry are non-squares and all entries are between 0 and limit_u.
There is no magic square of squares where top-middle and bottom-middle entry are non-squares and all entries are between 0 and limit_v.
There is no magic square of squares where the bottom-right entry and central entry are non-squares and all entries are between 0 and limit_v.
There is no magic square of squares where the top-middle and central entry are non-squares and all entries are between 0 and limit_v.
These results apply to symmetries and rotations as well.
I think this means there are no other examples besides Bermner’s one where values are in this ballpark.
Other magic square problems
I also tried finding solutions to additive-multiplicative magic squares and bimagic squares. These problems seem much harder for a SAT solver; the number of variables and clauses explodes much faster.
And disappointingly, I again found nothing. (╯°□°）╯︵ ┻━┻
Thoughts about SAT solvers in general
While doing this project, I learned quite a bit about the SAT solving landscape.
These three SAT solvers were fastest with the magic square problems:
I found these by looking at SAT solver competition winners and seeing patterns which solvers tend to rank high.
I’d say the overall winner is Lingeling for magic square problems. Most of the time, Lingeling is the solver that would be fastest at finding a solution. MapleSAT occasionally seemed faster for some experiments. For example MapleSAT seemed quite a lot faster for magic square problems where all operations are modulo some power of two (which was one of my failed experiments). I do not have explanation why.
The SAT solver landscape is evolving so these solvers may not be at the top anymore next year.
There are vast differences between these tools in terms of how convenient they are to use.
Cryptominisat5 is by far the most full-featured in terms of tooling. And it outputs lots of information. It has lots of quality-of-life features. It is most pleasant to use. But is not the fastest, at least not for the problems I was doing. I made use of Cryptominisat5’s XOR implementation for some experiments; the Haskell DSL I wrote is able to emit XOR clauses for some operations (in particular addition of integers). It made the DIMACS files much smaller but it did not significantly improve solving times.
In contrast, MapleSAT, while fast at solving problems, is lacking in all other ways. It does not respond to CTRL+C when I want to interrupt it. MapleSAT does not output any information at all until it finishes. I tried increasing verbosity but all it did was make MapleSAT report when it garbage collects. But it does solve SAT problems pretty fast.
When I first learned long ago how to compile my first Linux kernel I enjoyed looking at compiler messages. I believe SAT solvers should do the same and show me lots of fluff about how they are working hard at the problem :) Cryptominisat5 definitely wins in this category.
Finding magic squares with SAT solvers seems to have been a dead end. As of writing of this, I still have bunch of solvers running on some of problems. I suspect they will never finish. They will run as long as the server I’m running them is up.
If there is a way to make SAT solving faster I would suspect it might be in lemmas. As in, we discover some powerful lemmas we can add to SAT problem as clauses. This might help them prune search space a lot. But I find it hard to say confidently that this would be a promising avenue of research.
If this topic was interesting to you and you want to learn more, here are some of my reading suggestions.
- Christian Boyer’s website is the best magic square site out there. This is where I learned most things I know about magic square problems and existing research.
- Bremner, Andrew. “On squares of squares.” Acta Arithmetica 88.3 (1999): 289-297. This is the person who found the 7 entries out of 9 3x3 magic square I showcased in this post.
- Wikipedia page for SAT
- Cryptominisat5 home page. The author of Cryptominisat5 maintains a blog on that site and for me it was enlightening reading material that helped me understand the SAT solving research landscape a bit.
- SAT solver competition
Some historical key innovations in SAT solving have been DPLL and CDCL. They stand for Davis-Putnam-Logemann-Loveland algorithm and Conflict-Driven Clause Learning.
- For DDPL look for: Davis, Martin; Logemann, George; Loveland, Donald (1962). “A Machine Program for Theorem Proving”. Communications of the ACM. 5 (7): 394–397.
- For CDCL look for: J.P. Marques-Silva; Karem A. Sakallah (November 1996). “GRASP-A New Search Algorithm for Satisfiability”. J. ACM. 7 (3): 201–215.
I wish I could recommend some books but I didn’t read any relevant books for this project so I cannot recommend anything.