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:
As most distributions have switched to systemd as default "init", some
people have asked why we actually keep sysvinit around, as it's old and
crusty, and systemd can do so much more.
My answer is: systemd and sysvinit solve entirely different problems, and
neither can ever replace the other fully.
The big argument in favour of systemd is integration: when you keep
everything in one process, it is easy to make sure that components talk to
each other. That is nice, but kind of misses the point: integration could
be done via IPC as well, and systemd uses a lot of it to separate
privileges anyway.
The tighter integration comes from something else: the configuration
format. Where sysvinit uses a lot of shell scripts ("imperative" format),
systemd uses explicit keywords ("descriptive" format), and this is the
important design decision here: descriptive formats cannot do anything
unanticipated, neither good nor bad.
This is important for UI programmers: if there is a button that says "if I
close the lid switch, suspend the laptop", then this needs to be connected
to functionality that behaves this way, and this connection needs to work
in both directions, so the user will find the active setting there when
opening the dialog. So, we need to limit ourselves to a closed set of
choices, so the UI people can prepare translations.
This is the design tradeoff systemd makes: better integration in exchange
for less flexibility.
Of course, it is simple to allow "custom" actions everywhere, but that
starts to break the "well-integrated" behaviour. There is an old blog
post
from Joey Hess about how to implement a simple alarm clock, using systemd,
and this shows both how powerful and how limited the system is.
On one hand, the single line 
In case you ever wanted to look at 
Here is my monthly update covering a large part of what I have been doing in the free software world (
Is your table a mess of wires? Do you have multiple devices connected via serial and can't remember which is /dev/ttyUSBX is connected to what board? Unless you are a embedded developer, you are unlikely to deal with serial much anymore - In that case you can just jump to the next post in your news feed. Introducting ser2netUsually people start with minicom for serial access. There are better tools - picocom, screen, etc. But to easily map multiple serial ports, use 
First I tried to find a sensible Debian package to record the
battery status, assuming that this must be a problem already handled
by someone else. I found
