Reviews: Learning to Solve SMT Formulas

The paper discusses the problem of solving SMT formula by means of combinations of operations on formulas called tacticts. Such combinations form simple programs called strategies operating on a state represented by the formula. The paper presents an approach for learning the strategies. The approach works in two phases: first a policy is learned, that defines a probability distribution over tacticts given the state, then this is transformed into a set of sequences of tactics that are combined into strategies by adding branching instructions. The approach is experimentally evaualated by comparing its performance with respect to hand crafted strategies using the Z3 SMT solver.