Searching expressions

During a coffee break at work, the following brainteaser came up:

0 0 0 = 6
1 1 1 = 6
2 2 2 = 6
3 3 3 = 6
4 4 4 = 6
5 5 5 = 6
6 6 6 = 6
7 7 7 = 6
8 8 8 = 6
9 9 9 = 6
10 10 10 = 6

For each row, one is supposed to fill in the operators that make the expression true. One is not allowed to add more digits, of course. The allowed operators are the arithmetic operators, exponentiation, square root, and factorial. For example, we have:

(1 + 1 + 1)! = 6
3 * 3 - 3 = 6

We solved 0 through 10, but struggled with 11. We also wondered whether there were some interesting solutions for 0-10 that we had missed.

I have been intrigued by symbolic programming and automated theorem proving since I first read about it. This seemed like a simple enough problem to start exploring those subjects. The first obstacle, which proved to be the most difficult one in the end, was conceptual blocks on my part. From proving mathematical theorems in university, I'm used to feeling that at each step in the derivation, there is an "infinite" number of possible moves, if only one is creative enough.

Tokens. x, y (numbers)
Unary operator. U: x -> y
Merge operator. M: x, y -> z

Example
State: [x, y, z]
Applied operation: M1 ('add'), index 0
Results: [M0(x, y), z] = [x+y, z]

Searching through expressions
However, if we want to do a systematic search in the computer, we need to be able to enumerate the possible moves. In our case, we have restricted ourselves to a finite number of operators, and there is a finite number of tokens to apply them to. So the number of moves in each step is not only enumerable, but finite. My idea for looking for an answer here is to simply do exhaustive search, using BFS (breadth-first search). Breadth-first search should help us find one valid solution quickly (if we assume that there is at least one relatively simple solution). However, if we want to find all solutions, it doesn't really matter which search algorithm is used, as we will have to go through all states anyway.

The really important thing is termination conditions. I pruned all states which had at least one token which was not a real integer. I also pruned all states with an integer larger than 1000.

Implementation
The search can be done very conveniently using networkx. The states are represented as nodes (the key is a tuple of the tokens). The edges are directed, and each edge has a feature with a representation of the operation. This help verify correctness, and display the result.

Another question is how to return solutions. First, I tried to return all simple paths from the starting stated to the goal state. For x=9, this gave over 17000 solutions. Clearly a lot of them were the same up to permutation. I decided to return one solution per immediate predecessor to the target state. For each immediate predecessor, I return the shortest path in the search graph. This brought down the number of solutions to no more than a few 10's at most.

Results
The resulting successful computations can be plotted using graphviz via pydot. Installed through:

apt-get install graphviz
pip3 install pydot




Some examples. The _index suffixes are there because pydot doesn't accept custom labels.

The only solution found for 1.

One of two solutions found for 8.

One of 22 solutions found for 9.

The searcher found many solutions that I hadn't thought about, however most were not very interesting. I ran it for numbers up to 1000, and sadly there was not a lot of surprises. Going back to the problem we had in the beginning, it did not find a solution for 11. The workable numbers up to 1000 are typically very even numbers. The highest workable I found was 729, which goes through 81:

Path from 729. which goes through [729, 729, 729]->[27, 27, 27]->81->9->3->6.

The highest workable prime found is 37, which goes through 36:

Conclusion
This was a very fun exercise and it yielded successful results quickly, even if it was not so surprising. It should be noted that we're relying on numerical answers here as opposed to having an exact representation of numbers. This works well for integers, but wouldn't generalize to reals.