Skip to content

feat: sd-dnnf-checker#24

Draft
IbrahimElk wants to merge 9 commits intoML-KULeuven:mainfrom
IbrahimElk:feat/sd-dnnf-checker
Draft

feat: sd-dnnf-checker#24
IbrahimElk wants to merge 9 commits intoML-KULeuven:mainfrom
IbrahimElk:feat/sd-dnnf-checker

Conversation

@IbrahimElk
Copy link
Copy Markdown
Contributor

This PR adds some property-checks for sd-DNNF circuits implemented using Klay.
Primarily, syntactic checks including decomposability and smoothness, and exposes the results to python.
This PR also adds tests covering these new check methods.

* this adds a bottom-up checker that walks the circuit once, and checks
- decomposability: no variable appears in more than one child of an AND
- smoothness: every child of an OR mentions exactly the same variable scope

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
* exported symbols (e.g. check_sdnnf) are visible
  for linking and debugging

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
* this commit will be eventually reversed

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
@IbrahimElk IbrahimElk marked this pull request as draft March 27, 2026 14:10
@IbrahimElk
Copy link
Copy Markdown
Contributor Author

IbrahimElk commented Mar 27, 2026

@jjcmoon do you think its best to merge now ? or rather later, when i complete the following issues in kompyle 5 15.

I'll also clean up a bit the code in this PR, i have some commented out code that i should remove.
And also remove to_dot_file from this PR that i needed in my personal branch for debugging.

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.

1 participant