Simplifying (SAT) encodings

• Constraint propagation...

  • Unit propagation P , ~P V Q => Q
  • Pure literal elimination (If a proposition occurs with the same polarity in any clause that it occurs in, set it to True)
    • Works only when all satisfying assignments are considered equivalent [Wolfe & Weld, IJCAI-99]

• Syntactic manipulations:

  • Resolve away dependent variables
    • Fluent or Action variables can be eliminated in state-based encodings
      • P11--A12--P22 becomes P11 => P22

• Compilation Tricks

  • Split n-ary actions & propositions to 2-ary ones
    • Move(x,y,z,t) leads to O( #obj * #obj * #obj X k) variables
    • MB(x,t), MF(y,t), M(z, t) leads to 3*O(#obj, k) variables

Previous slide

Next slide

Back to first slide

View graphic version