Wiki

Clone wiki

sketch-frontend / DutchFlag

We illustrate how to solve Dijkstra's Dutch Flag challenge problem using Sketch to test hypotheses rather than in the traditional way.

Problem Statement

The famous Dutch national flag problem comes from Chapter 14\ref{DijkstraBook}. There is a row of buckets numbered 1 to N where each bucket contains one pebble and each pebble is either red, white or blue. The problems asks for a program to rearrange (if necessary) the pebbles in the order of the Dutch national flag, i.e. in the order of first the red pebbles, then the white, and finally the blue pebbles. The operations allowed in the program are :

swap(i,j): exchanges the pebbles in bucket numbered i and j.

observe(i) : returns the color of the pebble in bucket numbered i

The program needs to some special requirements. Firstly it should be able to cope up with all possible 3^N pebbles configuration in N>=0 buckets. Secondly only a fixed number of variables of type integer are allowed to be used. And finally only one observe(i) operation is allowed per pebble i. Furthermore, programs with fewer number of swap operations are preferred.

Simple version

We derive a solution program using three kinds of knowledge: facts, insights, and hypotheses. Facts are attributes of the program that are always true, insights are aspects of the program we assume to be true, and hypotheses are attributes of the program that we guess to be true. We rely on the synthesizer to help us determine whether our hypotheses are true; we can think of the sketching process as providing an oracle to help us walk over the hypothesis space.

First we can derive facts from the resource constraints of the problem. We are told that we have a fixed number of variables that can take on values ranging from 0 to N, so we can first declare those. We anticipate having a few variables to keep track of array indices, a loop condition variable, and a swap destination.

We'll also want to keep a count of the number of observe's we make in order to specify the resource constraint that we only examine each ball once. To adhere to the resource condition that we only buck each element once, we can keep a variable count of the number of times we buck, asserting that it is at most n when the program completes. If the synthesizer examines an algorithm that bucks some element twice, it can always construct a counterexample showing that algorithm is incorrect.

Since the resource constraints do not allows us to keep track of an unbounded number of previously seen colors, we can hypothesize that we use our fixed number of variable to keep track of pointers to buckets, and that we use these buckets to divide our bucket array into "zones." Since we have no prior knowledge about possible ball distribution, we may hypothesize that each of the variables should be initialized to being some offset of the beginning or end of the row of buckets. The array of buckets is symmetric, so we can arbitrarily decide to start examining on one end (by initializing our loop variable to 0).

int v0 = {| 0 | N |};
int v1 = {| 0 | N |};
int v2 = {| 0 | N |};
int v3 = {| 0 | N |};
int lv = 0;

int swap2;
int count = 0;

We can also hypothesize that we'll need a loop that helps us scan through the buckets until some condition is met. During the loop, we probably want to examine the "current" bucket:

while(lv < {| v0 | v1 | v2 | v3 |}) {
  int curbucket = observe(arr, lv, count);

  if (curbucket == 0) {
    /* Do something. */
  } else if (curbucket == 1) {
    /* Do something. */
  } else if (curbucket == 2) {
    /* Do something. */
  }
}

In each case, we probably want to optionally update some variables, optionally do a swap, and optionally update some more variables. We are using a hypothesis that we are only updating the variables by a fixed amount each loop iteration.

if (curbucket == 0) {
  v0 = {| v0 | v0 + 1 | v0 - 1|};
  v1 = {| v1 | v1 + 1 | v1 - 1|};
  v2 = {| v2 | v2 + 1 | v2 - 1|};
  v3 = {| v3 | v3 + 1 | v3 - 1|};

  swap2 = {| lv |v0 | v1 | v2 | v3 |};
  arr = swap(arr, lv, swap2);

  v0 = {| v0 | v0 + 1 | v0 - 1|};
  v1 = {| v1 | v1 + 1 | v1 - 1|};
  v2 = {| v2 | v2 + 1 | v2 - 1|};
  v3 = {| v3 | v3 + 1 | v3 - 1|};

  lv = lv + ??;
} 

Note that by not specifying the swap destination swap2, we are allowing the possibility of no swap.

To summarize, our sketch incorporates the following resource constraints directly from the problem statement:

  • Our operations are buck and swap.
  • We can call buck on each element at most once.
  • We use a fixed number of variables storing either integers ranging from 0 to n or color information.

Our sketch also incorporates the following programmer insights:

  • We are scanning across the buckets until we reach some condition. To do this, we use a loop increment variable lv which we are only moving in a fixed direction.
  • Whenever we examine each element, we want to do something different based on what color the element is.
  • Our fixed number of variables store pointers to buckets.

Our successful sketch incorporated the following hypotheses the involve moving balls between "zones:"

  • Besides the loop variable, we have three variables initialized to one of the ends of the array that moves a fixed amount each loop iteration.
  • During each loop iteration, we examine the "current" element: the element the loop variable currently points to.
  • During each loop iteration, we swap the current element with one of our other pointers.

Full code for sketch

We show our full sketch code below.

int N = 4;

int observe(int[N] arr, int i, ref int count) {
  ++count;
  return arr[i];
}

