vhavlena
commented
4 months ago Results on everything
# of formulae: 103318
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ---- ----- --------- ----- ----- ----- ----- ------- --------- ----- -------- -------
z3-noodler-605ccd5-d95fe13 0 1342 15990.37 0.16 0.01 1.75 0 0 638 658 46 0
z3-noodler-b0899c4-d95fe13 0 1365 16198.75 0.16 0.02 1.75 0 0 638 658 69 0
cvc5-1.1.2 0 3619 76478.24 0.77 0.00 6.77 0 0 2 3608 9 0
z3-4.13.0 0 5631 132036.99 1.35 0.01 8.11 0 0 210 4960 461 0
ostrich-5dd2e10ca 0 16986 782639.00 9.06 1.75 19.20 0 0 0 16962 12 12
z3-4.13.0+cvc5-1.1.2 0 2562 60604.78 0.60 0.00 6.00 0 0 2562 0 0 0
z3-noodler-605ccd5-d95fe13+z3-4.13.0+cvc5-1.1.2 0 144 11050.73 0.11 0.00 1.61 0 0 144 0 0 0
--------------------------------------------------Results on woorpje (targetted benchmark)
Benchmark woorpje
# of formulae: 809
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ---- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-605ccd5-d95fe13 0 36 144.39 0.19 0.01 1.70 0 0 0 19 17 0
z3-noodler-b0899c4-d95fe13 0 59 296.91 0.40 0.02 2.62 0 0 0 19 40 0
cvc5-1.1.2 0 54 45.21 0.06 0.01 0.23 0 0 0 54 0 0
z3-4.13.0 0 27 300.36 0.38 0.02 4.80 0 0 0 27 0 0
ostrich-5dd2e10ca 0 55 7072.39 9.36 4.64 15.95 0 0 0 51 2 2
z3-4.13.0+cvc5-1.1.2 0 20 67.20 0.09 0.01 0.89 0 0 20 0 0 0
z3-noodler-605ccd5-d95fe13+z3-4.13.0+cvc5-1.1.2 0 11 42.57 0.05 0.01 0.84 0 0 11 0 0 0
--------------------------------------------------
This PR optimizes the Nielsen transformation with a priority queue instead of dequeue as a datastructure for storing nodes of a proof graph. Now we prefer nodes with smaller formulae as they more likely reach a final node.