Skip to content

Conversation

@redianthus
Copy link
Contributor

@redianthus redianthus commented Nov 21, 2025

This will be useful in Owi to make the PC independence algorithm better, for now, a conjunction is forced to be put under the same union-find group, which is unfortunate. Splitting them this way before adding them to the UF should improve things a lot.

I also added split_disjunctions while I was at it, but not sure it'll be useful for now.

It may be possible to push the split even further, for instance, if we have e defined as $¬(P ∨ Q)$ we could do split_conjunctions e to be $\lbrace ¬P ; ¬Q \rbrace $. But I am not sure yet if this belong to this function or to a simplification, so I left it out for now. I'll experiment with this and see what would be best.

@redianthus redianthus requested a review from a team as a code owner November 21, 2025 12:02
Co-authored-by: Filipe Marques <[email protected]>
@redianthus
Copy link
Contributor Author

@filipeom, should be OK now :)

Copy link
Member

@filipeom filipeom left a comment

Choose a reason for hiding this comment

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

Thanks! 🙏

@filipeom filipeom merged commit bdefa65 into formalsec:main Nov 21, 2025
9 checks passed
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