On Jul 14, 3:59 pm, Chris Gorecki <[EMAIL PROTECTED]> wrote:
> Hi All,
>
> I'm currently trying to implement a function for the propositional
> calculus package that would determine if two statements are logically
> equivalent. The usage would be something along the lines of:
>
> sage: a = propcalc.formula('a | (b&c)')
> sage: b = propcalc.formula('(x&y) | z')
> sage: a.equivlant(b)
> True
>
> One way to do this would be to examine the truth tables of each for
> every possible mapping of the variable, but the run time would be
> exponential plus some. Does anyone know of a better way to implement
> this?
This is equivalent to satisfiability, so there's a huge literature on
the topic. Nobody knows of an algorithm that's better than
exponential in the worst case (a polynomial-time algorithm would prove
P=NP), but there are lots of algorithms that are better than brute-
force search. See http://en.wikipedia.org/wiki/Satisfiability (the
section "Algorithms for solving SAT") for a brief introduction.
Carl
--~--~---------~--~----~------------~-------~--~----~
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/sage-devel
URLs: http://www.sagemath.org
-~----------~----~----~----~------~----~------~--~---
