Tag Archives: DNF Non-Tautology

I’d never heard of “Ianov schemes” before, but we’ll be using them for the next couple of problems, so let’s take a look!

The problem: Strong Inequivalence of Ianov Schemes.  This is problem PO16 of the appendix.

The description: Given two programs with a single variable x and instructions:

1. x = f(x) (where f is some function from some given set of functions F)
2. if p(x) goto I1 else goto I2 (p(x) is a boolean predicate from some given set of predicates P, I1 and I2 are instructions in the program)
3. Halt

Are the two programs not strongly equivalent: Can we find a function from F for each f, a predicate from P for each p, and an initial value for each variable that gives different final values for the variable in both programs?

Example: Here is one similar to what we will need in a minute:

P1:

1: if p(x) then 4 else 2
2: x =  f(x)
3: Halt
4: Halt

P2:

1: Halt

Suppose the only choice for f is f(x)= x+ 1(so, changing the variable).  Then the programs are different if we have a p(x) that will let us get to line 2 in P1.  If our only choice of p is something like “p(x) = true”, then the two programs are always equivalent.  If our set of P is (p(x) = true, p(x) = false), then we can choose a predicate that makes the programs inequivalent.

Reduction: The paper from Constable, Hunt, and Sahni basically does this in two parts.  G&J say to use 3SAT, but this looks to me like DNF Non-Tautology.

First (this is Proposition 2.11), they show how to take a DNF formula and turn it into a program.  The program works as a giant chain of if statements checking each literal in each clause.  If a literal is checked to be false, we move on to the next clause.  If all of the literals in a clause are true, we make it to the first (“+”) halting state.  If none of the clauses make it to the “+” state, we go to the second (“-“) halting state.  This means that the “-” state is only reachable if we do not start with a tautology.

Next (This is part iii of Corollary 2.14 of Theorem 2.13), they show that they can extend this into an Ianov scheme program by making the “+” state be just a halt command (so the variable never gets changed), and the “-” state be:

1: x= f(x)  (Where f is some function that changes x)
2: halt.

So the only way this program is different from the trivial “just halt” program is if we can reach the “-” instruction, which only happens if the formula is not a tautology.

Difficulty: 5. The program to test the non-tautology is not that hard.  As usual, the hardest part is parsing all of the definitions in the problem