On the difficulty of enforcing directional consistency at the SAT level

• Partial consistency that is enforced by refinement of disjunctive plans can also be done at the SAT level through resolution

  • But the resolution will be undirected
    • will consider clauses from multiple levels
  • and thus can be costly

• Moral: Refinements allow directed consistency enforcement..

~ load-A-1 V ~load-B-1]

in-A-1 => load-A-1

in-B-1 => load-B-1

With resolution, we get

~In-A-1 V ~In-A-2

Previous slide

Next slide

Back to first slide

View graphic version