Goal specification #108

vakker · 2022-06-30T13:08:12Z

vakker
Jun 30, 2022

Hi,

I'm experimenting with the blocks example, I haven't modified the domain spec in block2.lisp.
I have 3 main issues at the moment.

The planner doesn't solve the problem

When I try a very simple 3 block problem, e.g.:

(make-problem 'problem3 'blocks-normal
              '((arm-empty)
                (block b1)
                (block b2)
                (block b3)
                (on-table b1) (on b2 b1)
                (on-table b3)
                )
              '((achieve-goals ((on-table b2)
                                (on b1 b3))
                 ))
              )

That results in:

((((ACHIEVE-GOALS ((ON-TABLE B2) (ON B1 B3)))
   ((ASSERT-GOALS ((ON-TABLE B2) (ON B1 B3)) NIL)
    ((ASSERT-GOALS ((ON B1 B3)) ((GOAL (ON-TABLE B2))))
     ((ASSERT-GOALS NIL ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))
      (0 (!ASSERT ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2)))) 0))))
   ((FIND-NOMOVE) (0 (!ASSERT ((DONT-MOVE B3))) 1)))))

with the final state:

 (DONT-MOVE B3)
 (GOAL (ON B1 B3))
 (GOAL (ON-TABLE B2))
 (ON B2 B1)
 (ON-TABLE B3)
 (ON-TABLE B1)
 (BLOCK B3)
 (BLOCK B2)
 (BLOCK B1)
 (ARM-EMPTY)

The planner finds a solution (that still doesn't solve the problem) to contradicting goal specifications.

(make-problem 'problem3 'blocks-normal
              '((arm-empty)
                (block b1)
                (block b2)
                (block b3)
                (on-table b1) (on b2 b1)
                (on-table b3)
                )
              '((achieve-goals ((on-table b2)
                                (on b1 b3)
                                (on b3 b1)
                                )
                 ))
              )

Plan:

((((ACHIEVE-GOALS ((ON-TABLE B2) (ON B1 B3) (ON B3 B1)))
   ((ASSERT-GOALS ((ON-TABLE B2) (ON B1 B3) (ON B3 B1)) NIL)
    ((ASSERT-GOALS ((ON B1 B3) (ON B3 B1)) ((GOAL (ON-TABLE B2))))
     ((ASSERT-GOALS ((ON B3 B1)) ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))
      ((ASSERT-GOALS NIL
        ((GOAL (ON B3 B1)) (GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))
       (0 (!ASSERT ((GOAL (ON B3 B1)) (GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))
        0))))))))

State:

 (GOAL (ON B3 B1))
 (GOAL (ON B1 B3))
 (GOAL (ON-TABLE B2))
 (ON B2 B1)
 (ON-TABLE B3)
 (ON-TABLE B1)
 (BLOCK B3)
 (BLOCK B2)
 (BLOCK B1)
 (ARM-EMPTY)

The planner finds a solution (that still doesn't solve the problem) to goal specifications with terms missing from the problem all together:

(make-problem 'problem3 'blocks-normal
              '((arm-empty)
                (block b1)
                (block b2)
                (block b3)
                (on-table b1) (on b2 b1)
                (on-table b3)
                )
              '((achieve-goals ((on-table b2)
                                (on b1 b3)
                                (dummy 1)
                                )
                 ))
              )

Is this intended? Am I missing something?

Answered by rpgoldman

Jun 30, 2022

With respect to your first question, it looks like there is a combination of two problems:

The blocks domain simply returns a plan when it fails, instead of noticing it's at a dead end. When I add a verify-solution task to the method for achieve-goals, SHOP no longer claims to have a solution for problem3. Here's what I added:

