Space vs Time Trade-off : Dynamic Variable Reordering

Space vs Time Trade-off : Dynamic Variable Reordering

• Transparent to the user
• Essential when:
  • Static ordering heuristics is not able to find the best ordering
  • No single good ordering exists for computing reachable states
• Helps the computation by :
  • Providing an ordering which results in less BDD nodes
• In general results in more computation time if kept enabled continuously
  • Need to invoke it judiciously
  • “enable” mode vs “force” mode

Previous slide

Next slide

Back to the first slide

View Graphic Version