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


closed as unclear what you're asking by D.W., Raphael Apr 11 '14 at 6:41

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ So what's your question? I can't find a question in your post. $\endgroup$ – D.W. Apr 11 '14 at 5:18
  • $\begingroup$ That, and it's formatted horribly. Please use LaTeX for maths and markdown to e.g. make links nicer. $\endgroup$ – Raphael Apr 11 '14 at 6:41
  • $\begingroup$ I edited the format and added the explicit question, could i remove my hold? $\endgroup$ – user40780 Apr 11 '14 at 12:26
  • 1
    $\begingroup$ Your edit says that this is a cross-post from another Stack Exchange site, where the question has a bounty attached to it. Cross-posting is explicitly against our site policy, because it wastes people's time when they answer questions that already have answers elsewhere, and it fragments answers. So, no, this should stay closed. $\endgroup$ – David Richerby Apr 11 '14 at 17:49
  • $\begingroup$ the problem why i need to cross post is that no practical solution is achieved in MO for a long time and here I believe better answer could be achieved... $\endgroup$ – user40780 Apr 11 '14 at 19:27

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.

  • $\begingroup$ Yup. Or, use ILP. $\endgroup$ – D.W. Apr 11 '14 at 5:19
  • $\begingroup$ SMT solvers also avoid the exponential blowup by representing range constraints implicitly, as do constraint solvers. But combinatorial optimization problems of this kind are generally hard for all existing solvers. $\endgroup$ – András Salamon Apr 11 '14 at 22:11

Not the answer you're looking for? Browse other questions tagged or ask your own question.