Reduction from IMP- to SAS+

[wimmers]

We need to reduce IMP- to the SAS+ planning formalism.

In this step, we will need to rely on the existence of polynomial bounds to generate a finite transition system from a given IMP- input program. We get a polynomial bound for the number of computation steps in the input size from to the definition of NP. We then prove that the sizes of the numbers stored in registers are also polynomially bounded. This allows us to apply a technique like bit-blasting to translate the arithmetic operations on registers.

Proof obligations:

• Functional correctness of the translation
• Polynomial size bound on the transition system

Questions:

• Should Turing machines be an intermediate translation step?

A reference on SAS+: https://www.jair.org/index.php/jair/article/view/10751/25678

7 is on the critical path for this.

[notiho]

I want to be assigned this issue

[notiho]

I think that during our last discussion Mohammad said that in general, the size of numbers stored in the registers can't be polynomially bounded, and only the number of distinct values each variable can take during the execution is polynomially bounded. Hence, I would pursue an approach that is slightly different than what described above.

[notiho]

It appears that that in order to implement this, one does need to rely on something like bit blasting.

[maxhaslbeck]

Discussions with @notiho, @BilelGho and @mabdula uncovered some issues with the reduction from IMP- to SAS+. As a result we will try to first tackle a simpler problem (#24), finish the whole pipeline to SAT for it and then tackle this issue afterwards.

[notiho]

Since it turns out #24 is already not that easy, @mabdula and I think that it makes sense to solve this using #28 in combination with #24.