Inefficient existential preconditions resolution

[Rezenders]

Hi @fmrico,

Unfortunately, the solution I proposed for existential predicates is inefficient. It is literally exploring the whole state space to check if the predicates are satisfied. This can easily explode. For example, if there are 75 instances and an existential precondition has 5 variables, this results in 75^5 possible combinations to check, which is unfeasible.

A concrete example (complete formulation can be found here):

    (:derived (inferred-Fg_status ?fg ?IN_ERROR_NFR_string)
        (and
            (= ?IN_ERROR_NFR_string IN_ERROR_NFR_string)
            (exists (?mqa ?eqa ?mqav ?fd ?eqav)
                (and
                    (inferred-FunctionGrounding ?fg)
                    (inferred-HasQAvalue ?fg ?mqa)
                    (inferred-IsQAtype ?eqa water_visibility)
                    (inferred-HasValue ?mqa ?mqav)
                    (inferred-TypeFD ?fg ?fd)
                    (inferred-HasValue ?eqa ?eqav)
                    (inferred-HasQAestimation ?fd ?eqa)
                    (inferred-IsQAtype ?mqa water_visibility)
                    (inferred-FunctionDesign ?fd)
                    (inferred-QAvalue ?mqa)
                    (inferred-QAvalue ?eqa)
                    (inferred-LessThan ?mqav ?eqav)
                )
            )
        )
    )

We need to come up with a mechanism to prune the possible variable combinations. I don't have any good ideas so far.

[tobiaswjohn]

The general procedure should be to start from the state, i.e. known facts and build the set of all derived facts from that. This applies to the existential quantification and the derived predicates.

I assume, that there is a set S that contains all atomic formulas of the form (p a_1 ... a_n) that are true in the current state

• notations:
  • variables are named ?x_1 until ?x_n
  • object names are a_1 until a_n
  • derived predicates have the form (:derived (p ?x_1 ... ?x_n) P'), where the predicate (p ?x_1 ... ?x_n) is derived, if the condition P' is satisfied (where ?x_1,...,?x_n occur freely in P')

Algorithm for derived predicates

• The general semantics of derived predicates is defined in this paper (see page 525 and the algorithm on page 526). The algorithm here is a version of that. In general, the algorithm tries to iteratively apply all rules (function derive) until no additional new facts can be derived.

• algorithm to compute all derived predicates from a state S, i.e. a set of satisfied atomic formulas

  allDerived(S):
  S' := union(S, derive(S))
  while (S != S'):
    S := S'
    S' := union(S, derive(S))
  return S

• one single inference step for the derived predicates

  derive(S):
  D := Set()
  forAll derived predicates derPred:
       case derPred = (:derived (p ?x_1 ... ?x_n) P') :
          E := eval(P', S)
          Derived := {(p a_1 ... a_n) | (x_1=a_1,...,x_n=a_n) in E}
          // CAVE: if some variables are never used in P': add all combinations of them to Derived
          D := union(D, Derived)
  return D

• the function eval returns for a piece of PDDL code (e.g. predicate, existential formula) the possible assignments that hold (given a state)

• variables that do not occur in the assignment are not restricted by the formula → can be assigned any object

• i.e. it maps PDDL code Pand state Sto a set

  {{?x_1=a_1,...,?x_n=a_n}, {?x_1=a_1',...,?x_n=a_n'},...}

eval(P, S):
   case P = (p ?x_1 ... ?x_n) :
      return {{?x_1=a_1,...,?x_n=a_n} | (p a_1 ... a_n) in S}

   case P = (exists (?x_j) P') :
      E := eval(P', S)
      return {{?x_1=a_1,...,?x_n=a_n} | {?x_1=a_1,...,?x_n=a_n, ?x_j=a_j} in E}

   case P = (and (P' R')) :
      E_1 := eval(P', S)
      E_2 := eval(R', S)
      return join(E_1, E_2)   // join via shared variables

Algorithm to decide preconditions

Based on the before mentioned, we can decide, if the precondition of an action is satisfied.

• general algorithm to compute, if preconditions are satisfied: compute all derived predicates → evaluate preconditions based on derived predicates
• algorithm: returns true if precondition is satisfied
• assumption: precondition is something that can be used in evalfunction

  evalPrecond(pre):
   S := state
   S_D := allDerived(S)
   if {?x_1=a_1,...,?x_n=a_n} in eval(pre, S_D): // CAVE: if eval-function does not set all variables --> those can have any value
      return true
   else:
      return false

• note: one could make this more efficient by feeding the already assigned variables to the eval function, but this would make the pseudocode more ugly

[Rezenders]

@tobiaswjohn Thanks! I am working on improving the algorithm with your input. I will come back with some questions soon :)