  We consider the problem of binary image generation with given properties.
This problem arises in a number of practical applications, including generation
of artificial porous medium for an electrode of lithium-ion batteries, for
composed materials, etc. A generated image represents a porous medium and, as
such, it is subject to two sets of constraints: topological constraints on the
structure and process constraints on the physical process over this structure.
To perform image generation we need to define a mapping from a porous medium to
its physical process parameters. For a given geometry of a porous medium, this
mapping can be done by solving a partial differential equation (PDE). However,
embedding a PDE solver into the search procedure is computationally expensive.
We use a binarized neural network to approximate a PDE solver. This allows us
to encode the entire problem as a logical formula. Our main contribution is
that, for the first time, we show that this problem can be tackled using
decision procedures. Our experiments show that our model is able to produce
random constrained images that satisfy both topological and process
constraints.
