Sachin, Chris, I see that you wrote most of the code I'm referring to here.

There are a few things I don't like in the logic module:

• to_cnf is inefficient, particularly if you only care about satisfiability. This is issue 4075.
• If you want exact equivalence, not just satisfiable equivalence, there's not much you can do about to_cnf, but it would be nice if it could remove obviously redundant terms, like x | ~x, or if there were a function to do so.
• simplify_logic is a bit of a misnomer, because it actually tries to return some kind of normal form, which may not actually be the "simplest" (for instance, I consider Implies(x, y) to be simpler than y | ~x). Also, as noted above, it would be nice to just have a function to clean through some obvious redundancies in an expression, like x | ~x.
• Aside from that, simplify_logic doesn't let you pick whether it uses POS or SOP. If the two are the same length, it picks SOP. The result of these points is that it's sometimes very difficult to get a minimal cnf form of an expression. to_cnf returns a large expression with a log of x | ~x in it, and simplify_logic returns a dnf form.
• It doesn't help that POSform and SOPform take non-symbolic inputs.
• Why isn't to_dnf in init.py?
• bool_equal is very confusing. I misused it for some time. What it means is there "exists" a correspondence, whereas the name suggests the two expressions are equal for "all" correspondences.
• I haven't analyzed it deeply, but bool_equal seems to be inefficient. If issue 4075 is fixed, it should be faster to use satisfiable. Logical expressions a and b have a matching correspondence if satisfiable(Equivalent(a, b)) returns a model. They are exactly equal if satisfiable(Not(Equivalent(a, b))) returns False.
• There's already another issue for this, but we desperately need Basic types for True and False. I'm getting tired of special casing them everywhere. The worst thing is that if you do something like ~Equivalent(a, b) instead of Not(Equivalent(a, b)) and a and b are literally the same thing (so that Equivalent just returns True), the expression reduces to ~True, i.e., ~1, which gives -2, which is not logically false. Aside from that, it's annoying when a function didn't account for the possibility of a True or False input, and so raises an exception on trivial input.

I just wanted to write all these things down, so I don't forget them. I will probably try to tackle most of them soon, so if you have any input, especially on the bool_equal thing, that would be great.

I agree with most of these points. As you say, we could make bool-equal better architecturally, or rename it to ensure that the user understands it (same for simplify_logic). Originally, the idea behind simplify_logic is to convert any given expression to its simplest form using the three fundamental boolean operators - not, and, or. It doesn't concern itself with derived operators like Implies/Equivalent. Maybe we could rename simplify_logic? There is, however a way to get the simplest CNF/DNF form- use to_cnf with the simplify parameter. Unfortunately, it seems that that has not been shown in the docstrings. Guess we need to do it ASAP. As far as SOPform/POSform are concerned, they aren't meant to be a part of boolean function operation framework. They are, as you see, 'black boxes' to generate functions based on the truth table of boolean functions. Do you have a better method in mind to take input for them, in place of the existing API? If you could open a PR about these issues, maybe we could work on it together? About the new classes for True/False, we would require detailed discussion before implementing anything.

I didn't notice the simplify=True option to to_cnf. It seems it doesn't work:

In [48]: var("x:3") Out[48]: (x₀, x₁, x₂)

In [49]: a = Or(And(Not(x0), Not(x1), Not(x2)), And(Not(x0), x1, x2), And(Not(x1), x0, x2), And(Not(x2), x0, x1))

In [50]: print(to_cnf(a)) And(Or(Not(x0), Not(x1), Not(x2)), Or(Not(x0), Not(x1), Not(x2), x0), Or(Not(x0), Not(x1), Not(x2), x1), Or(Not(x0), Not(x1), Not(x2), x2), Or(Not(x0), Not(x1), x0), Or(Not(x0), Not(x1), x0, x1), Or(Not(x0), Not(x1), x0, x2), Or(Not(x0), Not(x1), x1), Or(Not(x0), Not(x1), x1, x2), Or(Not(x0), Not(x2), x0), Or(Not(x0), Not(x2), x0, x1), Or(Not(x0), Not(x2), x0, x2), Or(Not(x0), Not(x2), x1, x2), Or(Not(x0), Not(x2), x2), Or(Not(x0), x0), Or(Not(x0), x0, x1), Or(Not(x0), x0, x1, x2), Or(Not(x0), x0, x2), Or(Not(x0), x1, x2), Or(Not(x1), Not(x2), x0, x1), Or(Not(x1), Not(x2), x0, x2), Or(Not(x1), Not(x2), x1), Or(Not(x1), Not(x2), x1, x2), Or(Not(x1), Not(x2), x2), Or(Not(x1), x0, x1), Or(Not(x1), x0, x1, x2), Or(Not(x1), x0, x2), Or(Not(x1), x1), Or(Not(x1), x1, x2), Or(Not(x2), x0, x1), Or(Not(x2), x0, x1, x2), Or(Not(x2), x0, x2), Or(Not(x2), x1, x2), Or(Not(x2), x2))

