Case Study: SATPLAN with domain specific knowledge
Instantiate the domain specific rules as well, and then add them to the encoding.
Solve the full encoding…
- Won’t the encoding size increase with domain spefic rules?
- Yes, but the new rules support a lot of simplification so that after simplification, the encoding size actually reduces!!
Example in Blocks world (from Kautz & Selman, AIPS-99)
BW-c:
Original:
4258 vars (10% increase) /
30986 clauses (300% increase)
Final (after simplification):
3526 vars
22535 clauses