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;
  begin
    get(n);
    declare
      w : workspace( -T..T ):=(others=>B);
      procedure do_it_on ( w : in out workspace;
                          position : in out integer;
                          state : in out integer);
        begin
          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;
              else
                w(position):=(0 or 1)k; position:=position (+-1)k;
                state:=choose(next1, next2)k;
              end if;
          end case;
       end do_it_on;
      begin
        at_cell:=1; in_state:=1; get(w(1..n));
        for i in 1.. T loop
          do_it_on(w,at_cell,in_state);
        end loop;
        if in_state=accept then return true; end if;
      end;
  end nd_ada_f;

The decision problem NCOMP is:

Input: A non-deterministic program, AP;

An input x in <0,1>ⁿ 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:

• A non-deterministic Ada program, NA, and
• A polynomial p(n)

• For all x in {0,1}ⁿ such that f(x)=1, NCOMP( NA,x,p(n))=1

Theorem: ADA_NP=NP

Proof:

a) ADA_NP is a subset of NP.

Suppose that f is in ADA_NP.

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

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

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

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

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

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

b) NP is a subset of ADA_NP

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

Let W_n be the witness set for x in {0,1}ⁿ.

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

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

Let W_n be encoded in binary. Then

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

NA_f is the program which:

• In its first p(n) iterations generates each w in W_n on some computation path.
• In the next q(n) iterations runs the Check_f(x,w) algorithm (reaching accept iff Check_f(x,w)=1).

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

iff Check_f is in P.

In summary, Check_f 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 X_n=<^x₁,x₂,...,x_n>; A Boolean formula F over X_n, (whose length is at most r(n) for some polynomial r)

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

Cook's Theorem

SAT is NP-complete.

Proof: We have to do 2 things:

• Prove that SAT belongs to NP;
• Show that for any decision problem f in NP: f<=_pSAT:

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 NA_f for f and a polynomial p(n) such that, for any x in {0,1}ⁿ, f(x)=1 iff NCOMP( NA_f,x,p(n))=1

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

What do we know about NA_f on input x in {0,1}ⁿ?

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 NA_f.

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 NA_f.

We construct H(NA_f) 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(NA_f(x)) is built so that: in a satisfying assignment those variables which which are assigned the value true define a valid computation, CP of NA_f 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(NA_f)(V1,V2,V3) will be as given by (V1T, V2T, V3T) and define legal computations of NA_f on x, i.e. capture the conditions (C1) through (C6)

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

C1)

S(1,0)A(1,0) &_k=1ⁿ W( x_i,k,0) & &_k=-p(n)⁰ W(B,k,0) &_k=n+1^p(n) W(B,k,0)

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

&_i=0^p(n)( +_st=1^s S(st,i) ) & &_{1<=c< d<=s} (-S(c,i) + -S(d,i))

C3) Similarly,

&_i=0^p(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=0^p(n) &_k=-p(n)^p(n) ( +_{{v in {0,1,B }} W(v,k,i) ) &_v1=v2 ( -W( v₁,k,i) + -W( v₂,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) = ( ( st₁ , st₂ ), nv, ch )

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

We thus have (C6) as

&_i=1^p(n)-1 &_j=-p(n)^p(n) &_{{delta (st,v)}} MOVE(i,j,st,v, st₁ , st₂,nv,ch)

where MOVE(i,j,st,v, st₁, st₂, nv , ch) is,

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

Thus,

If at time i

NA_f is in_state st

at_cell j which contains v then

at time i+1,

NA_f is in_state st₁ or st₂

at_cell j+ch with cell j containing nv.

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

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

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

iff

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

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

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