Updates:
Blockedon: sympy:2531 sympy:4075
Comment #2 on issue 4076 by asmeu...@gmail.com: Improvements to logic module
http://code.google.com/p/sympy/issues/detail?id=4076
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.
--
You received this message because this project is configured to send all
issue notifications to this address.
You may adjust your notification preferences at:
https://code.google.com/hosting/settings
--
You received this message because you are subscribed to the Google Groups
"sympy-issues" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sympy-issues+unsubscr...@googlegroups.com.
To post to this group, send email to sympy-issues@googlegroups.com.
Visit this group at http://groups.google.com/group/sympy-issues.
For more options, visit https://groups.google.com/groups/opt_out.
