Power concatenation

The following program finds power concatenations for square numbers. For example, 16 and 9 are both square numbers and their concatenation is 169, which is also square.

function main () {
  int11 a, b, c;

  a = a.square;
  b = b.square;
  c = c.square;

  invariant a.concatenate(b) == c;
  invariant [a, b, c].all?(*positive?);
  invariant c < 1000000;

  expose a, b, c;
};

function concatenate (a, b) {
  return multiplier(b) * a + b;
};

function multiplier (n) {
  multiplier = (n < 10).if(10, # ten
               (n < 100).if(100, # hundred
               (n < 1000).if(1000, # thousand
               (n < 10000).if(10000, # ten thousand
               (n < 100000).if(100000, # hundred thousand
               (n < 1000000).if(1000000, # million
                -1))))));

  invariant multiplier != -1;

  return multiplier;
};

main();

Sentient finds all 29 solutions up to one million in about 40 seconds. The smallest and largest three solutions are given below:

Smallest:
"4" + "9" = "49" (roots: 2, 3, 7)
"16" + "9" = "169" (roots: 4, 3, 13)
"36" + "1" = "361" (roots: 6, 1, 19)

Largest:
"81" + "9025" = "819025" (roots 9, 95, 905)
"9" + "50625" = "950625" (roots 3, 225, 975)
"9" + "70225" = "970225" (roots 3, 265, 985)

How does it work?

We declare three integers and square them. This has the effect that a, b and c will be square numbers. We then concatenate ‘a’ with ‘b’ and specify an invariant that the result is equal to ‘c’. The call to ‘concatenate’ uses Sentient’s method syntax.

The ‘concatenate’ function works by calculating a ‘multiplier’, which is the number of decimal places to shift ‘a’ to the left before adding ‘b’ to the result. This ‘multiplier’ is determined by a nested conditional that considers the value of ‘b’. The invariant ensures we haven’t fallen off the end of the conditional which is the case when ‘b’ is too large.

The ‘main’ function finishes by specifying a couple more invariants. The first rules out trivial solutions (e.g. “0” + “9” = “9”). The second reinforces the limit of one million that could be exceeded in ‘c’ as a result of the concatenation. Finally, we expose a, b and c.

CLI example

Here is an example of running this program with the command-line interface:

sentient --run power-concatenation.json --machine riss --number 3

# standard output:
{"a":4,"b":900,"c":4900}
{"a":4,"b":225,"c":4225}
{"a":4,"b":2025,"c":42025}

The riss solver seems noticeably faster than the others at this problem.