The Talos Principle – Solving puzzles using SAT solvers

After my last post on Portal, there was a sale of The Talos Principle, so I got it and started playing. And soon I got stuck at these kind of puzzles where one has to fit in pieces into a frame. As a logician I hate to solve something by trial and error, so I decided I write a solver for these kind of puzzles, based on a propositional logic encoding and satisfiability solver. Sometimes it is good to be logician!

In the Talos Principle, access to new worlds and specific items is often blocked by gates that open by putting Sigils into the frame. Of course, collecting the sigils is the most challenging part, but that is often solvable by logical thinking. On the other hand, solving these fitting puzzles drove me crazy, so let us solve them with a SAT solver.

Encoding

I used a propositional encoding that for each combination of cells and sigils assigns a propositional variable, which is true if the specific sigil rests in on that cell in the final solution. That is, we have variable (encoded as x_i_j_n) where runs over the cells of the frame, and over the (numbered) sigils.

Setup

I have written a perl program that for a definition of a puzzle (see later), outputs SMT2 code, which then is checked for satisfiability and generation of model with the z3 solver (which is available in Debian).

Necessary assertions

We have to state relations between these propositional variables to obtain a proper solution, in particular we have added the following statements:

• every field has at least one sigil on it
• every field has at most one sigil on it
• every sigil is used at least once
• defining equations for the sigil’s form

Let us go through them one by one:

Every field has at least on sigil on it

That is an easy part by asserting

In the SMT2 code it would look like

(assert (or x_i_j_1 x_i_j_2 ... x_i_j_n))

Every field has at most one sigil on it

This can be achieved by asserting for each tile and each pair of different sigil (numbers), that not both of the two hold:

and in SMT2 code:

(assert (and
  (not (and x_1_1_1 x_1_1_2))
  (not (and x_1_1_1 x_1_1_3))
...
(assert (and
  (not (and x_1_2_1 x_1_2_2))
  (not (and x_1_2_1 x_1_2_3))
...

Every sigil is used at least once

This was a bit a tricky one. First I thought I want to express that every sigil is used exactly once by excluding that for one sigil there are more fields assigned to it then the sigil contains parts. So if a sigil occupies 4 tiles, then every combination of 5 tiles needs to evaluate to false. But with 8×8 or so frames, the number of combinations simply explodes to above several million, which brings my harddrive size and z3 to an end.

The better idea was to say that every sigil was used at least once. Since all sigils together exactly fill the frame, this is enough. This can be done easily by assuming that for each sigil, at least one of the tiles is assigned to it:

or in SMT code for a 6×6 frame and the first sigil:

(assert (or x_1_1_n x_1_2_n ...  x_6_6_1))

Defining equations for the sigil’s form

Of course the most important part are the defining equations for the various sigils. Here I choose the following path:

• choose for each sigil form an anchor point
• for each tile in the frame and each sigil, put the anchor of the sigil on the tile, and express the 4 directions of rotation

So for example for the top-most sigil in the above photo, I choose the anchor point to be the center, and if that was in , I need to assume that for the upright position

holds. In the same way, when rotated right, we need

All these options have to be disjunctively connected, in SMT code for the case where the anchor lies at (4,2).

(assert (or
  ...
  (and x_3_2_n x_4_2_n x_5_2_n x_4_3_n)
  (and x_3_3_n x_3_2_n x_3_1_n x_4_2_n)
  (and x_3_2_n x_4_2_n x_5_2_n x_4_1_n)
...

When generating these equations one has to be careful not to include rotated sigils that stick out of the frame, though.

Although the above might not be the optimal encoding, the given assertions suffice to check for SAT and produce a model, which allows me to solve the riddles.

Implementation in Perl

To generate the SMT2 code, I used a Perl script, which is very quickly hacked together. The principle function is (already coded for the above riddle):

create_smt2_def(8,6,'a','a','b','cl','cl','cr','cr','cr','q','q','sl','sl');

where the first two arguments define the size of the frame, and the rest are codes for sigil types:

• a podest, the first sigil in the above screen shot
• b stick, the third sigil above, the long stick
• cl club left, the forth sigil above, a club facing left
• cr club right, the sixth sigil above, a club facing right
• q square, the ninth sigil above
• sl step left, the last sigil in the above image
• sr step right, mirror of step left (not used above)

This function first sets up the header of the smt2 file, followed by shipping out all the necessary variable definitions, in SMT these are defined as Boolean functions, and the other assertions (please see the Perl code linked below for details). The most interesting part are the definitions of the sigils:

  # for each piece, call the defining assertions
  for my $n (1..$nn) {
    my $p = $pieces[$n-1];
    print "(assert (or\n";
    for my $i (1..$xx) {
      for my $j (1..$yy) {
        if ($p eq 'q') { 
          type_square($xx,$yy,$i,$j,$n); 
        } elsif ($p eq 'a') {
          type_potest($xx,$yy,$i,$j,$n);
    ....

Every sigil type has its own definiton, in case of the a podest, the type_podest function:

sub type_potest {
  my ($xx,$yy,$i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i - 1; $ir = $i + 1; $iu = $i;
  $jl = $jr = $j; $ju = $j + 1;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}

This function is prototypical, one defines the tiles a sigil occupies if the anchor is placed on (i,j) for an arbitrary orientation of the sigil, and then calls do_rotate_shipout on the list of occupied tiles. This function in turn is very simple:

sub do_rotate_shipout {
  my ($xx,$yy, $i, $j, $n, @pairs) = @_ ;
  for my $g (0..3) {
    @pairs = rotate90($i, $j, @pairs);
    check_and_shipout($xx,$yy, $n, $i, $j, @pairs);
  }
}

as it only rotates four times by 90 degrees, and then checks whether the rotated sigil is completely within the frame, and if yes ships out the assertion code. The rotation is done by multiplying the vector from (i,j) to the tile position with the (0 -1 1 0) matrix and adding it again to (i,j):

sub rotate90 {
  my ($i, $j, @pairs) = @_ ;
  my @ret;
  while (@pairs) {
    my $ii = shift @pairs;
    my $jj = shift @pairs;
    my $ni = $i - ($jj - $j);
    my $nj = $j + ($ii - $i);
    push @ret, $ni, $nj;
  }
  return @ret;
}

There are a few more functions, for those interested, the full Perl code is here: tangram.pl. There is no user interface or any config file reading done, I just edit the source code if I need to solve a riddle.

Massaging the output

Last but not least, the output of the z3 solver is a bit noisy, so I run the output through a few Unix commands to get only the true assignments, which gives me the location of the tiles. That is, I run the following pipeline:

perl tangram.pl | z3 -in | egrep 'define-fun|true|false'  | sed -e 'h;s/.*//;G;N;s/\n//g' | grep true | sort

which produces a list like the following as output:

  (define-fun x_1_1_10 () Bool    true)
  (define-fun x_1_2_10 () Bool    true)
  (define-fun x_1_3_5 () Bool    true)
  (define-fun x_1_4_6 () Bool    true)
  (define-fun x_1_5_6 () Bool    true)
  (define-fun x_1_6_6 () Bool    true)
  (define-fun x_2_1_10 () Bool    true)
  (define-fun x_2_2_10 () Bool    true)
  (define-fun x_2_3_5 () Bool    true)
  ...

from which I can read up the solution that puts the tenth sigil (a square) in the lower left corner: