This is another one of those “mainly ignore most of the problem” reductions.

**The Problem: **Inequivalence of Loop Programs Without Nesting.Ā This is problem PO14 of the appendix.

**The description: **Given:

- a set of X variables,
- a subset Y of X which are “input” variables,
- a specific output variable x
_{0} - Two programs P
_{1}and P_{2}with the commands:- x <- y (x gets a copy of y)
- x <- 0Ā (x gets set to 0)
- x<- x + 1 (x is incremented by 1)
- DO x
_{i }{S_{1}S_{2}..S_{n}} ENDĀ (see below)

.. is there a way to assign the variablse in Y so that P_{1} and P_{2 } produce *different* outputs in our output variable x_{0}?

**Example: ** The semantics of the “DO” statement are (they’re better described by Tsichrtizis in his paper) that we execute the loop body a number of times equal to the value of x_{i} (if it is 0, we do not execute the loop at all).Ā The S_{i} statements can be any program statement except another loop (since we are looking at programs without nesting- even allowing one level of nesting makes this problem undecidable).

So, here are two programs x_{1} is our input variable and x_{0} is our output variable:

**P1:**

x_{0} <- 0

DO x_{1}

x_{0 }<- x_{0} + 1

END

**P2:**

x_{0} <- x_{1}

These programs are equivalent as long as we do not allow our input values to be negative (which seems to be the convention) because both programs will copy the integer value in x_{1} into x_{0} (though P1 does it more slowly).Ā Suppose we used the alternate P1

**P1′:**

x_{0} <- 0

DO x_{1}

x_{0 }<- x_{0} + 1

x_{0} <- x_{0} + 1

END

..this has the effect of making x_{0}‘s value twice the value of x_{1}.Ā While P1 and P2 will still have the same value in x_{0} if x_{1}=0, any other value in x_{1} will result in different outputs, making our programs inequivalent.

**Reduction: **Constable, Hunt, and Sahni use 3SAT.Ā The basic idea is to use loops that execute at most once as if statements.Ā (I don’t think they have a loop that iterates more than once in the whole program).Ā So for example, they will set up a clause variable C_{i} that will be set to 1 if any of its literal variables are true with a subprogram like:

C_{i} <- 0

DO C_{i1}Ā (C_{i1} is the first literal of clause i)

C_{i} <- 1 (Technically this is C_{i} <- 0 followed by C_{i} <- C_{i} +1)

END

DO C_{i2}

C_{i} <- 1

END

DO C_{i3}

C_{i} <- 1

END

..each of the loops will set C_{i} to 1 if the literal is true, and leave it alone if the literal is false.

So, with that in mind, we take a 3SAT formula and write a program:

- Our input variables are the variables to the formula.
- We create the negations of all of the variables in an if statementĀ (this way we have both positive and negative literals for each variable)
- We compute all of the C
_{i}variables as above - We compute the negations of all of the C
_{i}variables. (we need this because our loop-based if statement can only do things if a variable is 1, not 0) - We create a variable P that is initially 1.Ā If any of the negated C
_{i}variables are 1 (so the regular C_{i}variable was 0, so the clause was not satisfied), we reset P to 0.Ā P is our output variable.

This program will output P to 1 if its inputs form a satisfiable arrangement of variables, and will output 0 otherwise.Ā This is our P1 program.

Our P2 program is a program that always outputs 0.Ā P1 and P2 will be different if and only if the formula is satisfiable.

**Difficulty: **5. The reduction itself is pretty easy- “write a program that sees if the inputs are satisfiable”.Ā The hard part is realizing that you don’t really use the loop structure as a loop, and that you aren’t searching for an input to make it satisfiable, you’re just using whatever input the SAT instance gives you.