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
- Lifting (variablized encodings)???