A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems

In this paper, we present a new approach for measuring the expected runtimes (hardness) of SMT problems. The required features, the statistical hardness model used and the machine learning technique which we used are presented. The method is applied to estimate the hardness of problems in the Quantifier Free Bit Vector (QFBV) theory and we used four of the contesting solvers in SMTCOMP2011 to demonstrate the technique. We have qualitatively expanded some propositional SAT features existing in the literature to directly work on general SMT problem instances without preprocessing. Experimental results with the standard set of benchmarks are promising and our implementation proves the concept.