int[N] swap(int[N] arr, int i, int j) {
  int tmp = arr[i];
  arr[i] = arr[j];
  arr[j] = tmp;
  return arr;
}

void dutch_flag_fn(int[N] arr) implements dutch_flag {
  int v0 = {| 0 | N |};
  int v1 = {| 0 | N |};
  int v2 = {| 0 | N |};
  int v3 = {| 0 | N |};
  int lv = 0;

  int swap2;
  int count = 0;

  for (int i = 0; i < N; ++i) {
    if (arr[i] > 2) { arr[i] = 0; }
  }

  while(lv < {| v0 | v1 | v2 | v3 |}) {
    int curbucket = observe(arr, lv, count);
    if (curbucket == 0) {
      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      swap2 = {| lv |v0 | v1 | v2 | v3 |};
      arr = swap(arr, lv, swap2);

      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      lv = lv + ??;
    } else if (curbucket == 1) {
      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      swap2 = {| lv | v0 | v1 | v2 | v3|};
      arr = swap(arr, lv, swap2);

      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      lv = lv + ??;
    } else if (curbucket == 2) {
      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      swap2 = {| lv | v0 | v1 | v2 | v3|};
      arr = swap(arr, lv, swap2);

      v0 = {| v0 | v0 + 1 | v0 - 1|};
      v1 = {| v1 | v1 + 1 | v1 - 1|};
      v2 = {| v2 | v2 + 1 | v2 - 1|};
      v3 = {| v3 | v3 + 1 | v3 - 1|};

      lv = lv + ??;
    }
  }

  assert(count <= N);
  return;
}

Traditional sketch with reference implementation

The traditional sketch technique involves writing a sketch and a reference implementation. For our reference implementation we can simply implement a bubble sort, which yields the desired result but violates the resource constraints.

int[n] specA(int[N] input){
  int i,j,temp;

  for(i=0;i<N;i++){
    if(input[i]>=3)
      input[i]=0;
  }

  for(i=0;i<N;i++){
    for(j=i+1;j<N;j++){
      if(input[i]>input[j]){
        temp=input[j];
        input[j]=input[i];
        input[i]=temp;
      }
    }
  }

  return input;
}

Note that we'll have to change the return type of the sketch to be int[N] and return the array at the end.

Sketching using postconditions

Instead of providing a reference implementation, we can also assert a sortedness postcondition. This is sufficient: we do not need to state that the resulting array is a permutation of the original array because we only use the swap function for updates.

for(int i = 0; i < N - 1; ++i) {
  assert(arr[i+1]>=arr[i]);
}

This will yield analogous results to the case where we provided a reference implementation. We will declare an empty reference implementation as follows:

void dutch_flag(int[N] arr) {
  return;
}

Running

If we wanted to produce a sketch, a C++ output, and a C++ test file, we can run the following command:

sketch -fe-keep-asserts -fe-output-code -fe-output-test --bnd-inbits 2 workshop/dutch_flag.sk

The important flags here are -fe-keep-asserts, which makes sure the optimizations don't remove the asserts (in the version where we only sketch using post-conditions), and -bnd-inbits 2, which sets the bound on the input bits to 2.

Actual solution

Upon running the program, we can discover the actual solution.

Simplified simple solution code

The above sketch generate solution code can be simplified to get the following code. Lets have a bit closer inspection of the code. This interestingly conforms to the optimal algorithm.

The algorithm maintains two boundary variables v2 (for white boundary) and v3 (for blue boundary). The loop iterates until the loop variable lv becomes equal to the blue boundary v3. Inside the loop body, we have following three cases:

The currently inspected pebble is Red (0) : the red pebble is swapped with the pebble at the white boundary. In addition the white boundary and the loop variable are incremented.

The inspected pebble is White (1) : only the loop variable lv is incremented.

The inspected pebble is Blue (2) : firstly the blue boundary (v3) is decremented and then the blue pebble is swapped with the pebble on the blue boundary. Interestingly the loop variable is not incremented.

void dutch_flag_fn(int[N] arr)
{
  int v2=0; int v3=0; int lv=0;
  
  int count=0;

  v2 = 0;  /* white boundary */
  v3 = N;  /* blue boundary */
  lv = 0;
 
  while( lv < v3)
  {
    int curbucket = observe(arr, lv, count);
    if (curbucket == 0) /* red pebble */
    {
      arr = swap(arr, lv, v2);
      v2 = v2+1;
      lv = lv+1;
    }
    else
    {
      if(curbucket == 1) /* white pebble */
      {       
           lv = lv+1;
      }
      else
      {
        if(curbucket == 2) /* blue pebble */
        {
          v3 = v3-1;
          arr = swap(arr, lv, v3);
          lv = lv+0;
        }
      }
    }
  }
}

Unmodified solution code

