How does SATPLAN use the 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
-