Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality
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.