Feat/add extensive testing - #9
Merged
Merged
Conversation
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
* check circuit output matches CNF truth table for all assignments, covering trivial and random 3-CNF cases. * check compiled circuits satisfy decomposability and smoothness via klay.check_sdnnf. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Collaborator
Author
|
Work related to Arjun’s integration will be handled separately in another branch and a dedicated PR. |
* FCircuit's operator/= was a no-op, causing non-decomposable circuits when GANAK's flipped_declit conflict path calls branch_mc /= weight(x1) to undo a previously multiplied-in literal weight. * Literal weights are now kept in pending_lits_ rather than immediately committed into the AND tree. operator/= removes the literal from this list. Pending lits are committed into node_ only when an OR node is built, which is after the division window has closed. * Also fix larger_than() to use count_ instead of returning false, so GANAK's cube selection heuristic has a meaningful ordering. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
* in order to access sdnnf checker of klay Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
IbrahimElk
force-pushed
the
feat/add-extensive-testing
branch
from
March 24, 2026 08:45
c87ed73 to
733c237
Compare
* Remove the compile_from_ganak(string) overload that created its own circuit internally, callers must now provide an existing circuit explicitly. * Expand test_api.py into a TestAPI class Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
IbrahimElk
force-pushed
the
feat/add-extensive-testing
branch
from
March 24, 2026 08:50
733c237 to
c206583
Compare
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Collaborator
Author
* non-chronological backtracking is not yet compatible with circuit building. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #8
This PR was originally opened to verify that adding Arjun to
compile_from_ganakwould not break any circuits.To support that verification, I added an sd-DNNF checker to
klaythat checks decomposability and smoothness.That checker is currently available in my branch here:
https://github.com/IbrahimElk/klay/tree/feat/sd-dnnf-checker
and will hopefully be merged into the main
klaybranch at:https://github.com/ML-KULeuven/klay
Using this checker, I found that
compile_from_ganakwithout any preprocessing by Arjun was producing incorrect circuits. This PR fixes that issue infield_circuit.hand adds more extensive tests to ensure the behavior remains correct in the future.It also introduces exhaustive equivalence tests that verify the CNF formula and the generated circuit encode the same Boolean function. Since testing all CNF formulas is infeasible, the test suite focuses on small formulas, random 3-CNF instances, and edge cases.