Complexity of Lloyd-Topor

From: Stefan Decker (stefan@ISI.EDU)
Date: 02/18/03

  • Next message: Mike Dean: "Joint Committee telecon tomorrow 25 February"
    a comment to the Lloyd-Topor discussion:
    the worst-case complexity of Lloyd-Topor is exponential
    (in the number of "<->" (equivalences) used).
    The reason is that "<->" is transformed into
    two implications: "A<->B"  => "A->B" and "A<-B".
    So each equivalence doubles the number of formulas which needs to be
    transformed, which results in the exponential complexity.
    However, the number of equivalences in a formula is usually small,
    so this behavior is not a real problem.
    Not taking equivalences into account, Lloyd-Topor behaves nicely:
    the time complexity is linear in the length of the formula.

    This archive was generated by hypermail 2.1.4 : 02/18/03 EST