How to guess the maximum of a functionHow to guess the maximum of a function

Verification of the safety and security of programs and even synthesis made a lot of progress over the last decades, but we are still mostly limited to solving decision problems. Quantitative versions of these problems, such as finding an _optimal_ program satisfying a given specification, are still considered to be a big challenge. What makes these problems hard is that the solution space is exponentially large, evaluating the quality of a single point can be hard, and that gradients are not very informative (comparing the quality of two programs does not tell us much about where to search for an even better program). In this talk I will present a new algorithm that overcomes these challenges in a refreshing way: We encode the problem as a Boolean formula and draw a random model from the solution space, which is guaranteed to be likely close to the maximum. I will first review recent progress in approximate model counting that allows us to draw random solutions and then I will show how a simple transformation on Boolean formulas allows us to increase the likelihood of drawing 'good' solutions. We implemented and evaluated the algorithm and showed that we can effectively solve problems from program synthesis and security that couldn't be solved with any existing approach.

The corresponding paper is "Maximum Model Counting" published at AAAI 2017 together with Sanjit A. Seshia and Daniel J. Fremont.