Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality [closed]

Question

The original problem of Domino Tiling and Wang Tile has great theoretical interest on computability theory... However, the great emerging problem on application of Wang Tile in material science and physics requires the tiling to satisfy one more condition:

The tiling should satisfy some proportionality, say, Tile 1 should appear with frequency 1/16, Tile 2 with frequency 9/16, Tile 3 with 6/16, Tile 4 with frequency 0...

The most important decision problem is the following: Could a given set of Tile tile a grid of size NxN satisfying the frequency constraint within a error of +-epsilon.

For example: could the set {Tile 1, Tile 2, Tile 3, Tile 4} tile the NxN grid with frequency 1/16+-0.01, 9/16+-0.01, 6/16+-0.01, 0+-0.01 respectively....

From one of my previous post:

Algorithms for NP complete problem

I realize the decision problem of tiling without such constraint could be modeled by SAT... With this constraint the problem becomes ridiculously difficult and I eagerly seek for solutions towards this finite decidable problem.... (we could forget epsilon for a moment if the problem with epsilon is too hard)...

So here is the question: how do we model this problem in MIP or SAT or any other optimization algorithm?

For more detail why this problem is practical in material science and physics, see my previous post:

coloring in lattice

reference for wang tile

Computational approach deciding whether a set of Wang Tile could tile the space up to some size

P.S. this is a bounty question from mathoverflow without yet a applicable solution...

Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality

Answer 1

Use a SAT solver that also allows you to express pseudo-Boolean constraints.

Encoding the verification of the existence of the tiling of an NxN grid as a CNF formula is straightforward. Each grid position will have a set of variables associated with it of which only one will be set true if a particular tile occupies that position. Add clauses that force exactly one of each set of variables to be set true. Add other clauses that demand grid neighbors be the correct sort of tile out of the available choices.

The epsilon requirement means requiring that only a fixed number of the grid position variables for each tile type be set true, or that the number set be within a certain range. This is complicated by the fact that the naive expression of such constraints in CNF takes a number of clauses exponential in the number of variables involved. There are more efficient encodings that involve adder and comparison circuits, but a solver that accepts pseudo-Boolean constraints directly will either work without such encodings or will save you the trouble of creating these circuit encodings yourself.