(:method (achieve-goals ?goals)
       ()
       ((assert-goals ?goals nil)
        (find-nomove) (add-new-goals) (find-movable) (move-block) (verify-solution)))

    (:method (verify-solution)
      (and (setof ?g (goal ?g) ?gs)
           (all-true ?gs))
      ()
      )

    (:- (all-true nil)
        ())

    (:- (all-true (?g . ?rest))
        (and ?g
     …

View full answer

rpgoldman · 2022-06-30T16:30:04Z

rpgoldman
Jun 30, 2022
Maintainer

With respect to your first question, it looks like there is a combination of two problems:

The blocks domain simply returns a plan when it fails, instead of noticing it's at a dead end. When I add a verify-solution task to the method for achieve-goals, SHOP no longer claims to have a solution for problem3. Here's what I added:

(:method (achieve-goals ?goals)
       ()
       ((assert-goals ?goals nil)
        (find-nomove) (add-new-goals) (find-movable) (move-block) (verify-solution)))

    (:method (verify-solution)
      (and (setof ?g (goal ?g) ?gs)
           (all-true ?gs))
      ()
      )

    (:- (all-true nil)
        ())

    (:- (all-true (?g . ?rest))
        (and ?g
             (all-true ?rest)))

This leads immediately to the second question: "why doesn't SHOP find a solution to this problem?" The answer is that SHOP needs to know that blocks are clear in order to be able to move them. Here is the repaired problem definition:

(make-problem 'problem3-revised 'blocks-normal
          '((arm-empty)
            (block b1)
            (block b2)
            (block b3)
            (on-table b1) (on b2 b1)
            (on-table b3)
            (clear b3)
            (clear b2)
            )
          '((achieve-goals ((on-table b2)
                            (on b1 b3))
             ))
          )

The contradictory problem oddity is explained the same way. If you add my check for correct plan to the domain definition and add the relevant clear facts to the problem definition, SHOP fails to find a plan (as it should).
I have not verified, but I'm pretty sure that the reason for this is the same as above: SHOP simply returns whatever it has as a plan when it's done planning, whether it's found a plan or whether it's just hit a dead end.

I will update blocks2.lisp to have the plan correctness check.

8 replies

rpgoldman Jul 1, 2022
Maintainer

I am seeing the same thing. I checked the axiom, which appears to be working as expected. I haven't had time to fully check the planning transcript (see below). Please have a look at it yourself, and see if you can find anything. If nothing else, it will give you experience debugging SHOP! I will be looking over it, too, but the more eyeballs the better.

Checking the Axiom

I added the axiom, and by using (shop-trace :goals), I can see that the axiom is being used. I have tested the axiom, and as far as I can tell right now, it gives the right results:

SHOP-USER> (query '((clear b3)) (shop::problem-state 'axiom-blocks-problem) :domain 'blocks-axiom)


Level 0, trying to satisfy goal (CLEAR B3)

Level 0, axiom matches goal (CLEAR B3)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1091 :VAL B3))

Level 2, trying to satisfy goal (ON #:?_OTHER7971092 B3)

Level 2, candidate fact (ON B2 B1) fails to match goal (ON #:?_OTHER7971092 B3)


Level 2, state axioms fail goal (ON #:?_OTHER7971092 B3)

Level 2, couldn't match goal (ON #:?_OTHER7971092 B3)

Level 0, matched goal (CLEAR B3)
(NIL)
NIL
SHOP-USER> (query '((clear b2)) (shop::problem-state 'axiom-blocks-problem) :domain 'blocks-axiom)


Level 0, trying to satisfy goal (CLEAR B2)

Level 0, axiom matches goal (CLEAR B2)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1093 :VAL B2))

Level 2, trying to satisfy goal (ON #:?_OTHER7971094 B2)

Level 2, candidate fact (ON B2 B1) fails to match goal (ON #:?_OTHER7971094 B2)


Level 2, state axioms fail goal (ON #:?_OTHER7971094 B2)

Level 2, couldn't match goal (ON #:?_OTHER7971094 B2)

Level 0, matched goal (CLEAR B2)
(NIL)
NIL
SHOP-USER> (query '((clear b1)) (shop::problem-state 'axiom-blocks-problem) :domain 'blocks-axiom)


Level 0, trying to satisfy goal (CLEAR B1)

Level 0, axiom matches goal (CLEAR B1)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1095 :VAL B1))

Level 2, trying to satisfy goal (ON #:?_OTHER7971096 B1)

Level 2, state fact (ON B2 B1) satisfies goal (ON #:?_OTHER7971096 B1)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?_OTHER7971096 :VAL B2))

Level 0, state axioms fail goal (CLEAR B1)

Level 0, couldn't match goal (CLEAR B1)
NIL
NIL
SHOP-USER>

That agrees with the set of clear facts I added to fix the original problem.

Planning still fails

Here's the transcript of the failing plan session:

SHOP-USER> (find-plans 'axiom-blocks-problem)

---------------------------------------------------------------------------
Problem #<SHOP3::PROBLEM AXIOM-BLOCKS-PROBLEM> with :WHICH = :FIRST, :VERBOSE = 1


Depth 0, trying task (:TASK ACHIEVE-GOALS ((ON-TABLE B2) (ON B1 B3)))

Depth 0, reduced task (:TASK ACHIEVE-GOALS ((ON-TABLE B2) (ON B1 B3)))
 reduction (:ORDERED
            (:TASK :IMMEDIATE ASSERT-GOALS ((ON-TABLE B2) (ON B1 B3)) NIL)
            (:TASK FIND-NOMOVE) (:TASK ADD-NEW-GOALS) (:TASK FIND-MOVABLE)
            (:TASK MOVE-BLOCK) (:TASK VERIFY-SOLUTION))

Depth 1, trying task (:TASK :IMMEDIATE ASSERT-GOALS ((ON-TABLE B2) (ON B1 B3))
                      NIL)

Depth 1, reduced task (:TASK :IMMEDIATE ASSERT-GOALS ((ON-TABLE B2) (ON B1 B3))
                       NIL)
 reduction (:ORDERED
            (:TASK :IMMEDIATE ASSERT-GOALS ((ON B1 B3)) ((GOAL (ON-TABLE B2)))))

Depth 2, trying task (:TASK :IMMEDIATE ASSERT-GOALS ((ON B1 B3))
                      ((GOAL (ON-TABLE B2))))

Depth 2, reduced task (:TASK :IMMEDIATE ASSERT-GOALS ((ON B1 B3))
                       ((GOAL (ON-TABLE B2))))
 reduction (:ORDERED
            (:TASK :IMMEDIATE ASSERT-GOALS NIL
             ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2)))))

Depth 3, trying task (:TASK :IMMEDIATE ASSERT-GOALS NIL
                      ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))

Depth 3, reduced task (:TASK :IMMEDIATE ASSERT-GOALS NIL
                       ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))
 reduction (:ORDERED
            (:TASK :IMMEDIATE !!ASSERT
             ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2)))))

