Learning to Solve SMT Formulas
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 100× runtime improvement over a state-of-the-art SMT solver.
Thank you for the detailed rebuttal! I have accordingly updated my score from 6 to 7. ---------------------------- This paper proposes a framework for learning solving strategies for Satisfiability Modulo Theories (SMTs). SMT generalizes SAT, and as such can be used to model a variety of verification applications, among others. Given an instance, an SMT solver such as Z3 will select a strategy, i.e. a sequence of transformations, that will be applied step by step to the input formula, culminating in solving it and returning the answer (true or false). The choice of strategies in SMT solvers is currently heuristic or manually optimized for a set of instances. Alternatively, this paper proposes to learn strategies based on training instances and label-strategies resulting from exploration. A set of learned strategies are then synthetized into a decision tree structure than can be easily fed into the Z3 solver. Experimentally, it is shown that the proposed approach can boost the performance of Z3 significantly.  I am rather positive about this paper, hence my score of 6/10. The paper is relatively well-written, although some points could be clarified here and there. The problem this paper addresses is definitely interesting, and part of a recent effort that aims at improving constraint solvers for MIP/SAT/CSP/SMT using machine learning. I really appreciate the 2-step methodology proposed by the authors, as they do not try to ignore the advances in SMT solvers, but rather hybridize Z3 with their learned strategies. I think that the main weakness of the paper, in its current version, is the experimental results. This is not to say that the proposed method is not promising - it definitely is. However, I have some questions that I hope the authors can address.  - Time limit of 10 seconds: I am quite intrigued as to the particular choice of time limit, which seems really small. In comparison, when I look at the SMT Competition of 2017, specifically the QF_NIA division (http://smtcomp.sourceforge.net/2017/results-QF_NIA.shtml?v=1500632282), I find that all 5 solvers listed require 300-700 seconds. The same can be said about QF_BF and QF_NRA (links to results here http://smtcomp.sourceforge.net/2017/results-toc.shtml). While the learned model definitely improves over Z3 under the time limit of 10 seconds, the discrepancy with the competition results on similar formula types is intriguing. Can you please clarify? I should note that while researching this point, I found that the SMT Competition of 2018 will have a "10 Second wonder" category (http://smtcomp.sourceforge.net/2018/rules18.pdf).  - Pruning via equivalence classes: I could not understand what is the partial "current cost" you mention here. Thanks for clarifying.  - Figure 3: please annotate the axes!!  - Bilinear model: is the label y_i in {-1,+1}?  - Dataset statistics: please provide statistics for each of the datasets: number of formulas, sizes of the formulas, etc.  - Search models comparison 5.1: what does 100 steps here mean? Is it 100 sampled strategies?  - Missing references: the references below are relevant to your topic, especially [a]. Please discuss connections with [a], which uses supervised learning in QBF solving, where QBF generalizes SMT, in my understanding. [a] Samulowitz, Horst, and Roland Memisevic. "Learning to solve QBF." AAAI. Vol. 7. 2007. [b] Khalil, Elias Boutros, et al. "Learning to Branch in Mixed Integer Programming." AAAI. 2016.  Minor typos: - Line 283: looses -> loses