Blocking Patterns: Pattern generation through stochastic SAT solving

Alpha Release Version

What are 'blocking patterns'?

Suppose that you have an n x n grid of cells, where each cell must be coloured either black or white.

A blocking pattern is an h x w bitmask, where 1 ≤ h, w ≤ n, which when applied to a subset of our grid, if we have a match between wherever the mask is true and where the grid subset is coloured black, then the entire grid subset must be coloured black.

For example, suppose we have the blocking pattern [[1, 0], [0, 1]]. When we overlay the mask on our grid, over the cells (i, j), (i, j + 1), (i + 1, j) and (i + 1, j + 1), we get that if two diagonally opposite cells (i, j) and (i + 1, j + 1) are coloured black, then so must be the cells (i, j + 1) and (i + 1, j).

Hence the name blocking pattern - a pattern which when matched, forces an entire black coloured block to be drawn.

If we think of the colours black and white as true and false respectively, and the variable x_{(i, j)} refers to the truth value associated with the cell (i, j), we can translate this blocking pattern into an implication:

( x_{i, j} ∧ x_{i + 1, j + 1} ) ⇒ ( x_{i, j + 1} ∧ x_{i + 1, j} )

In general, one can translate a set of blocking patterns into a number of implications for each valid position where the bitmask can be overlayed. Our goal is to generate a colouring of our grid such that this list of implications is satisfied.

Example:

Considering a 16 x 16 grid and applying the two complementary blocking patterns

[[1, 0], [0, 1]] and [[0, 1], [1, 0]]

we get the following valid cell colouring:

Installation

This utility requires the ALLLSatisfiabilitySolver library to be installed, which is available at https://github.com/xmif1/ALLLSatisfiabilitySolver.

Once installed, clone this repository and cd into the project directory. Then run:

1. mkdir ./build
2. cd ./build
3. cmake ..
4. make