#TALOS PRINCIPLE WORLD 2 PUZZLES CODE#
#TALOS PRINCIPLE WORLD 2 PUZZLES TRIAL#

When generating these equations one has to be careful not to include rotated sigils that stick out of the frame, though.Īlthough 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.

#TALOS PRINCIPLE WORLD 2 PUZZLES CODE#

In the same way, when rotated right, we needĪll these options have to be disjunctively connected, in SMT code for the case where the anchor lies at (4,2).

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

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.

choose for each sigil form an anchor point.

Of course the most important part are the defining equations for the various sigils. Or in SMT code for a 6×6 frame and the first sigil: (assert (or x_1_1_n x_1_2_n. This can be done easily by assuming that for each sigil, at least one of the tiles is assigned to it: Since all sigils together exactly fill the frame, this is enough. The better idea was to say that every sigil was used at least once.

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. So if a sigil occupies 4 tiles, then every combination of 5 tiles needs to evaluate to false. 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. This can be achieved by asserting for each tile and each pair of different sigil (numbers), that not both of the two hold: In the SMT2 code it would look like (assert (or x_i_j_1 x_i_j_2. Let us go through them one by one: Every field has at least on sigil on it

defining equations for the sigil’s form.

every field has at most one sigil on it.

every field has at least one sigil on it.

We have to state relations between these propositional variables to obtain a proper solution, in particular we have added the following statements: 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). That is, we have variable (encoded as x_i_j_n) where runs over the cells of the frame, and over the (numbered) sigils.

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

#TALOS PRINCIPLE WORLD 2 PUZZLES TRIAL#

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. And soon I got stuck at these kind of puzzles where one has to fit in pieces into a frame. After my last post on Portal, there was a sale of The Talos Principle, so I got it and started playing.

Talos principle world 2 puzzles