feat: sd-dnnf-checker by IbrahimElk · Pull Request #24 · ML-KULeuven/klay

IbrahimElk · 2026-03-24T09:46:14Z

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.

IbrahimElk · 2026-03-27T14:17:55Z

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 the bindings in this PR that i needed in my personal branch for debugging.

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

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

- following stricter c++ guidelines: https://google.github.io/styleguide/cppguide.html#Namespaces Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

enables safe subclassing of circuit from external consumers (e.g. kompyle). Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Replace the determinism comment with a more accurate note: checking determinism on arbitrary NNF circuits is coNP-complete. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Also drops the stale comment explaining why get_indices is bound on Circuit. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Not all tests are run during ci. Run all tests manually `pytest tests/* -vv -rs` Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

IbrahimElk · 2026-04-24T14:27:09Z

@jjcmoon Would it be possible to bump the version when deciding to merge these changes ?
(such that the changes will be available in pypi)

jjcmoon

I think this could simplified quite a bit, c.f. the comments.

jjcmoon · 2026-05-06T12:51:19Z

    std::vector<Node*> roots = {};

-    ~Circuit() {
+    virtual ~Circuit() {


Why make Circuit virtual? I feel this isn't necessary.

It's handy when inheriting the circuit class, although, it doesn't fit this PR,
I could move this to another PR if needed ?

In kompyle, for example, I inherit the circuit class in order to add an extra field,
but that fields doesn't fit in the klay project. So, i thought that would be the best solution ?

The field is to have a mapping from variable names to indices such that you can process
multiple non-cnf files into the same klay circuit and don't have the same name from different
files map to different indices in the same klay circuit.

jjcmoon · 2026-05-06T12:52:43Z

+#include <string>
+#include <vector>
+
+#include <cassert>


Move unused headers.

i have moved some to the cpp file, could you check if that is what you wanted ?
see commit 728e3b2

check latest commit instead or rather 8d8962a

jjcmoon · 2026-05-06T12:55:01Z

+
+std::string sdnnf_summary(const SDNNFResult& r);
+
+class IPropertyChecker {


This seems over-engineered. Can't you just make two methods that check decomposability and smoothness?

sure, basically, have only the methods:

SDNNFResult check_decomposability(const Circuit& circuit, std::size_t max_violations); SDNNFResult check_smooth(const Circuit& circuit, std::size_t max_violations); SDNNFResult check_sdnnf(const Circuit& circuit, std::size_t max_violations);

i have done what was ordered from me, am i free to go my lord ?

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

* gets automatically detected by pytest, which is used in CI Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

* removing unused code Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

* was used to check certain things when completing the search trough the klay circuit, but is now unused. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

* moving certain dependencies to cpp Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Remove the IPropertyChecker interface, DecomposabilityChecker and SmoothnessChecker classes, and the run_checks dispatcher in favour of two static helpers (check_and_decomp, check_or_smooth) called directly from check_decomposability, check_smooth and check_sdnnf. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

jjcmoon

Thanks for the changes!

IbrahimElk mentioned this pull request Mar 24, 2026

Feat/add extensive testing ML-KULeuven/kompyle#9

Merged

IbrahimElk marked this pull request as draft March 27, 2026 14:10

IbrahimElk added 9 commits April 16, 2026 11:11

feat: expose sdnnf checker to python

a6da42d

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

test: add sd-dnnf checker api tests

8a42e79

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

feat: expose circuit_to_dot for debugging

6ac2a37

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

cmake: move properties to core klay

9b7bf8c

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

build: add temporary debug build type

3e3f866

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

feat: separate decomposability and smoothness checks

7a5bbad

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

feat: expose decomposability checks to python

4131093

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

build: remove temporary debug build type (b8ff7f0)

ce22597

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

IbrahimElk force-pushed the feat/sd-dnnf-checker branch from 3ba6338 to ce22597 Compare April 16, 2026 09:18

IbrahimElk added 2 commits April 16, 2026 16:29

ref: wrap in namespace klay instead of using-directive

1bbe4c5

- following stricter c++ guidelines: https://google.github.io/styleguide/cppguide.html#Namespaces Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

fix: place properties and util in namespace klay

e7e8deb

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

IbrahimElk force-pushed the feat/sd-dnnf-checker branch from d606b48 to e7e8deb Compare April 16, 2026 14:32

IbrahimElk added 5 commits April 19, 2026 12:06

ref: make circuit destructor virtual

fcb0cad

enables safe subclassing of circuit from external consumers (e.g. kompyle). Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: remove determinism-checker code

df225fa

Replace the determinism comment with a more accurate note: checking determinism on arbitrary NNF circuits is coNP-complete. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: remove unused circuit_to_dot Python binding

b0d6267

Also drops the stale comment explaining why get_indices is bound on Circuit. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

chore: move STL includes to header, fix formatting and spelling

8c192e1

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

fix: double-encoding of CNF filename in JAX fuzzer

b0b87c0

Not all tests are run during ci. Run all tests manually `pytest tests/* -vv -rs` Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

IbrahimElk marked this pull request as ready for review April 24, 2026 14:25

jjcmoon requested changes May 6, 2026

View reviewed changes

IbrahimElk added 6 commits May 6, 2026 15:07

ref: remove copyright headers from src/include files

d80b3d2

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: rename test/api.py to test/test_api.py

99452b3

* gets automatically detected by pytest, which is used in CI Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: remove deterministic flag and related comments

9fe2377

* removing unused code Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: remove finalize in IPropertyChecker

833331c

* was used to check certain things when completing the search trough the klay circuit, but is now unused. Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: making headers self-contained

728e3b2

* moving certain dependencies to cpp Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

ref: remove unused include headers

8d8962a

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

IbrahimElk added 2 commits May 6, 2026 16:09

fix: alignment <= 80 characters

8463539

Signed-off-by: IbrahimElk <ibrahim_elkaddouri@outlook.com>

jjcmoon approved these changes May 7, 2026

View reviewed changes

jjcmoon merged commit b3fd675 into ML-KULeuven:main May 7, 2026
1 check passed


		std::string sdnnf_summary(const SDNNFResult& r);

		class IPropertyChecker {

Uh oh!

Conversation

IbrahimElk commented Mar 24, 2026

Uh oh!

IbrahimElk commented Mar 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

IbrahimElk commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jjcmoon left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jjcmoon May 6, 2026

Choose a reason for hiding this comment

Uh oh!

IbrahimElk May 6, 2026

Choose a reason for hiding this comment

Uh oh!

jjcmoon May 6, 2026

Choose a reason for hiding this comment

Uh oh!

IbrahimElk May 6, 2026

Choose a reason for hiding this comment

Uh oh!

IbrahimElk May 6, 2026

Choose a reason for hiding this comment

Uh oh!

jjcmoon May 6, 2026

Choose a reason for hiding this comment

Uh oh!

IbrahimElk May 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

IbrahimElk May 6, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jjcmoon left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

IbrahimElk commented Mar 27, 2026 •

edited

Loading

IbrahimElk commented Apr 24, 2026 •

edited

Loading

IbrahimElk May 6, 2026 •

edited

Loading