Constrained Image Generation Using Binarized Neural Networks with Decision Procedures

TL;DR

This paper introduces a novel approach to generate binary images with specific properties by approximating PDE solutions with neural networks and employing decision procedures for constrained image synthesis.

Contribution

It is the first to demonstrate that constrained binary image generation can be formulated and solved using decision procedures with neural network approximations of PDEs.

Findings

Successfully generated images satisfying topological constraints

Neural network approximation reduces computational cost of PDE solving

Decision procedures effectively handle complex constraints

Abstract

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.