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

Reconsider Ord trait on BddValuation #36

Open
daemontus opened this issue Mar 3, 2023 · 5 comments
Open

Reconsider Ord trait on BddValuation #36

daemontus opened this issue Mar 3, 2023 · 5 comments
Milestone

Comments

@daemontus
Copy link
Member

Right now, this is a "derived" trait implementation. But this may be slightly unintuitive, because it is just a "lexicographic" ordering. On surface, this is reasonable because it follows the normal iteration order. But there are a few considerations to be made:

  • Is this even useful? Do we expect people to compare valuations like this?
  • Should ordering fail on incompatible valuations? (i.e. different variable count).
  • Shouldn't there rather be a PartialOrd between BDD valuations and partial valuations that is instead based on "inclusion"? Wouldn't this be a more natural ordering on valuations?
@daemontus
Copy link
Member Author

Just a quick note that the earliest point where we can safely change this is the 1.0.0 version, since this would be a breaking change.

@daemontus daemontus added this to the 1.0.0 milestone May 3, 2023
@zao111222333
Copy link
Contributor

Hi, in this time can we directly add derived PartialOrd to Bdd and BddNode?

I understand this implementation mightly be useless and confused for most of people... But here is one scenarios when I want to sort some BooleanExpression according their Bdd. I don't care the sorting metric, just clustering the same logic as near as possible. (e.g., A&B, B&A should be close to each other and far from A&!B).

Thank you!

@daemontus
Copy link
Member Author

daemontus commented Aug 12, 2024

Hi! Sorry for the late response.

I am a bit reluctant to add an ordering to BDDs directly, since this could be interpreted in many different ways. For example, one could order BDDs by size (in terms of nodes), one could order them by the number of positive results the function gives (function weight/cardinality), one could order them by implication (i.e. A <= B if A implies B), etc. There really isn't a one true "normal" ordering.

However, I see your point. Since Rust supports Vec::sort_by, I would propose the following:

Add a collection of pre-made sorting methods that can be used with sort_by in various scenarios. Some of these would be total, while some can be only partial. So you could use vec.sort_by(Bdd::size_sort), vec.sort_by(Bdd::cardinality_sort), vec.sort_by(Bdd::structural_sort) (your suggestion), and vec.sort_by(Bdd::implication_sort), etc.

Would this work for you?

@daemontus
Copy link
Member Author

daemontus commented Aug 12, 2024

I've added the comparator methods here as Bdd::cmp_*: 932984c

This is now included in the library since version 0.5.18.

@zao111222333
Copy link
Contributor

Hi! Thank you a lot for your help!

I've used the Bdd::cmp_* to my cases, it is a very useful API (especially Bdd::cmp_structural for me). I know it's a hard work to implement so many ways to do comparsion.
Thank you!

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

No branches or pull requests

2 participants