Tag Archives: 3SAT

Inequivalence of Loop Programs Without Nesting

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 x0
  • Two programs P1 and P2 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 xi {S1 S2..Sn} END  (see below)

.. is there a way to assign the variablse in Y so that P1 and P2 produce different outputs in our output variable x0?

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 xi (if it is 0, we do not execute the loop at all).  The Si 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 x1 is our input variable and x0 is our output variable:

P1:

x0 <- 0
DO x1
x0 <- x0 + 1
END

P2:

x0 <- x1

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 x1 into x0 (though P1 does it more slowly).  Suppose we used the alternate P1

P1′:

x0 <- 0
DO x1
x0 <- x0 + 1
x0 <- x0 + 1
END

..this has the effect of making x0‘s value twice the value of x1.  While P1 and P2 will still have the same value in x0 if x1=0, any other value in x1 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 Ci that will be set to 1 if any of its literal variables are true with a subprogram like:

Ci <- 0
DO Ci1  (Ci1 is the first literal of clause i)
Ci <- 1 (Technically this is Ci <- 0 followed by Ci <- Ci +1)
END

DO Ci2
Ci <- 1
END

DO Ci3
Ci <- 1
END

..each of the loops will set Ci 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 Ci variables as above
  • We compute the negations of all of the Ci 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 Ci variables are 1 (so the regular Ci 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.

Inequivalence of Programs with Arrays, Inequivalence of Programs with Assignments

Both of these problems are from the same paper and use basically the same proof, so we’ll do them together.

The Problems: Inequivalence of Programs With Arrays (PO11 in the appendix) and Inequivalence and Programs with Assignments (PO12 in the appendix)

The Description (for Inequivalence of Programs With Assignments): 

Given two programs P and Q that access a common set of variables, S.  Each statement in the program is of the form “x0 <- if x1 = x2 then x3 else x4“, where each xi is a variable from S.  Will the two programs always give different output for all initial variable configurations?

The Description (for Inequivalence of Programs With Assignments):

Same idea, but the possible statements in the program are:

  • Select an element B of an array α: A <- α.B
  • Update an element B of an array α: α.B <- A
  • “Operate” on an operation Φ: A <- Φ B1B2..Bk.  Φ comes from a given finite set of operations and is expected to take a certain number of arguments (k) that we know ahead of time.

Example: The “outputs” of these programs are the final values of the variables.  They denote a “final” value by representing a program as a Directed Acyclic Graph, and the leaf nodes (of outdegree 0) are the variables with final values.  We will specify what variables we care about as output variables

So for example, we might have the one-line program:

k <- if i=j then 2 else 3

Compared to the one-line program:

k <- if i=j then 3 else 2

If k is our output variable, then for all values of i and j both programs will produce different outputs.  If we change our second program to:

k<- if i=j then 2 else 2

…then if we assign i and j the same values, both programs will give the same output.

Reduction (for Inequivalence of Programs With Assignments): Downey and Sethi use 3SAT.  If we start with a formula with variables y1..yn we will create a program with variables {T,F, A1..An, B1..Bn,).  Then we just write a program that checks if all clauses are true.  “D” will be our output variable and will be updated for each clause.  We start it as true initially:

D <- if T = T then T else T // D is true so far

Then we check the first clause.  A variable “C” will be used for each clause.  It starts out false and will be set to true once the clause is satisfied:

C <- if F = F then F else F // C is false so far

Then for each literal x1..x3 we check if it has been made true.  We use Ai if the literal is positive in the clause and Bi if the literal is negative in the clause.  So suppose our clause was (y1, ~y2, y4), we’d have the lines:

// does the first literal make the clause true?
C <- if A1 = T then T else C
// does the second literal make the clause true?
C <- if B2 = T then T else C
// does the third literal make the clause true?
C <- if A4= T then T else C

C now is true if and only if the clause is satisfied, so let’s update D:

// D becomes false if we don't satisfy that clause
D <- if C = T then D else F

We then repeat that process for each clause.  At the end, we add rules saying that a variable and its negation can’t both have the same value:

D <- if A1 = B1 then F else D

..repeated for each variable.

The final output of this program is D, which will be true if our inputs legally satisfied the formula, and false otherwise.

Our second program just outputs the constant “F”.  The programs will produce different outputs if and only if there is a way for the first program to produce a T, which happens when D is true, which happens when all clauses are true, which happens when the formula is satisfiable.

Reduction (Inequivalence of Programs With Arrays): The same program works, we just need to replace our assignment if operations.  We do this by placing all of the elements of what we are comparing into an array, and replacing the statement “E <- if A=B then C else D” with:

α.A <- D
α.B <- C
E <- α.A

..if A and B are the same, then we will fill that spot in the array with D then C, and get a C out.  Otherwise, the two assignments go to different locations, and E is set to what is in the array at position A, which is the value D.  Since we can go back to the previous reduction and replace all of its statements with 3 statements under the new rules, the reduction works in the same way.

Difficulty: 6.  This isn’t a hard reduction to do, I think the hardest thing is to get students to think in terms 0f the restrictions these programs require.  There are no loops or anything (that would make this problem undecidable, at least in general), and representing variables as positions in an array is something we might be used to doing if all variables are integers, but since variables here are things like “B2” some work might need to be done to convince students that the mapping to integers for all variables is reasonable.  It’s not a thing we do as much with modern high-level languages as we might have done in the 1970s when the underlying machine was much more exposed.

Code Generation With Unfixed Variable Locations

Sorry for the long break.  I’m hoping to use this summer to get most of the rest of the way through this book.

The Problem: Code Generation With Unfixed Variable Locations.  This is problem PO8 in the appendix.

The Description: Given a program (a sequence of instructions I1..In), a set V of variables, a “short address span” B, and a desired program size M.  We want to assign addresses to both the instructions of the program and the variables.  If an instruction accesses a variable that is within B instructions of its use, we can represent that instruction in one byte (using the “short address”).  Otherwise, the instruction is represented in two bytes (using the “long address”).  Can we place all instructions and variables in M addresses or less?

Example: Suppose I have the following instructions (A, B, and C are variables, “ref” just means the instruction refers to that variable)

ref A
ref A
ref B
ref C

If B=1 (so all short references have to be within one instruction of the variable address), we can place all instructions and variables in 7 addresses, for example:

ref A
A
ref A
ref B
B
C
ref C

If instead that second A reference was at the end of the sequence of instructions:

ref A
ref B
ref C
ref A

..then (because we can’t change the order of the instructions in the program), we would have to make one of the references to A long, for example:

ref A
A
ref B 
B
C
ref C
ref A (long)

That second instruction that references A is a long reference, so this program needs 8 bytes of address space.

Reduction: The paper by Robertson uses 3SAT, So let’s start with a 3SAT instance with n variables and m clauses, each clause Cj contains literals Aj1, Aj2, and Aj3.Having just 1 or 2 literals in a clause is ok too.

Robertson notes that for any two literals V and W, if you have V and ~W appear as one (complete, two-element) clause, and also have ~V and W appear as a different clause, then V and W must both have the same truth value in order to satisfy both clauses.  This gets us a way to add more variables to the formula that have truth values the same as some other variable.  Specifically, if some variable V shows up in our formula more than 5 times, we can create a new variable W to replace three of those occurrences of V, and add two clauses to the end (the clauses (V ∨ ~W) and (~V ∨ W)).  This forces our new W to have the same truth value V will have if the formula is satisfied, and reduces the number of occurrences of V.  We repeat this process until no variable appears more than 5 times in the formula.  So, now we can say that for some variable Vi, it appears in clauses Ci1 through Ci5 (or maybe less than 5 if the variable occurs less than 5 times).

The program we will build will consist of “modules” that can be moved independently.  Each variable will have two modules (“t” and “f” modules), and each clause will have one.  Here is a picture of a variable “t” module:

“l” is the paper’s version of B- the maximum distance we can put a short reference to a variable.

What we’re seeing here is:

  • A “slot” we can put a variable (or more than one) into
  • 16 instructions that refer to a new variable ui
  • 3 instructions that reference each of the variables corresponding to the (at most 5) literals and clauses the variable can appear in.

The “f” mode is similar except that the definition of τr is negated (it’s the positive variable if ~Vi occurs as a literal).  The new variable ui appears in the t and f modules for variable i and noplace else, so the only way references to it can be short is if it is placed into the “slot” in either the “t” module (meaning variable i is set to true) or the “f” module (meaning variable i is set to false).  If we put ui in the slot of (say) the “f” module, then we have enough room to also place the variables corresponding to the literals in the same block making everything short.  But by putting the ui variable in the “f” module, all of the references to it from the “t” module will be long (adding 16 extra bytes of address space), making all of the literals too far away from the slot for the slot to be useful in that module.

We also have a module for the clause (the “c”-module):

Notice that the versions of the literals that actually appear in the clause are to the right of the slot.  These α variables are the same ones we had in the variable modules (so each α variable shows up once in a “c” module, but 3 times each in a “t” or “f” module).  Since there are more references to the α variables in our variable modules, the optimal placement should be to place those variables in the slot of the “t” or “f” modules (not in the “c” module).  The “remaining” α variables (the negations of the ones we put into the slot in either the “t” or “f” modules and which it didn’t help us to put in the slot of the other module) can go into the slot here and make one of the corresponding β references short.

We do have that extra γj cell to play around with, and here is where either the paper has a mistake, or I lose the ability to follow.  What is supposed to happen is that if we fill the slot with a variable that is referred to by one of the β variables then that reference will be short, and the reference from γ to δ will be within the range of a short reference.  That’s fine, but the paper wants this to be the α variable that we did not place in the “t” or “f” module.  But if placing the α in the “t” module meant setting the variable to true, then what is not in the module is the negation of that module, which feels like we are doing things backward- like we want to set the variable to true, we should have put ui in the “f” module so that the literal that can be placed in our clause module corresponds to the true version of the literal.

I’m not sure it matters much to the reduction.  If I’m right, it just means we should have labeled the α variables the negations of what they really are.  But it does worry me.

The proof finishes with deciding values of B and M to make it all work.  B ends up being 31 (it comes from the distance we need to separate the 16 ui instructions from the τ instructions), and M ends up being 16n+4* the total number of literals in the formula.

Difficulty: 7.  This has a lot of pieces, but (except for that end part) I think it’s pretty feasible to see how all of the pieces fit together.

 

 

Protected: Code Generation on a One-Register Machine

This content is password protected. To view it please enter your password below:

Protected: Tree Transducer Language Membership

This content is password protected. To view it please enter your password below:

Protected: ETOL Language Membership

This content is password protected. To view it please enter your password below:

Protected: Regular Expression Inequivalence on Single Character Alphabets

This content is password protected. To view it please enter your password below:

Protected: Minimum Inferred Regular Expression

This content is password protected. To view it please enter your password below:

Protected: First Order Subsumption

This content is password protected. To view it please enter your password below:

Protected: Predicate Logic Without Negation

This content is password protected. To view it please enter your password below: