Address failing test

[haz]

Currently fails: https://github.com/QuMuLab/python-nnf/blob/master/test_nnf.py#L613

[haz]

So I've taken a deeper dive into this. For reference, this is the paper that captures the algorithm: https://www.ijcai.org/Proceedings/15/Papers/281.pdf

The important excerpt:

The algorithm iterates until it computes all prime implicants and a (prime) implicate cover of F. Observe that this prime implicate cover is essentially what C already represents when F is represented in CNF [Palopoli et al., 1999; Jabbour et al., 2014].

The cover doesn't mean that it will compute all prime implicates, but rather enough to collectively capture the theory. In particular, the example sentence is (-1 & 2) | (-3 & 1), and the problematic comparison is between the implicants and sentence.negate().implicates().negate(). Since sentence.negate() results in a CNF, the implicates() of that is just the same (correct according to the excerpt above). Inspecting the theory at that point, it's clear that the missing term is just the resolution (on variable 1) of the two binary clauses. So no new information provided, and thus not required by the implicate cover.

@blyxxyz Can you confirm the above? If so, then I think the test need not pass. This would all change if equality is meant to be the KC sense: i.e., the models correspond exactly. Best way I can think of doing that would be to negate one of the sentences, conjoin them, and check for satisfiability (unsat means the original two are semantically equivalent).

[haz]

*nudge*

Just about to throw some more tests in for the Tseitin stuff, but would like to close this out too if it makes sense to you.

[blyxxyz]

That asymmetry (all implicants, some implicates) sounds like it's the culprit. But it's the comparison between sentence.negate().implicants().negate() and sentence.implicates() that fails, not the other one.

I think I've reconstructed my thinking behind the test.

• A→B is equivalent to ¬B→¬A, so any implicate of the sentence is also a negated implicant of the negated sentence.
• (Does this also hold for prime implicates and prime implicants? I'm not sure right now, but if not then the test should probably go entirely.)
• So sentence.negate().implicants().negate() gives all prime implicates.
• We go wrong because .implicates() may not return all of them.
• A correct check would be that sentence.implicates().children <= sentence.negate().implicants().negate().children, and something along the same lines for the other.
• The documentation for .implicates() should be changed (currently it says "Extract the prime implicates of the sentence.").

Does this sound right? If so, I'll open a fix soon.

(I think NNF.equivalent already implements the check you mention, by the way.)

[haz]

It does, yep. And I think it also holds for prime setting (I'm assuming you meant if a negated prime implicate is a prime implicant in the negated theory). Easier to see this when you play around with the model interpretation of implicates / implicants (ala Venn diagrams or similar): T |= C iff models(T) <= models(C)

I noticed that equivalent check later on, ya. And also another pleasant surprise to see the AMC stuff!

[blyxxyz]

An interesting test failure caused by the same assumption. It only happens in PyPy, probably because its sets remember insertion order (like CPython's dicts since 3.6).

test_implicates_implicants_idempotent asserts that s.implicates() == s.implicates().implicates(). This isn't the case:

Python 3.6.9 (7.3.1+dfsg-4, Apr 22 2020, 05:27:13)
[PyPy 7.3.1 with GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>>> from nnf import *
>>>> s = Or({And({~Var(1), ~Var(2)}), And({Var(1), ~Var(3)})})
>>>> s.implicates()
And({Or({~Var(1), ~Var(3)}), Or({Var(1), ~Var(2)})})
>>>> s.implicates().implicates()
And({Or({~Var(1), ~Var(3)}), Or({Var(1), ~Var(2)}), Or({~Var(3), ~Var(2)})})

That seems ok to me, because we make no guarantees about redundant clauses, so I'll fix the test in #17.