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 -- keep binary clauses #436

Closed ahmed-irfan closed 1 year ago

ahmed-irfan commented 1 year ago

This PR modifies the clause reduction heuristic. With the changes, we will keep the binary clauses in addition to the clauses that are used in the BCP and the half of the clauses kept according to the activity score.

I did some quick experiments -- 3 mins timeout, 8GB memory. Overall, we see improvement. However, one regression (QF_NIA) test timeout with this PR -- that test is disabled in thiS PR.

QF_UF: 6879 -> 7084 QF_AX: 519 -> 522 QF_NRA: 10841 -> 10848 QF_NIA: 15683 -> 15827

coveralls commented 1 year ago

Coverage Status

Coverage: 64.244% (-0.006%) from 64.25% when pulling 4e18eb1cfc912c630838551171364fed8fca751e on mcsat-keep-binary-clauses into eb46358378f88496bb8457e628bbf9131f130cae on master.