As mentioned in my previous 
post<https://groups.google.com/d/topic/sympy/pWlun8V2NYI/discussion>, 
I'm working on a simplify function
for Boolean (and eventually relational) objects. The idea is to have the
following behavior:

>> simplify(A|((C|B)&A))
A

>> simplify(((A>>B) & (B>>C)) >> (A>>C)) #proving transitivity of 
implication
True

In general, boolean formula simplification is at least NP-hard as a 
generalization of SAT. 
It is also not completely related to the Quine-McCluskey algorithm, in that 
A&B | A&C is a fully simplified output for the Quine-McCluskey algorithm,
but the factored A&(B|C) form is intuitively smaller. For these reasons, 
I'm 
going with a heuristic simplifier.

Currently, the logical module silently takes some extra transformation 
steps when 
defining a formula. For example, Not() will push down the expression tree 
all the negations. This gets in the way of simplifying. Indeed,
~A | ~B | ~C | ~D is objectively more complex than ~(A & B & C & D).

I think we have to separate this rewriting behavior from the construction
of a boolean expression.

Alex

-- 
You received this message because you are subscribed to the Google Groups 
"sympy" group.
To view this discussion on the web visit 
https://groups.google.com/d/msg/sympy/-/dWGHR7umveYJ.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to 
[email protected].
For more options, visit this group at 
http://groups.google.com/group/sympy?hl=en.

Reply via email to