Machine learning for instance selection in SMT solving

Daniel El Ouraoui, Pascal Fontaine and Cezary Kaliszyk

We provide here experimental data.

Solver:

The binaries files of veriT here

  • The verbose mode can be activated using the following option --verb-learning-stats

  • Activate veriT without learning in comparative mode:

    ./veriT --disable-print-success --compare-ml-native

  • Activate the learning option in veriT with the first model veriT(M):

    ./veriT --disable-print-success --learning-native

  • Activate the learning option in veriT with the second model veriT(M²):

    ./veriT --disable-print-success --learning-native --learning-native-2

  • Activate the learning option in veriT with both models veriT(M + M²):

    ./ml-m2.sh

  • Activate veriT learning that is veriT + portofolio:

    ./ml-without-learning.sh

  • Activate the learning option in veriT with a portfolio approach veriT(M + M²) + portofolio:

    ./ml-with-learning.sh

Benchmarks:

XGBoost configuration:

  • XGBoost training configuration for veriT(M) here

  • XGBoost training configuration for veriT(M²) here

Results:

The evaluations here