Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nielsen optimizations #136

Merged
merged 3 commits into from
Apr 26, 2024
Merged

Nielsen optimizations #136

merged 3 commits into from
Apr 26, 2024

Conversation

vhavlena
Copy link
Collaborator

@vhavlena vhavlena commented Apr 24, 2024

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.

@vhavlena
Copy link
Collaborator Author

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
--------------------------------------------------

image

@vhavlena vhavlena marked this pull request as ready for review April 26, 2024 08:19
@vhavlena vhavlena requested a review from jurajsic April 26, 2024 08:19
Copy link
Member

@jurajsic jurajsic left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

@vhavlena
Copy link
Collaborator Author

Can I merge it?

@jurajsic jurajsic merged commit 0fa55a5 into devel Apr 26, 2024
@jurajsic jurajsic deleted the nielsen-opts branch April 26, 2024 21:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants