Non-deterministic Ada Programs

A program can alter one `bit' of memory at a time.

The current bit is indexed by an integer value: at_cell

The next bit is always adjacent to the previous one.

The program is in one of a finite number, s say, of states.

The next state entered is chosen non-deterministically from a choice of two.

A complete program is specified when the action for each state and bit value is defined.

State s is the unique accept state.

procedure nd_ada_f (T:integer) is
  type workspace is array (integer range <>) of 01B;
  n : integer;
      w : workspace( -T..T ):=(others=>B);
      procedure do_it_on ( w : in out workspace;
                          position : in out integer;
                          state : in out integer);
          case state is
            when k =>
              if w(position)=B then
                w(position):=(0 or 1)k; position:=position (+-1)k;
                state:=choose(next1, next2)k;
              elsif w(position)=0 then
                w(position):=(0 or 1)k; position:=position (+-1)k;
                state:=choose(next1, next2)k;
                w(position):=(0 or 1)k; position:=position (+-1)k;
                state:=choose(next1, next2)k;
              end if;
          end case;
       end do_it_on;
        at_cell:=1; in_state:=1; get(w(1..n));
        for i in 1.. T loop
        end loop;
        if in_state=accept then return true; end if;
  end nd_ada_f;

The decision problem NCOMP is:

Input: A non-deterministic program, AP;

An input x in <0,1>n for AP;

A time bound T.

Question: Is there a `computation path' of AP on x that accepts in T iterations?

Computation Tree

An Alternative to NP

ADA_NP is the class of decision problems, f, for which there are:

that satisfy:

Theorem: ADA_NP=NP


a) ADA_NP is a subset of NP.

Suppose that f is in ADA_NP.

Let NAf and p(n) be the program and polynomial such that for all x in {0,1}n:

f(x)=1 if and only if NCOMP(NAf, x, p(n))=1

A set of witnesses to f(x)=1 is the set of computation paths NACP, for NAf.

Checkf(CP,x)=1 if CP is a valid accept computation for NAf on input x.

Given NAf, CP and x this can be checked by simulating NAf on x using the computation path CP.

This test can be done in polynomial-time, so Checkf is in P, i.e. f is in NP.

b) NP is a subset of ADA_NP

Let f is in NP, so that Checkf is in P.

Let Wn be the witness set for x in {0,1}n.

For any w in Wn it must hold that |w|<= p(n) for some polynomial p(n).

(otherwise Checkf(x,w) could not be carried out in P).

Let Wn be encoded in binary. Then

For all x in {0,1}n there are at most 2p(n) `witnesses to f(x)=1'.

NAf is the program which:

NCOMP(NAf,x,p(n)+q(n))=1 if and only if NAf has a path of length p(n)+q(n) ending in accept on input x.

iff NAf constructs a witness w for x after p(n) moves which checks correctly in q(n) steps

iff Checkf is in P.

In summary, Checkf in P implies that f is in ADA_NP.

Hence (from (a) and (b)), ADA_NP=NP.

The Satisfiability Problem (SAT) is:

Input: A set of n Boolean variables Xn=<^x1,x2,...,xn>; A Boolean formula F over Xn, (whose length is at most r(n) for some polynomial r)

Question: Is there an assignment, a of true/false to the variables Xn with the property that F(a)=true?

Cook's Theorem

SAT is NP-complete.

Proof: We have to do 2 things:

i.e. Any instance x of f can be transformed into an instance F(x) of SAT such that f(x)=1 iff SAT (F(x))=1.

That (a) holds has already been shown.

Now let f be any decision problem in NP.

We know that f also belongs to ADA_NP (since NP=ADA_NP).

So there is a non-deterministic Ada program NAf for f and a polynomial p(n) such that, for any x in {0,1}n, f(x)=1 iff NCOMP( NAf,x,p(n))=1

To show that SAT is NP-complete, we build an instance of SAT (i.e. a Boolean formula), H (NAf) (Xm(n)) with the property

H(NAf)(Xm(n)) is satisfiable



What do we know about NAf on input x in {0,1}n?

At any value i of its main for loop its status is fully described by

A1) The value of in_state.

A2) The value of at_cell.

A3) The content (0, 1, or B) of each `bit' w(k).

These can change only in accordance with what the procedure do_it_on allows, given the initial n-bit input x.

So, suppose we wish to know if a given sequence of p(n) configurations (i.e. state, position, memory) is a valid accepting computation path on NAf.

Then such a sequence must embody all of the following characteristics at all times i:

C1) At time i=0: in_state=1, w(1..n)=x, all other bits equal B; at_cell=1.

C2) in_state has exactly one value at time i.

C3) at_cell has exactly one value at time i.

C4) w(k) has exactly one value at time i, (for all k)

C5) in_state=s (accept state) at i=p(n).

C6) w(-p(n)...p(n)), at_cell, and in_state must change from time i to time i+1 according to the case statement in do_it_on of NAf.

We construct H(NAf) with the Boolean variables: (below 0 <= i <= p(n))

V1) 3(2p(n)+1)(p(n)+1) variables

W(v,k,i) with v in {0,1,B}, -p(n) <= k <= p(n)

V2) s(p(n)+1) variables

S(st,i) 1 <= st <= s,

V3) (2p(n)+1)(p(n)+1) variables

A(k,i) -p(n) <= k <= p(n)

H(NAf(x)) is built so that: in a satisfying assignment those variables which which are assigned the value true define a valid computation, CP of NAf on x:

V1T) W(v,k,i)=1 iff in CP: at time i, `bit' w(k) contains v.

V2T) S(st,i)=1 iff in CP: at time i, in_state=st.

V3T) A(k,i)=1 iff in CP: at time i, at_cell=k.

Thus the whose only satisfying assignments of H(NAf)(V1,V2,V3) will be as given by (V1T, V2T, V3T) and define legal computations of NAf on x, i.e. capture the conditions (C1) through (C6)

(Below & denotes logical and; + denotes logical or. For brevity we assume and is implied).


S(1,0)A(1,0) &k=1n W( xi,k,0) & &k=-p(n)0 W(B,k,0) &k=n+1p(n) W(B,k,0)

C2) `exactly one value' == `at least one value' and at most one value.

&i=0p(n)( +st=1s S(st,i) ) & &1<=c< d<=s (-S(c,i) + -S(d,i))

C3) Similarly,

&i=0p(n) ( +k=-p(n)p(n) A(k, i) ) & &-p(n) <=c< d<=p(n) ( -A(c,i) + -A(d,i) )

C4) Again, similarly,

&i=0p(n) &k=-p(n)p(n) ( +{v in {0,1,B } W(v,k,i) ) &v1=v2 ( -W( v1,k,i) + -W( v2,k,i) )

C5) S(s,p(n))

C6) is, superficially, more complicated, however at time i: from

in_state=st, at_cell=k, w(k) is one of {0,1,B}

the case statement determines the values at time i+1 of

the new value of at_cell

the content of w(k),

the two possible next states to jump to.

Thus each of the s states is described by a `move' function:

delta (st,v) = ( ( st1 , st2 ), nv, ch )

where v is in {0,1,B}, nv is in {0,1}, ch=(+or-)1

We thus have (C6) as

&i=1p(n)-1 &j=-p(n)p(n) &{delta (st,v)} MOVE(i,j,st,v, st1 , st2,nv,ch)

where MOVE(i,j,st,v, st1, st2, nv , ch) is,

S(st,i)& A(j,i)& W(v,j,i) -> ( S( st1,i+1) & A(j+ch,i+1) & W(nv,j,i+1) + S( st2,i+1) & A(j+ch,i+1) & W(nv,j,i+1) )


If at time i

NAf is in_state st

at_cell j which contains v then

at time i+1,

NAf is in_state st1 or st2

at_cell j+ch with cell j containing nv.

So the final formula H(NAf) (V1,V2,V3) is

C1 & C2 & C3 & C4 & C5 & C6 ( V1,V2,V3 )

H(NAf)(V1,V2,V3) is satisfiable


NCOMP (NAf,x,p(n))=1.

If NCOMP( NAf,x, p(n))=1 setting the variables of V1, V2, V3 that encode the accepting computation path of NAf gives a satisfying assignment of H;

H guarantees that the true variables of any satisfying assignment must represent a valid computation of NAf on input x that ends in accept after p(n) steps. i.e. a witness that NCOMP ( NAf, x, p(n) )=1