logic module: stop silently transforming expressions?

[Alex]

As mentioned in my previous post, 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

[Aaron Meurer]

I agree. I thought we had an issue for this, but I can't find it. But
we definitely should remove all but the most trivial simplifications
(i.e., automatically simplifying expressions with literal True or
False).

Aaron Meurer

[Alex]

Seems good to me. I'm just a little unsure about what counts as a "most trivial simplification".

Do you count A | ~A <=> True as a trivial simplification the constructor should do? Isn't that potentially

going to confuse the user? To me, a boolean expression as inputed, and its simplified form are potentially

both worth keeping. Somebody might need the unsimplified form whatsoever (?)

[Aaron Meurer]

No, even that I would leave alone. I was saying that basically the
only exceptions should be if a literal is in the expression, like True
| x or True & x. This is similar to the approach taken in many other
parts of SymPy (there the "literals" are numbers like 3 or pi).

I think this strikes a good balance between avoiding automatic
simplification that is difficult or impossible to have not happen, and
requiring the user to type simplify() just to get the most trivial
evaluations to happen.

By the way, what automatic simplifications are currently happening?
The only one I know of, aside from ones involving boolean literals, is
the conversion of xor. It looks like things like x | ~x and x & ~x are
being left alone.

Aaron Meurer

> --
> 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/-/kkrkJ89koBkJ.
>
> To post to this group, send email to sy...@googlegroups.com.
> To unsubscribe from this group, send email to
> sympy+un...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/sympy?hl=en.

[Alex]

Yes, A | ~A are left alone. A | A simplifies to A, which is fine. I think that's about it.

There is a bunch of other functions aside from xor which directly

translates to and, or, not operations:

Nand - I'm good with translating it at construction time

Nor -- can stay as is too

Xor -- should probably not be rewritten automatically

Implies -- should not be rewritten automatically

Equivalent -- should not be rewritten automatically

ITE (if-then-else) -- should not be rewritten automatically

In general, I think it will be quite hard to make simplify() "compile"

to the last 4 high-level expressions, except for the implication.

The general approach would anyway be to translate everything to

And, Or, Not format and work with this limited set of operations:

it's much easier to work on that.

Once a smaller form is found, some heuristic could try to find

Xor, Implies, etc patterns and "compile up" to these functions, although

I don't think that a final expression full of => signs and xors is necessary

simpler than its $|~ equivalent.

[Aaron Meurer]

On Fri, Jul 27, 2012 at 1:28 AM, Alex <alex.kan...@gmail.com> wrote:
> Yes, A | ~A are left alone. A | A simplifies to A, which is fine. I think
> that's about it.
> There is a bunch of other functions aside from xor which directly
> translates to and, or, not operations:

Yes, autosimplification of A | A lets us do optimizations at
constructor time (namely, dumping the args in a set) that are probably
not worth giving up just so that expressions like that would be
expressible.

>
> Nand - I'm good with translating it at construction time
> Nor -- can stay as is too

I agree. These can stay as they are, unless there are requests to
make them unevaluated.

>
> Xor -- should probably not be rewritten automatically
> Implies -- should not be rewritten automatically
> Equivalent -- should not be rewritten automatically
> ITE (if-then-else) -- should not be rewritten automatically

Definitely. Especially for Xor, which even has its own symbol
recognized by Python.

I thought of one other case. x << y should continue to be the same
thing as y >> x (we recently removed this sort of thing from <, >, <=,
and >=, but I think this case is different: rarely do you want to
write x <- y in that order.

>
> In general, I think it will be quite hard to make simplify() "compile"
> to the last 4 high-level expressions, except for the implication.
> The general approach would anyway be to translate everything to
> And, Or, Not format and work with this limited set of operations:
> it's much easier to work on that.
>
> Once a smaller form is found, some heuristic could try to find
> Xor, Implies, etc patterns and "compile up" to these functions, although
> I don't think that a final expression full of => signs and xors is necessary
> simpler than its $|~ equivalent.

Sure, we'll have to see what works. Personally, any logical
expression that's more than a few symbols long is hard to read,
regardless what form it's in. Perhaps some cases will not be simpler,
but certainly some will be (as a simple example, take the case where
the entire expression can be reduced to a single Xor or Implies). So
probably there is some middle ground, and heuristics that can be used
to find it. Perhaps it has something to do with nesting of the
operations.

And by the way, I think it would be cool to have an algorithm that can
convert a cnf form of a bunch of nested implies back to the implies,
even if the latter is relatively messy.

Aaron Meurer

[Alex]

Alright, everything sounds quite good to me, except that

the << being equivalent to >> is slightly distasteful to me.

That's only going to cause confusion. 

I would personally keep it, just because 

sometimes you don't want to rewrite the full expression

but just want to reverse the direction of the implication

and see what happens.

I'm opening a new issue then.

Alex