void dutch_flag_fn([int[4] arr_0]) implements dutch_flag
{
  int[4] arr_1=arr_0;
  int v2_2=4;
  int v3_3=0;
  int lv_4=0;
  int count_5=0;
  for(int i_6=0;(i_6)<(4);i_6 = (i_6)+(1))
  {
    if((arr_1[i_6])>(2))/*dutch_flag.sk:30*/
    {
      arr_1[i_6] = 0;
    }
  }
  bit s_7=1;
  while(s_7)
  {
    int s_8=0;
    observe([arr_1, lv_4, count_5, s_8])
    if((s_8)==(0))/*dutch_flag.sk:35*/
    {
      v2_2 = (v2_2)+(1);
      v3_3 = v3_3;
      int[4] s_9=0;
      swap([arr_1, lv_4, v3_3, s_9])
      arr_1 = s_9;
      v2_2 = (v2_2)-(1);
      v3_3 = (v3_3)+(1);
      lv_4 = (lv_4)+(1);
    }
    else
    {
      if((s_8)==(1))/*dutch_flag.sk:50*/
      {
        v2_2 = (v2_2)-(1);
        v3_3 = v3_3;
        int[4] s_10=0;
        swap([arr_1, lv_4, v3_3, s_10])
        arr_1 = s_10;
        v2_2 = (v2_2)+(1);
        v3_3 = v3_3;
        lv_4 = (lv_4)+(1);
      }
      else
      {
        if((s_8)==(2))/*dutch_flag.sk:65*/
        {
          v2_2 = (v2_2)-(1);
          v3_3 = (v3_3)-(1);
          int[4] s_11=0;
          swap([arr_1, lv_4, v2_2, s_11])
          arr_1 = s_11;
          v2_2 = v2_2;
          v3_3 = (v3_3)+(1);
          lv_4 = (lv_4)+(0);
        }
      }
    }
    s_7 = (lv_4)<(v2_2);
  }
  assert ((count_5)<=(4));
  for(int i_12=0;(i_12)<(3);i_12 = (i_12)+(1))
  {
    assert ((arr_1[(i_12)+(1)])>=(arr_1[i_12]));
  }
}

Extension of Dutch Flag Problem

We can extend the previous Dutch Flag problem to the case when more than one pebbles can be observed at the same time. All the previous constraints still applies. Let us consider the case of looking at two pebbles at a time. The problem now becomes a lot more interesting as several optimizations can be performed based on observing two pebbles.

For example in the above algorithm, whenever we see a blue pebble we swap the pebble with the pebble at the blue boundary. If the second pebble at the blue boundary we can see that there is no need to swap the two pebbles as both are blue in color. We can simply move the blue boundary without performing the swap operation. Similar interesting cases occur when the second ball is observed to be red and white respectively.

To solve this problem using sketch we can essentially take our previous sketch and let the solver deal the special case of trying to synthesize the program to handle the case when the two pebbles are blue. We enumerate the three cases of seeing a blue pebble and a red, a white and a blue pebble respectively. In the case of seeing the second blue pebble we comment the swap call to see if the synthesizer can synthesize a program that can avoid the swap call.

#define SWAP_AND_ADJUST       v2 = {| v2 | v2 + 1 | v2 - 1|}; v3 = {| v3 | v3 + 1 | v3 - 1|}; swap2 = {| lv | v0 | v1 | v2 | v3|}; arr = swap(arr, lv, swap2); v2 = {| v2 | v2 + 1 | v2 - 1|}; v3 = {| v3 | v3 + 1 | v3 - 1|}; lv = lv + ??;


void dutch_flag_fn(int[N] arr) implements dutch_flag
{
  int v2=0; int v3=0; int lv=0;
  
  int count=0;

  v2 = 0;  /* white boundary */
  v3 = N;  /* blue boundary */
  lv = 0;
 
  while( lv < v3)
  {
    int curbucket = observe(arr, lv, count);
    if (curbucket == 0) /* red pebble */
    {
      arr = swap(arr, lv, v2);
      v2 = v2+1;
      lv = lv+1;
    }
    else
    {
      if(curbucket == 1) /* white pebble */
      {       
           lv = lv+1;
      }
      else
      {
        if(curbucket == 2) /* blue pebble */
        {
          secondball = v3 - 1;
          
          if(lv < {| v2 | v3 | secondball |}){ /*check at least two balls are left which can be observed */
            
             secbucket = observe(arr, secondball, count);
             
             if(secbucket == 0){
                  
                 SWAP_AND_ADJUST
                 SWAP_AND_ADJUST

             }
             else if(secbucket == 1){
      
                 SWAP_AND_ADJUST
                 SWAP_AND_ADJUST
             }
             else if(secbucket == 2){
                  v2 = {| v2 | v2 + 1 | v2 - 1|};
                  v3 = {| v3 | v3 + 1 | v3 - 1|};

                 // swap2 = {| lv | v0 | v1 | v2 | v3|};
                 // arr = swap(arr, lv, swap2); /* comment swap function to see if this can be avoided */

                 v2 = {| v2 | v2 + 1 | v2 - 1|};
                 v3 = {| v3 | v3 + 1 | v3 - 1|};

                 lv = lv + ??;

                 SWAP_AND_ADJUST
             } 
           
          }
          else{
               
                 SWAP_AND_ADJUST
          }
             
        }
      }
    }
  }
}

After running the solver, it indeed figures out that the swap call is not required in the case of two blue pebbles.

Updated