Trying to bridge the gap between WFC “Even Simpler Tiled Model” and CSP propositional rules

Photo by Ross Sneddon on Unsplash

“Even Simpler Tiled Model” (ESTM) leads to an interesting question about rules properties (article also posted on: https://dev.to/antigones/trying-to-bridge-the-gap-between-wfc-even-simpler-tiled-model-and-constraint-satisfaction-problem-csp-propositional-rules-1oka)

Recently I tried to implement my own version of “Even Simpler Tiled Model” — a simplified version of Wave Function Collapse algorithm (source: https://github.com/antigones/py-wfc-estm) as explained in this page.

“Even Simpler Tiled Model”, just like Wave Function Collapse, can be for example used to generate maps out of a set of rules. The idea is that it is possible to formalize those rules from a sample map and then use them to generate a new one, “propagating” reasoning about admissible/unadmissible values from tile to tile.

Playing with my own implementation, a question arose: what defines a rule making a map difficult to collapse, when applying the Wave Function Collapse algorithm in its “Even Simpler Tiled Model” (ESTM) simplified form?
Trying to answer this question, I ended up fallbacking the model to a propositional logic rules-related question and trying to formalize “Even Simpler Tiled Model” as a set of propositional logic rules.
I took a sample map, defined as follows:

img = [
          'LLLLLLLLLL',
          'LLLLLLLLLL',
          'LLLLLLLLLL',
          'LLLLLLLLLL',
          'LLLLLCLLCC',
          'LLLLCSCCSS',
          'LLLCSSSSSS',
          'LLCSSSSSSS',
          'LCSSSSSSSS',
          'CSSSSSSSSS'
      ]

Analyzing the sample map, the following rules came out:

{
    'L': {
        (1, 0): {'L', 'C'}, 
        (0, 1): {'L', 'C'}, 
        (0, -1): {'L', 'C'}, 
        (-1, 0): {'L'}
    }, 

    'C': {
        (-1, 0): {'L'}, 
        (0, -1): {'S', 'L', 'C'}, 
        (1, 0): {'S'}, 
        (0, 1): {'S', 'L', 'C'}
    }, 

    'S': {
         (-1, 0): {'S', 'C'}, 
         (0, -1): {'S', 'C'}, 
         (1, 0): {'S'}, 
         (0, 1): {'S', 'C'}}
     }
}

The rules informally state the following (see map at the beginning of this post):

• a Land can have a Land at North, East, South, West; Coast in the East, West, South
• Sea can have Coast or Sea in the North, Sea in the South, Coast or Sea at East and West
• Coast must have Land in the North; can have Land or Coast and East and West; must have Sea at south

Let’s rewrite this set of rules as a set of logic propositions.
To accomplish this task and to be sure not to forget a rule, I wrote my own model checker using SymPy.

An 1x2 sized world

Since we have to rewrite the rules for each and every cell in the map, we first consider a 1x2 sized world.
In this world, we define:

L_00, “there is a land in (0,0)”
C_00, “there is a coast in (0,0)”
S_00, “there is sea in (0,0)”

L_10, “there is a land in (1,0)”
C_10, “there is a coast in (1,0)”
S_10, “there is a sea in (1,0)”

And the rules as:

{
    C_00: S_10 & ~C_10 & ~L_10, 
    C_10: L_00 & ~C_00 & ~S_00, 

    L_00: ~S_10 & (C_10 | L_10), # a Land in (0,0) only admit a C or a L in (1,0), does not admit Sea
    L_10: L_00 & ~C_00 & ~S_00, 

    S_00: S_10 & ~C_10 & ~L_10, 
    S_10: ~L_00 & (C_00 | S_00)

    (C_00 | L_00 | S_00), # you have to choose at least a value
    (C_10 | L_10 | S_10)
}

(where “:” stands for “if and only if”)

To have a “valid” world map (i.e. a map respecting all the defined rules) we can only choose a set of truth values assignment satisfying all the rules (a model).
The model checker prints all the assignments satisfying all the rules.

For this small world, we have the two following models:

Reading the first row in the truth table, we can see that choosing Land in (0,0) pushes a Coast or a Land in (1,0). This gives us two perfectly valid maps in just one row:

L
C

or

L
L

Reading the second row in the truth table, we can see that choosing a Sea or a Coast in (0,0) only pushes a Sea in (1,0):

CS
S

leading to the two (both valid) maps:

C
S

and

S
S

A 2x2 map

We can extend reasoning for maps of size beyond 1x2. Let’s consider a 2x2 world map.
We can again write the propositional ruleset:

{
    C_00: S_10 & ~C_10 & ~L_10 & (C_01 | L_01 | S_01), 
    C_01: S_11 & ~C_11 & ~L_11 & (C_00 | L_00 | S_00), 
    C_10: L_00 & ~C_00 & ~S_00 & (C_11 | L_11 | S_11), 
    C_11: L_01 & ~C_01 & ~S_01 & (C_10 | L_10 | S_10), 

    L_00: ~S_01 & ~S_10 & (C_01 | L_01) & (C_10 | L_10), 
    L_01: ~S_00 & ~S_11 & (C_00 | L_00) & (C_11 | L_11), 
    L_10: L_00 & ~C_00 & ~S_00 & ~S_11 & (C_11 | L_11), 
    L_11: L_01 & ~C_01 & ~S_01 & ~S_10 & (C_10 | L_10), 

    S_00: S_10 & ~C_10 & ~L_01 & ~L_10 & (C_01 | S_01), 
    S_01: S_11 & ~C_11 & ~L_00 & ~L_11 & (C_00 | S_00), 
    S_10: ~L_00 & ~L_11 & (C_00 | S_00) & (C_11 | S_11), 
    S_11: ~L_01 & ~L_10 & (C_01 | S_01) & (C_10 | S_10),

    (C_00 | L_00 | S_00),
    (C_01 | L_01 | S_01),
    (C_10 | L_10 | S_10),
    (C_11 | L_11 | S_11)
}

and use the model-checker to determine models:

We have four models here.
Let’s choose S in (1,1) — filtering all the models having S_11 to True:

The truth table suggests the following situation:

Let’s choose L in (0,0):

The truth table evolves the map to the following one:

which is valid.

If we take a step back and choose S in (0,0) then we have:

which leads to the following (equivalent) set of maps:

which can be “unraveled” as the following four maps:

Going up, 3x3 maps

Using the model checker to generate/check rules for a 3x3 map, we obtain the following models:

Let’s choose L for (2,2), to observe propagation as rule inference:

Leading to the map:

which shows propagation of Land values across the tiles!

Let’s choose L in (2,0) — and note that it is interchangeable with a Coast:

This gives two valid maps, where there is no difference in putting a Land or a Coast in (2,1):

A “very difficult” map

Let’s stress things and consider the following sample map:

img_hard = [
               'KB',
               'SB',
           ]

and again, let’s write out the rules as logic proposition:

{
    B_00: B_10 & ~B_01 & ~K_01 & ~K_10 & ~S_01 & ~S_10, 
    B_01: B_11 & ~B_00 & ~K_11 & ~S_11 & (K_00 | S_00), 
    B_10: B_00 & ~B_11 & ~K_00 & ~K_11 & ~S_00 & ~S_11, 
    B_11: B_01 & ~B_10 & ~K_01 & ~S_01 & (K_10 | S_10), 

    K_00: B_01 & S_10 & ~B_10 & ~K_01 & ~K_10 & ~S_01, 
    K_01: S_11 & ~B_00 & ~B_11 & ~K_00 & ~K_11 & ~S_00, 
    K_10: B_11 & ~B_00 & ~K_00 & ~K_11 & ~S_00 & ~S_11, 
    K_11: ~B_01 & ~B_10 & ~K_01 & ~K_10 & ~S_01 & ~S_10, 

    S_00: B_01 & ~B_10 & ~K_01 & ~K_10 & ~S_01 & ~S_10, 
    S_01: ~B_00 & ~B_11 & ~K_00 & ~K_11 & ~S_00 & ~S_11, 
    S_10: B_11 & K_00 & ~B_00 & ~K_11 & ~S_00 & ~S_11, 
    S_11: K_01 & ~B_01 & ~B_10 & ~K_10 & ~S_01 & ~S_10,

    (B_00 | K_00 | S_00),
    (B_01 | K_01 | S_01),
    (B_10 | K_10 | S_10),
    (B_11 | K_11 | S_11)    
}

The model checker only returns 1 model:

the only admissible solution.

For a 3x3 map with the “hard” rules, we obtain UNSAT and the map cannot collapse.