Depth 4, trying task (:TASK :IMMEDIATE !!ASSERT
                      ((GOAL (ON B1 B3)) (GOAL (ON-TABLE B2))))

Depth 5, trying task (:TASK FIND-NOMOVE)

Level 0, trying to satisfy goal (BLOCK #:?X1110)

Level 0, state fact (BLOCK B3) satisfies goal (BLOCK #:?X1110)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1110 :VAL B3))

Level 2, trying to satisfy goal (DONT-MOVE B3)

Level 2, state axioms fail goal (DONT-MOVE B3)

Level 2, couldn't match goal (DONT-MOVE B3)

Level 3, trying to satisfy goal (NEED-TO-MOVE B3)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE1--763
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON B3 #:?Y1112)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B3 #:?Y1112)


Level 5, state axioms fail goal (ON B3 #:?Y1112)

Level 5, couldn't match goal (ON B3 #:?Y1112)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE2--764
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON-TABLE B3)

Level 5, state fact (ON-TABLE B3) satisfies goal (ON-TABLE B3)
satisfiers NIL

Level 6, trying to satisfy goal (GOAL (ON B3 #:?Z1113))

Level 6, candidate fact (GOAL (ON B1 B3)) fails to match goal (GOAL
                                                               (ON B3 #:?Z1113))


Level 6, candidate fact (GOAL (ON-TABLE B2)) fails to match goal (GOAL
                                                                  (ON B3
                                                                   #:?Z1113))


Level 6, state axioms fail goal (GOAL (ON B3 #:?Z1113))

Level 6, couldn't match goal (GOAL (ON B3 #:?Z1113))

Level 5, state axioms fail goal (ON-TABLE B3)

Level 5, matched goal (ON-TABLE B3)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE3--765
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON B3 #:?Y1112)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B3 #:?Y1112)


Level 5, state axioms fail goal (ON B3 #:?Y1112)

Level 5, couldn't match goal (ON B3 #:?Y1112)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE4--766
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON B3 #:?Y1112)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B3 #:?Y1112)


Level 5, state axioms fail goal (ON B3 #:?Y1112)

Level 5, couldn't match goal (ON B3 #:?Y1112)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE5--767
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON B3 #:?Z1113)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B3 #:?Z1113)


Level 5, state axioms fail goal (ON B3 #:?Z1113)

Level 5, couldn't match goal (ON B3 #:?Z1113)

Level 3, axiom matches goal (NEED-TO-MOVE B3)
     axiom #:NEED-TO-MOVE6--768
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1111 :VAL B3))

Level 5, trying to satisfy goal (ON B3 #:?W1114)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B3 #:?W1114)


Level 5, state axioms fail goal (ON B3 #:?W1114)

Level 5, couldn't match goal (ON B3 #:?W1114)

Level 3, state axioms fail goal (NEED-TO-MOVE B3)

Level 3, couldn't match goal (NEED-TO-MOVE B3)

Depth 5, reduced task (:TASK FIND-NOMOVE)
 reduction (:ORDERED (:TASK :IMMEDIATE !!ASSERT ((DONT-MOVE B3)))
            (:TASK FIND-NOMOVE))

Depth 6, trying task (:TASK :IMMEDIATE !!ASSERT ((DONT-MOVE B3)))

Depth 7, trying task (:TASK FIND-NOMOVE)

Level 0, trying to satisfy goal (BLOCK #:?X1116)

Level 0, state fact (BLOCK B3) satisfies goal (BLOCK #:?X1116)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1116 :VAL B3))

Level 2, trying to satisfy goal (DONT-MOVE B3)

Level 2, state fact (DONT-MOVE B3) satisfies goal (DONT-MOVE B3)
satisfiers NIL

Level 0, state fact (BLOCK B2) satisfies goal (BLOCK #:?X1116)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1116 :VAL B2))

Level 2, trying to satisfy goal (DONT-MOVE B2)

Level 2, state axioms fail goal (DONT-MOVE B2)

Level 2, couldn't match goal (DONT-MOVE B2)

Level 3, trying to satisfy goal (NEED-TO-MOVE B2)

Level 3, axiom matches goal (NEED-TO-MOVE B2)
     axiom #:NEED-TO-MOVE1--763
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1117 :VAL B2))

Level 5, trying to satisfy goal (ON B2 #:?Y1118)

Level 5, state fact (ON B2 B1) satisfies goal (ON B2 #:?Y1118)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?Y1118 :VAL B1))

Level 6, trying to satisfy goal (GOAL (ON B2 #:?Z1119))

Level 6, candidate fact (GOAL (ON B1 B3)) fails to match goal (GOAL
                                                               (ON B2 #:?Z1119))


Level 6, candidate fact (GOAL (ON-TABLE B2)) fails to match goal (GOAL
                                                                  (ON B2
                                                                   #:?Z1119))


Level 6, state axioms fail goal (GOAL (ON B2 #:?Z1119))

Level 6, couldn't match goal (GOAL (ON B2 #:?Z1119))

Level 5, state axioms fail goal (ON B2 #:?Y1118)

Level 5, matched goal (ON B2 #:?Y1118)

Level 3, axiom matches goal (NEED-TO-MOVE B2)
     axiom #:NEED-TO-MOVE2--764
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1117 :VAL B2))

Level 5, trying to satisfy goal (ON-TABLE B2)

Level 5, state axioms fail goal (ON-TABLE B2)

Level 5, couldn't match goal (ON-TABLE B2)

Level 3, axiom matches goal (NEED-TO-MOVE B2)
     axiom #:NEED-TO-MOVE3--765
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1117 :VAL B2))

Level 5, trying to satisfy goal (ON B2 #:?Y1118)

Level 5, state fact (ON B2 B1) satisfies goal (ON B2 #:?Y1118)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?Y1118 :VAL B1))

Level 6, trying to satisfy goal (GOAL (ON-TABLE B2))

Level 6, candidate fact (GOAL (ON B1 B3)) fails to match goal (GOAL
                                                               (ON-TABLE B2))


Level 6, state fact (GOAL (ON-TABLE B2)) satisfies goal (GOAL (ON-TABLE B2))
satisfiers NIL

Level 6, state axioms fail goal (GOAL (ON-TABLE B2))

Level 6, matched goal (GOAL (ON-TABLE B2))

Level 5, state axioms fail goal (ON B2 #:?Y1118)

Level 5, matched goal (ON B2 #:?Y1118)

Level 0, state fact (BLOCK B1) satisfies goal (BLOCK #:?X1116)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1116 :VAL B1))

Level 2, trying to satisfy goal (DONT-MOVE B1)

Level 2, state axioms fail goal (DONT-MOVE B1)

Level 2, couldn't match goal (DONT-MOVE B1)

Level 3, trying to satisfy goal (NEED-TO-MOVE B1)

Level 3, axiom matches goal (NEED-TO-MOVE B1)
     axiom #:NEED-TO-MOVE1--763
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1121 :VAL B1))

Level 5, trying to satisfy goal (ON B1 #:?Y1122)

Level 5, candidate fact (ON B2 B1) fails to match goal (ON B1 #:?Y1122)


Level 5, state axioms fail goal (ON B1 #:?Y1122)

Level 5, couldn't match goal (ON B1 #:?Y1122)

Level 3, axiom matches goal (NEED-TO-MOVE B1)
     axiom #:NEED-TO-MOVE2--764
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1121 :VAL B1))

Level 5, trying to satisfy goal (ON-TABLE B1)

Level 5, state fact (ON-TABLE B1) satisfies goal (ON-TABLE B1)
satisfiers NIL

Level 6, trying to satisfy goal (GOAL (ON B1 #:?Z1123))

Level 6, state fact (GOAL (ON B1 B3)) satisfies goal (GOAL (ON B1 #:?Z1123))
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?Z1123 :VAL B3))

Level 6, candidate fact (GOAL (ON-TABLE B2)) fails to match goal (GOAL
                                                                  (ON B1
                                                                   #:?Z1123))


Level 6, state axioms fail goal (GOAL (ON B1 #:?Z1123))

Level 6, matched goal (GOAL (ON B1 #:?Z1123))

Level 5, state axioms fail goal (ON-TABLE B1)

Level 5, matched goal (ON-TABLE B1)

Level 0, state axioms fail goal (BLOCK #:?X1116)

Level 0, matched goal (BLOCK #:?X1116)

Depth 7, reduced task (:TASK FIND-NOMOVE)
 reduction (:ORDERED (:TASK :IMMEDIATE SHOP3::!!INOP))

Depth 8, trying task (:TASK :IMMEDIATE SHOP3::!!INOP)

Depth 9, trying task (:TASK ADD-NEW-GOALS)

Level 0, trying to satisfy goal (BLOCK #:?X1125)

Level 0, state fact (BLOCK B3) satisfies goal (BLOCK #:?X1125)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1125 :VAL B3))

Level 2, trying to satisfy goal (DONT-MOVE B3)

Level 2, state fact (DONT-MOVE B3) satisfies goal (DONT-MOVE B3)
satisfiers NIL

Level 0, state fact (BLOCK B2) satisfies goal (BLOCK #:?X1125)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1125 :VAL B2))

Level 2, trying to satisfy goal (DONT-MOVE B2)

Level 2, state axioms fail goal (DONT-MOVE B2)

Level 2, couldn't match goal (DONT-MOVE B2)

Level 3, trying to satisfy goal (GOAL (ON-TABLE B2))

Level 3, candidate fact (GOAL (ON B1 B3)) fails to match goal (GOAL
                                                               (ON-TABLE B2))


Level 3, state fact (GOAL (ON-TABLE B2)) satisfies goal (GOAL (ON-TABLE B2))
satisfiers NIL

Level 0, state fact (BLOCK B1) satisfies goal (BLOCK #:?X1125)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1125 :VAL B1))

Level 2, trying to satisfy goal (DONT-MOVE B1)

Level 2, state axioms fail goal (DONT-MOVE B1)

Level 2, couldn't match goal (DONT-MOVE B1)

Level 3, trying to satisfy goal (GOAL (ON-TABLE B1))

Level 3, candidate fact (GOAL (ON B1 B3)) fails to match goal (GOAL
                                                               (ON-TABLE B1))


Level 3, candidate fact (GOAL (ON-TABLE B2)) fails to match goal (GOAL
                                                                  (ON-TABLE B1))


Level 3, state axioms fail goal (GOAL (ON-TABLE B1))

Level 3, couldn't match goal (GOAL (ON-TABLE B1))

Level 4, trying to satisfy goal (GOAL (ON B1 #:?Y1126))

Level 4, state fact (GOAL (ON B1 B3)) satisfies goal (GOAL (ON B1 #:?Y1126))
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?Y1126 :VAL B3))

Level 0, state axioms fail goal (BLOCK #:?X1125)

Level 0, matched goal (BLOCK #:?X1125)

Depth 9, reduced task (:TASK ADD-NEW-GOALS)
 reduction (:ORDERED (:TASK :IMMEDIATE SHOP3::!!INOP))

Depth 10, trying task (:TASK :IMMEDIATE SHOP3::!!INOP)

Depth 11, trying task (:TASK FIND-MOVABLE)

Level 0, trying to satisfy goal (CLEAR #:?X1127)

Level 0, axiom matches goal (CLEAR #:?X1127)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1127 :VAL #:?BLOCK1129))

Level 2, trying to satisfy goal (ON #:?_OTHER7971130 #:?BLOCK1129)

Level 2, state fact (ON B2 B1) satisfies goal (ON #:?_OTHER7971130 #:?BLOCK1129)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?_OTHER7971130 :VAL B2)
            #S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1129 :VAL B1))

Level 0, state axioms fail goal (CLEAR #:?X1127)

Level 0, couldn't match goal (CLEAR #:?X1127)

Level 0, trying to satisfy goal (CLEAR #:?X1127)

Level 0, axiom matches goal (CLEAR #:?X1127)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1127 :VAL #:?BLOCK1131))

Level 2, trying to satisfy goal (ON #:?_OTHER7971132 #:?BLOCK1131)

Level 2, state fact (ON B2 B1) satisfies goal (ON #:?_OTHER7971132 #:?BLOCK1131)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?_OTHER7971132 :VAL B2)
            #S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1131 :VAL B1))

Level 0, state axioms fail goal (CLEAR #:?X1127)

Level 0, couldn't match goal (CLEAR #:?X1127)

Depth 11, reduced task (:TASK FIND-MOVABLE)
 reduction (:ORDERED (:TASK :IMMEDIATE SHOP3::!!INOP))

Depth 12, trying task (:TASK :IMMEDIATE SHOP3::!!INOP)

Depth 13, trying task (:TASK MOVE-BLOCK)

Level 0, trying to satisfy goal (STACK-ON-BLOCK #:?X1133 #:?Y1134)

Level 0, state axioms fail goal (STACK-ON-BLOCK #:?X1133 #:?Y1134)

Level 0, couldn't match goal (STACK-ON-BLOCK #:?X1133 #:?Y1134)

Level 0, trying to satisfy goal (PUT-ON-TABLE #:?X1133)

Level 0, state axioms fail goal (PUT-ON-TABLE #:?X1133)

Level 0, couldn't match goal (PUT-ON-TABLE #:?X1133)

Level 0, trying to satisfy goal (CLEAR #:?X1133)

Level 0, axiom matches goal (CLEAR #:?X1133)
     axiom #:CLEAR1--796
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?X1133 :VAL #:?BLOCK1135))

Level 2, trying to satisfy goal (ON #:?_OTHER7971136 #:?BLOCK1135)

Level 2, state fact (ON B2 B1) satisfies goal (ON #:?_OTHER7971136 #:?BLOCK1135)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?_OTHER7971136 :VAL B2)
            #S(SHOP3.UNIFIER::BINDING :VAR #:?BLOCK1135 :VAL B1))

Level 0, state axioms fail goal (CLEAR #:?X1133)

Level 0, couldn't match goal (CLEAR #:?X1133)

Depth 13, reduced task (:TASK MOVE-BLOCK)
 reduction (:ORDERED (:TASK :IMMEDIATE SHOP3::!!INOP))

Depth 14, trying task (:TASK :IMMEDIATE SHOP3::!!INOP)

Depth 15, trying task (:TASK VERIFY-SOLUTION)

Level 0, trying to satisfy goal (GOAL #:?G1137)

Level 0, state fact (GOAL (ON B1 B3)) satisfies goal (GOAL #:?G1137)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?G1137 :VAL (ON B1 B3)))

Level 0, state fact (GOAL (ON-TABLE B2)) satisfies goal (GOAL #:?G1137)
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?G1137 :VAL (ON-TABLE B2)))

Level 0, state axioms fail goal (GOAL #:?G1137)

Level 0, matched goal (GOAL #:?G1137)

Level 2, trying to satisfy goal (ALL-TRUE ((ON-TABLE B2) (ON B1 B3)))

Level 2, axiom matches goal (ALL-TRUE ((ON-TABLE B2) (ON B1 B3)))
     axiom #:ALL-TRUE1--798
satisfiers (#S(SHOP3.UNIFIER::BINDING :VAR #:?G1139 :VAL (ON-TABLE B2))
            #S(SHOP3.UNIFIER::BINDING :VAR #:?REST1140 :VAL ((ON B1 B3))))

Level 4, trying to satisfy goal (ON-TABLE B2)

Level 4, state axioms fail goal (ON-TABLE B2)

Level 4, couldn't match goal (ON-TABLE B2)

Level 2, state axioms fail goal (ALL-TRUE ((ON-TABLE B2) (ON B1 B3)))

Level 2, couldn't match goal (ALL-TRUE ((ON-TABLE B2) (ON B1 B3)))
Totals: Plans Mincost Maxcost Expansions Inferences  CPU time  Real time
           0       -       -         16         74     0.001      0.001

NIL
0.001209 (0.1209%)
SHOP-USER>

rpgoldman Jul 1, 2022
Maintainer

Aha! I see the problem. The problem has to do with a subtlety about negation in logic programming. SHOP wants to find any block that is clear:

        ;; Find all those blocks which can be moved to their final position
        ;; directly in the initial state of the world. Such blocks are marked
        ;; with either a put-on-table predicate or a stack-on-block predicate,
        ;; depending on their associated goal
        (:method (find-movable)
           (:first (clear ?x) (not (dont-move ?x))
                   (goal (on-table ?x)) (not (put-on-table ?x)))
                                        ; Decomposition
           ((!!assert ((put-on-table ?x))) (find-movable))

           (:first (clear ?x) (not (dont-move ?x)) (goal (on ?x ?y))
                   (not (stack-on-block ?x ?y)) (dont-move ?y) (clear ?y))
                                        ;Decomposition
           ((!!assert ((stack-on-block ?x ?y))) (find-movable))

           nil
           nil)

This cannot be done with negation-as-failure, which is how NOT works in the SHOP theorem prover. With ?x unbound, if you ask SHOP to satisfy (clear ?x), you are asking it to prove that all blocks are clear, which is not true. Negation by failure as in your axiom will only work as expected here when you are asking (not (on ?_ ?x)) if ?x is bound.

vakker Jul 7, 2022
Author

Ah, I see, thanks a lot for debugging it, that's really non-trivial.

So, as a workaround, this could work (as the first method in achieve-goals):

        (:method (find-clear)
           (:first (block ?x) (not (clear ?x)) (not (on ?_ ?x)))
           ((!assert ((clear ?x))) (find-clear))
           nil
           nil)

Out of curiosity, is there any way to make the axiom work without that workaround? I guess the "if ?x is bound" can only be a solution if the methods are refactored completely.
But with that axiom the example would be much simpler, because then none of the (!assert ((clear ?x))) statements are needed.

rpgoldman Jul 7, 2022
Maintainer

I haven't done this myself, but:

(:- (clear ?x) ((block ?x) (not (on ?_ ?x)))

would likely work. That way ?x would be bound before you get to checking the negation. Note, though, that this would make each invocation of clear potentially evaluate the rule for every block in the domain (if there were no clear blocks), which could be expensive. If the clear predicate was used a lot, it would be cheaper to eagerly compute it (write it in the domain as here) rather than lazily compute it with a rule.

Note also that in the original PDDL domain from which the SHOP domain was derived there are no axioms, and the limitations on the PDDL dialect means that axioms cannot be used.

In the planning competition, from which this domain was derived, axioms are not favored by the competitors. This makes sense because they complicate the planner in order to make domain specifications easier. But the competitors don't engineer domains! They are given them. Hence little incentive for competitors to submit planners supporting axioms.

I do build domains, so I very much favor axioms!

vakker Jul 7, 2022
Author

Great, that works, thanks!
Yeah, I'm also trying to build domains, and the less I need to manually specify, the better :)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Goal specification #108

{{title}}

Replies: 1 comment 8 replies

{{title}}

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

{{title}}

Select a reply

Goal specification #108

vakker Jun 30, 2022

Replies: 1 comment · 8 replies

rpgoldman Jun 30, 2022 Maintainer

rpgoldman Jul 1, 2022 Maintainer

Checking the Axiom

Planning still fails

rpgoldman Jul 1, 2022 Maintainer

vakker Jul 7, 2022 Author

rpgoldman Jul 7, 2022 Maintainer

vakker Jul 7, 2022 Author

vakker
Jun 30, 2022

Replies: 1 comment 8 replies

rpgoldman
Jun 30, 2022
Maintainer

rpgoldman Jul 1, 2022
Maintainer

rpgoldman Jul 1, 2022
Maintainer

vakker Jul 7, 2022
Author

rpgoldman Jul 7, 2022
Maintainer

vakker Jul 7, 2022
Author