I've stumbled upon this weird minetest map, can you make sense out of it?
Minetest + mesecons required
Non-standard flag format (enter bits as 0 and 1).
The task is a Minetest (Something like Minecraft) map, and it looks like this:
A HUUUUUUUUUUUUGE redstone circuit.
- Parse the map database.
- Dump all mesecons blocks' type, orientation, and position.
- Simplify all interconnections.
- Solve the boolean expression with z3.
There's a file named
map.sqlite. Clearly, this is what we want.
Open it with sqlite3, and there's only one table inside.
sqlite> .schema CREATE TABLE `blocks` ( `pos` INT PRIMARY KEY, `data` BLOB );
The file format is well documented in here.
In minetest, a voxel (i.e. a basic cube in the game) is called a "node". And 16x16x16 nodes is grouped into one block (i.e. a SQL record).
pos field is a 36-bits compressed integer contains 3 12-bits integers.
data field contains some metadata of the block and a zlib compressed array about each nodes.
I won't put format details here. Just follow its document to write a parser.
There's a lot of blocks only contains
ignore nodes. Instead of parse whole database, I only parse the mesecons-related blocks with this query:
SELECT pos, data FROM blocks WHERE instr(data, "mesecons") > 0;
You can find the parser from here
Here's a all the blocks I parsed:
air default:stone mesecons_insulated:insulated_on mesecons_insulated:insulated_off mesecons_extrawires:crossover_01 mesecons_extrawires:crossover_10 mesecons_extrawires:crossover_on mesecons_extrawires:crossover_off mesecons_extrawires:corner_on mesecons_extrawires:corner_off mesecons_extrawires:tjunction_on mesecons_extrawires:tjunction_off mesecons_gates:xor_on mesecons_gates:xor_off mesecons_gates:or_on mesecons_gates:or_off mesecons_gates:and_on mesecons_gates:and_off mesecons_gates:not_on mesecons_gates:not_off mesecons_lamp:lamp_off mesecons_walllever:wall_lever_off
And the lamp is in
(1, 2, 1938), which looks like:
Each node has two parameters, after comparing to the rendered result in the game. I figure out one of the parameters is its orientation.
When orientation is zero, all gates and wire points to the east (i.e. +x direction), corner looks like ┐, and tjunction looks like T.
Orientation 1 rotates 90° clock-wise, 2 rotates 180° clock-wise, 3 rotates 270° clock-wise.
Now, we are ready to reconstruct the circuit.
Simplify the circuit
In each nodes, there are four connection pins:
- (x - 0.5, y)
- (x + 0.5, y)
- (x, y - 0.5)
- (x, y + 0.5)
And I do the following things to reconstruct the circuit
- Create an edge list for each pins according to the node type and orientation.
- Simplify the edges by finding connected components.
- Remove those unconnected pins
- Sort the gates topologically. (The circuit in this task is a DAG)
Now it looks like:
type out inputs ('lever_0', 0, [ ]), ('lever_1', 1, [ ]), ('lever_2', 2, [ ]), ('lever_3', 3, [ ]), ... ('lever_37', 37, [ ]), ('lever_38', 38, [ ]), ('lever_39', 39, [ ]), ('not', 40, [34 ]), ('not', 41, [31 ]), ('not', 42, [30 ]), ... ('and', 3356, [3348, 3355]), ('and', 3357, [1274, 3353]), ('or', 3358, [3357, 1125]), ('and', 3359, [3358, 3356]), ('lamp', None, [3359 ])
While I was trying to understand the circuit with graphviz, my teammate found the solution with z3 solver.
He converted the constraint above to the following code using some regex:
from z3 import * v_0 = Bool('lever_0') v_1 = Bool('lever_1') v_2 = Bool('lever_2') ... v_37 = Bool('lever_37') v_38 = Bool('lever_38') v_39 = Bool('lever_39') v_40 = Not( v_34 ) v_41 = Not( v_31 ) v_42 = Not( v_30 ) ... v_3356 = And( v_3348, v_3355 ) v_3357 = And( v_1274, v_3353 ) v_3358 = Or( v_3357, v_1125 ) v_3359 = And( v_3358, v_3356 ) print("Solving") print(solve(v_3359, True))
Run it, and you'll get the flag.