search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

MCSAT Bool Plugin -- Bool bump factor #437

Closed ahmed-irfan closed 1 year ago

ahmed-irfan commented 1 year ago

This PR introduces a new parameter in the mcsat bool plugin heuristic. The new parameter is the times factor for boolean reasons when learning new clauses in the bool plugin.

Note that theory variables have also a times factor which is equal to the number of occurrences. This can give more preference to theory variables as decisions because theory variables can occur in many boolean terms and in fact in the same boolean term. So, basically the newly added times factor for boolean reasons tries to unbias. Currently it is set to 5 -- found via few experiments, and it is likely not optimal.

Here is the improvement on the smtlib benchmarks. (timeout: 3 mins ; mem: 8 GB).

QF_UF: 7084 -> 7274 QF_AX: 522 -> 543 QF_NRA: 10848 -> 10914 QF_NIA: 15827 -> 16311

coveralls commented 1 year ago

Coverage Status

Coverage: 64.23% (-0.01%) from 64.244% when pulling 1c8923f4ba1cbbd4bec2914fcd2a1f7e60c47b25 on bool-bump-factor into db898586b6735d5c924494a431cba251e3459dd2 on master.