Open lorangpi opened 5 months ago
Dear Pierrick,
Thanks for reaching out about this. I conducted the experiment as you did successfully. The action schema indeed seems correct. The problem that I see, in the PDDL you sent, is that your interpretation of the predicates is not right. Below, you will find the PDDL annotated by me. The initial/goal situations in the problem must be changed accordingly to fit the right interpretation. It is also important that you include the static predicates in the action schema and the initial state.
Also, the SAT approach is older than the ASP approach that is more easy to play with and adjust, although it could be a less efficient. The SAT approach is designed to be run in a cluster with 100s of nodes so that to solve many SAT instances in parallel.
Best.
(define (domain hanoi) (:requirements :strips :typing) (:types obj) (:predicates (p0 ?obj - obj) ; (not (clear ?obj)) (p1 ?obj1 ?obj2 - obj) ; (not (on ?obj2 ?obj1)) (b0 ?obj1 ?obj2 - obj) ; static (not (equal ?obj1 ?obj2)) (b1 ?obj1 ?obj2 - obj) ; static ?obj1 > ?obj2 )
(:action MOVE ; Move ?obj2 from ?obj0 to ?obj1 [ Hence, ?obj2 must be smaller than ?obj1 ]
:parameters (?obj0 ?obj1 ?obj2 - obj)
:precondition (and (not (p0 ?obj1)) ; (clear ?obj1)
(not (p0 ?obj2)) ; (clear ?obj2)
(p1 ?obj0 ?obj1) ; (not (on ?obj1 ?obj0))
(not (p1 ?obj0 ?obj2)) ; (on ?obj2 ?obj0)
; Here I ignore static predicates to relax the action conditions, for testing purposes
;(b0 ?obj0 ?obj1) ; ?obj0 != ?obj1
;(b0 ?obj0 ?obj2) ; ?obj0 != ?obj2
;(b0 ?obj1 ?obj2) ; ?obj1 != ?obj2
;(b1 ?obj0 ?obj2) ; ?obj0 > ?obj2 [ REDUNDANT ]
;(b1 ?obj1 ?obj2) ; ?obj1 > ?obj2
)
:effect (and (not (p0 ?obj0)) ; (clear ?obj0)
(p0 ?obj1) ; (not (clear ?obj1))
(p1 ?obj0 ?obj2) ; (not (on ?obj2 ?obj0))
(not (p1 ?obj1 ?obj2)) ; (on ?obj2 ?obj1)
))
)
(define (problem hanoi-problem) (:domain hanoi) (:objects o0 o1 o2 o3 o4 o5 - obj) (:init (p0 o0) ; (not (clear o0)) (p0 o1) ; (not (clear o1)) (p0 o2) ; (not (clear o2)) (p1 o0 o2) ; (not (on o2 o0)) (p1 o0 o3) ; (not (on o3 o0)) (p1 o1 o3) ; (not (on o3 o1)) (p1 o4 o1) ; (not (on o4 o1)) (p1 o4 o2) ; (not (on o4 o2)) (p1 o4 o3) ; (not (on o4 o3)) (p1 o5 o1) ; (not (on o5 o1)) (p1 o5 o2) ; (not (on o5 o2)) (p1 o5 o3) ; (not (on o5 o3)) ; Static predicates not in the state, ignored for testing purposes ; [Blai: Static predicates are needed; basically, they say which objects are smaller than others] ) (:goal (and (p0 o0) ; (not (clear o0)) (p0 o4) ; (not (clear o4)) (p0 o5) ; (not (clear o5)) (p1 o0 o1) ; (not (on o1 o0)) (p1 o0 o3) ; (not (on o3 o0)) (p1 o1 o2) ; (not (on o2 o1)) (p1 o1 o3) ; (not (on o3 o1)) (p1 o2 o3) ; (not (on o3 o2)) (p1 o4 o2) ; (not (on o2 o4)) (p1 o4 o3) ; (not (on o3 o4)) (p1 o5 o1) ; (not (on o1 o5)) (p1 o5 o2) ; (not (on o2 o5)) )) )
Hi,
Firstly, thank you for sharing your code publicly! I'm very enthusiastic about your work and would like to demonstrate its application in the field of robotics alongside other methods.
I've been attempting to replicate your results on the Towers of Hanoi problem (3x2 and 3x3). So far, I haven't been able to obtain a working PDDL action schema directly from the SAT solver without needing to make adjustments. For example, I've conducted several trials where I translated the output action schema to a PDDL domain and created a PDDL problem file using the states described in decoded.txt, but the planner I use (MetricFF) would not find a plan.
I've been using the benchmark "benchmarks_hanoi1op_1r.txt". Is this the satisfiable theory you used in the paper? The action schema that was outputted from this theory in hanoi1op_n530/decoded.txt is as follows:
Action schema: action a0 MOVE(?obj0,?obj1,?obj2): static-pre={b0(?obj0,?obj1),b0(?obj0,?obj2),b0(?obj1,?obj2),b1(?obj0,?obj2),b1(?obj1,?obj2)}, pre={-p0(?obj1),-p0(?obj2),p1(?obj0,?obj1),-p1(?obj0,?obj2)}, eff={-p0(?obj0),p0(?obj1),p1(?obj0,?obj2),-p1(?obj1,?obj2)}
However, I've noticed that some preconditions are missing, such as p0(?obj0) (p0 seems to represent NOT CLEAR here as they are negated). Similarly, for p1 (intuitively Non(y,x) - reversed in the paper), the precondition p1(?obj1,?obj2) is missing. (EDIT) This action schema seems even better than in the paper as it ignores unnecessary preconditions. Thus a planner should find a plan (plus I have verified by hand the transitions described in decoded.txt in the 3x2 problem and they are correct)
First: It seems like I'm trying the right theory/benchmark file? I also tried the same theory on the Hanoi 3x2 and 3x4 problems and got similar results. Currently, I'm running benchmark_hanoi1op.txt that lists thousands of theories, but this process seems very slow, and the paper mentions that only one theory satisfies the SAT problem in this domain.
Second: could it be that the planner does not find a plan because of the mix between negations and double negations ? Usually planners assume that unstated predicates are False by default (closed-world assumption), but this planning domain is negated (not clear, not on), which could cause interference maybe.
Have you already tried to use these action schemas to plan using PDDL, and would you have any suggestion?
Here is the command line I used: python experiment.py --remove_dir --dfas_path ../../dfas --verbose 1 benchmarks/benchmarks_hanoi1op_1r.txt 0
Here is the PDDL domain I wrote from the action schema (Note that I ignored static predicates to relax the action conditions, for testing purposes):
(define (domain hanoi) (:requirements :strips :typing) (:types obj)
(:predicates (p0 ?obj - obj) (p1 ?obj1 ?obj2 - obj) (b0 ?obj1 ?obj2 - obj) (b1 ?obj1 ?obj2 - obj) )
(:action MOVE :parameters (?obj0 ?obj1 ?obj2 - obj) :precondition (and (not (p0 ?obj1)) (not (p0 ?obj2)) (p1 ?obj0 ?obj1) (not (p1 ?obj0 ?obj2)) ;(b0 ?obj0 ?obj1) #Here I ignore static predicates to relax the action conditions, for testing purposes ;(b0 ?obj0 ?obj2) ;(b0 ?obj1 ?obj2) ;(b1 ?obj0 ?obj2) ;(b1 ?obj1 ?obj2) ) :effect (and (not (p0 ?obj0)) (p0 ?obj1) (p1 ?obj0 ?obj2) (not (p1 ?obj1 ?obj2)) ) ) )
Here is an example of the PDDL problem syntax I wrote from the states description in decoded.txt (c.f. states below): (define (problem hanoi-problem) (:domain hanoi) (:objects o0 o1 o2 o3 o4 o5 - obj) (:init (p0 o0) #Static predicates not in the state, ignored for testing purposes (p0 o1) (p0 o2) (p1 o0 o2) (p1 o0 o3) (p1 o1 o3) (p1 o4 o1) (p1 o4 o2) (p1 o4 o3) (p1 o5 o1) (p1 o5 o2) (p1 o5 o3) )
(:goal (and (p0 o0) (p0 o4) (p0 o5) (p1 o0 o1) (p1 o0 o3) (p1 o1 o2) (p1 o1 o3) (p1 o2 o3) (p1 o4 o2) (p1 o4 o3) (p1 o5 o1) (p1 o5 o2) )) )
States Used (inital state s0, goal state s26): s0{p0(o0),p0(o1),p0(o2),p1(o0,o2),p1(o0,o3),p1(o1,o3),p1(o4,o1),p1(o4,o2),p1(o4,o3),p1(o5,o1),p1(o5,o2),p1(o5,o3)} s26{p0(o0),p0(o4),p0(o5),p1(o0,o1),p1(o0,o3),p1(o1,o2),p1(o1,o3),p1(o2,o3),p1(o4,o2),p1(o4,o3),p1(o5,o1),p1(o5,o2)}
Thank you for your help! Best,