A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems

10 pages•Published: August 19, 2013

Mohammad Abdul Aziz, Amr Wassal and Nevine Darwish

Abstract

In this paper we present an approach for measuring the hardness of SMT problems.
We present the required features, the statistical hardness model used and the machine
learning technique which we used. We apply our method to estimate the hardness of
problems in Quantier Free Bit Vector (QFBV) theory and we used four of the contesting
solvers in SMT2011 to demonstrate our technique. We have qualitatively expanded some
propositional SAT features existing in the literature to directly work on general SMT
problem instances without preprocessing. The results show that our work is a promising
proof of concept.

Keyphrases: machine learning, smt, statistical hardness models

In: Pascal Fontaine and Amit Goel (editors). SMT 2012. 10th International Workshop on Satisfiability Modulo Theories, vol 20, pages 57-66.

Links:	https://easychair.org/publications/paper/kW
	https://doi.org/10.29007/z794

BibTeX entry

@inproceedings{SMT2012:Machine_Learning_Technique_Hardness,
  author    = {Mohammad Abdul Aziz and Amr Wassal and Nevine Darwish},
  title     = {A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems},
  booktitle = {SMT 2012. 10th International Workshop on Satisfiability Modulo Theories},
  editor    = {Pascal Fontaine and Amit Goel},
  series    = {EPiC Series in Computing},
  volume    = {20},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/kW},
  doi       = {10.29007/z794},
  pages     = {57-66},
  year      = {2013}}

Download PDF Open PDF in browser