Timezone: »

 
Poster
Learning to Solve SMT Formulas
Mislav Balunovic · Pavol Bielik · Martin Vechev

Tue Dec 04 02:00 PM -- 04:00 PM (PST) @ Room 517 AB #105
in Tue Poster Session B »

We present a new approach for learning to solve SMT formulas. We phrase the challenge of solving SMT formulas as a tree search problem where at each step a transformation is applied to the input formula until the formula is solved. Our approach works in two phases: first, given a dataset of unsolved formulas we learn a policy that for each formula selects a suitable transformation to apply at each step in order to solve the formula, and second, we synthesize a strategy in the form of a loop-free program with branches. This strategy is an interpretable representation of the policy decisions and is used to guide the SMT solver to decide formulas more efficiently, without requiring any modification to the solver itself and without needing to evaluate the learned policy at inference time. We show that our approach is effective in practice - it solves 17% more formulas over a range of benchmarks and achieves up to 100x runtime improvement over a state-of-the-art SMT solver.

Keywords: Reinforcement Learning and Planning · Applications · AutoML
[ Paper]  [ Poster] 

Author Information

Mislav Balunovic (ETH Zurich)
Pavol Bielik (ETH Zurich)
Martin Vechev (DeepCode and ETH Zurich, Switzerland)

Related Events (a corresponding poster, oral, or spotlight)

More from the Same Authors