Constrained image generation using binarized neural networks with decision procedures