In [52]: print(to_cnf(a, simplify=True)) And(Or(Not(x0), Not(x1), Not(x2)), Or(Not(x0), Not(x1), Not(x2), x0), Or(Not(x0), Not(x1), Not(x2), x1), Or(Not(x0), Not(x1), Not(x2), x2), Or(Not(x0), Not(x1), x0), Or(Not(x0), Not(x1), x0, x1), Or(Not(x0), Not(x1), x0, x2), Or(Not(x0), Not(x1), x1), Or(Not(x0), Not(x1), x1, x2), Or(Not(x0), Not(x2), x0), Or(Not(x0), Not(x2), x0, x1), Or(Not(x0), Not(x2), x0, x2), Or(Not(x0), Not(x2), x1, x2), Or(Not(x0), Not(x2), x2), Or(Not(x0), x0), Or(Not(x0), x0, x1), Or(Not(x0), x0, x1, x2), Or(Not(x0), x0, x2), Or(Not(x0), x1, x2), Or(Not(x1), Not(x2), x0, x1), Or(Not(x1), Not(x2), x0, x2), Or(Not(x1), Not(x2), x1), Or(Not(x1), Not(x2), x1, x2), Or(Not(x1), Not(x2), x2), Or(Not(x1), x0, x1), Or(Not(x1), x0, x1, x2), Or(Not(x1), x0, x2), Or(Not(x1), x1), Or(Not(x1), x1, x2), Or(Not(x2), x0, x1), Or(Not(x2), x0, x1, x2), Or(Not(x2), x0, x2), Or(Not(x2), x1, x2), Or(Not(x2), x2))

In [53]: to_cnf(a, simplify=True) Out[53]: (x₀ ∨ ¬x₀) ∧ (x₁ ∨ ¬x₁) ∧ (x₂ ∨ ¬x₂) ∧ (x₀ ∨ x₁ ∨ ¬x₀) ∧ (x₀ ∨ x₁ ∨ ¬x₁) ∧ (x₀ ∨ x₁ ∨ ¬x₂) ∧ (x₀ ∨ x₂ ∨ ¬x₀) ∧ (x₀ ∨ x₂ ∨ ¬x₁) ∧ (x₀ ∨ x₂ ∨ ¬x₂) ∧ (x₀ ∨ ¬x ₀ ∨ ¬x₁) ∧ (x₀ ∨ ¬x₀ ∨ ¬x₂) ∧ (x₁ ∨ x₂ ∨ ¬x₀) ∧ (x₁ ∨ x₂ ∨ ¬x₁) ∧ (x₁ ∨ x₂ ∨ ¬x₂) ∧ (x₁ ∨ ¬x₀ ∨ ¬x₁) ∧ (x₁ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₂ ∨ ¬x₀ ∨ ¬x₂) ∧ (x₂ ∨ ¬x₁ ∨ ¬x ₂) ∧ (¬x₀ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₀ ∨ x₁ ∨ x₂ ∨ ¬x₀) ∧ (x₀ ∨ x₁ ∨ x₂ ∨ ¬x₁) ∧ (x₀ ∨ x₁ ∨ x₂ ∨ ¬x₂) ∧ (x₀ ∨ x₁ ∨ ¬x₀ ∨ ¬x₁) ∧ (x₀ ∨ x₁ ∨ ¬x₀ ∨ ¬x₂) ∧ (x₀ ∨ x₁ ∨ ¬x ₁ ∨ ¬x₂) ∧ (x₀ ∨ x₂ ∨ ¬x₀ ∨ ¬x₁) ∧ (x₀ ∨ x₂ ∨ ¬x₀ ∨ ¬x₂) ∧ (x₀ ∨ x₂ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₀ ∨ ¬x₀ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₁ ∨ x₂ ∨ ¬x₀ ∨ ¬x₁) ∧ (x₁ ∨ x₂ ∨ ¬x₀ ∨ ¬x₂) ∧ (x₁ ∨ x₂ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₁ ∨ ¬x₀ ∨ ¬x₁ ∨ ¬x₂) ∧ (x₂ ∨ ¬x₀ ∨ ¬x₁ ∨ ¬x₂)

Notice for instance the very first term is (x₀ ∨ ¬x₀), which can be removed. I believe the cnf for this expression should be And(Or(Not(x0), Not(x1), Not(x2)), Or(Not(x0), x1, x2), Or(Not(x1), x0, x2), Or(Not(x2), x0, x1)) (i.e., the same as the original except with And and Or swapped).

The true/false stuff has been discussed before. See issue 2531 (and links therein to the mailing list). The work got stalled for some reason. I personally feel much less confused about the distinction that needs to be made between the two-valued and the three-valued logic. As Ronan noted, another issue there is when exactly given functions should return the bool True and when they should return the basic true.

Regarding bool_equal and simplify_logic, my biggest issue here is just with the name "bool_equal". Being able to "simplify" further in simplify_logic would be cool, but it's not priority for me right now. My issue is that the name bool_equal suggests "equal everywhere", not "equal somewhere".

By the way, "not satisfiable(Not(Equivalent(a, b)))" is a little hard to remember, but the good news is that newask() (https://github.com/sympy/sympy/pull/2508), because of the way it works, you will be able to just do newask(Equivalent(a, b)) and it will return True if they are logically equivalent (it will return None if they aren't equal everywhere, but are equal somewhere, and False if they are unequal). It's still probably a good idea to make a bool_equal function, though, because it avoids assumptions boilerplate that might come attached to ask (e.g., if your predicates are keys of Q, then ask will consider the known facts about those keys, whereas you might just want basic logical equivalence with no additional knowledge).

I'll open pull requests for my work on these issues as I get to them, and ping you on them.

Another thing that bugs the crap out of me that I may or may not get around to fixing is all the automatic evaluation that happens. Not automatically applies deMorgan's laws. Nor, Nand, Xor, and ITE are nothing more than fancy shortcuts. IMHO the only automatic evaluation that should happen is basic canonicalization (short circuiting, denesting, removing duplicate args, ordering the args canonically).

OK, see https://github.com/sympy/sympy/pull/2560.

We have moved issues to GitHub https://github.com/sympy/sympy/issues.

Migrated to http://github.com/sympy/sympy/issues/7175