search

QuMuLab / python-nnf

Manipulate NNF (Negation Normal Form) logical sentences
https://python-nnf.readthedocs.io
ISC License
17 stars 9 forks source link

Simplify tautologies #29

Closed haz closed 1 year ago

haz commented 1 year ago

Idea is to allow for tautologies in to_CNF conversions so that model counts aren't thrown off (variables mentioned in a tautological clause will be missing from the compilation).

haz commented 1 year ago

Closes #30

haz commented 1 year ago

Great idea! It caught a corner case where (x & ~x) | y was being simplified to just y. Can you have another look after the latest commit?

blyxxyz commented 1 year ago

Ah! I hadn't spotted that.

My only concern now is that the name simplify_tautologies is inaccurate because it also covers contradictions.

haz commented 1 year ago

Ah, right. Just simplify work?

haz commented 1 year ago

Thanks, @blyxxyz ! Should be all set to go if you want to approve/merge.