Non-HTN domain knowledge for SAT encodings

Invariants: A truck is at only one location

at(truck, loc1, I) & loc1 != loc2 => ~at(truck, loc2, I)

Optimality: Do not return a package to a location

at(pkg, loc, I) & ~at(pkg,loc,I+1) & I<J => ~at(pkg,loc,j)

Simplifying: Once a truck is loaded, it should immediately move

~in(pkg,truck,I) & in(pkg,truck,I+1) & at(truck, loc, I+1) =>

~at(truck, loc, I+2)

Once again, additional clauses first increase the encoding size

but make them easier to solve after simplification

(unit-propagation etc).

[Kautz & Selman, AIPS-98]