Orchestrated Constraint Solving¶

When trying to find solutions to complicated constraint systems, it is sometimes useful to explicitly break the problem into multiple states that can be solved in sequence. The main advantage of this approach, as opposed to solving the whole constraint system in one go, is that it allows the human operator to inject their domain knowledge about the problem being solved. The way that the program is broken apart, and the way that the various pieces are recombined, can have an enormous effect on how long it takes to solve a constraint system, and if it is feasible to solve at all.

Grackle is well suited to this style of “orchestrated” constraint solving. By giving the operator a convenient programmable front end to a variety of different solvers, it is relatively easy to experiment with different search strategies and different underlying solvers to find an effective decomposition strategy.

String Packing¶

To illustrate the basic idea of orchestrated solving, we introduce a constructed example problem. This problem involves finding inputs to a simple filtering process (sliding window average) that produces output containing certain sequences of values which have been chosen in advance, subject to some other constraints. The twist to this problem that makes it nontrivial is that we don’t care where in the output these sequences occur; just that they do occur.

To make this problem more concrete, suppose we have an input buffer consisting of 1000 integer values; the input values are constrained to fall between -300 and 300. We choose in advance 9 short strings of ASCII values (see the code excerpt below) as our target strings. We compute a sliding window average over the input buffer with a window width of 5; it is in this output buffer that we expect to find our target strings (as sequences of numbers corresponding to the ASCII values of the characters). Finally, we compute a second sliding window average with a window size of 35, and we constrain the output of this second sliding average to be between -1 and 1. This final constraint has the effect of causing the input buffer to be centered roughly near 0.

A solution to this problem consists of a vector of 9 location values (corresponding to the target strings) such that the output of the narrow sliding window average contains the target strings at those locations.

Naive Packing¶

The Grackle code below sets up this constraint problem and submits it all at once to the default solver (Yices).

% Parameters to the problem
len        = 1000; % how long is the input stream
width      =    5; % how wide is the narrow sliding avg. window
extra      =   30; % how much wider is the wide sliding avg. window
limit      =    1; % what is the limit for the wide sliding average?
inputlimit =  300; % maximum distance from 0 an input value can be
minsep     =    1; % minimum amount of separation between strings

% the strings we want to pack
segments  = { 'hello!asdf' ...
            , 'whatup'  ...
            , 'yall' ...
            , 'howdy', 'pardner' ...
            , 'WHATDO', 'YOUWANT' ...
            , 'howareyou' ...
            , 'my man'
            };
numsegs   = size(segments, 2);

% The symbolic input vector we are searching for
input     = symbolic_array('input', 1, len, 'integer');

% The vector of locations at which we place the strings
locs      = symbolic('locs', 1, numsegs+1, 'integer');

% symbolically calculate the narrow sliding window avg.
y = slide( input, width, 1 );
y_len = size(y, 2);

% symbolically calculate the wide sliding window avg.
z = slide( input, width+extra, 1 );

% constrain the strings away from the boundaries
locs_ok = locs(1) >= 50 & locs(numsegs) <= y_len - 50;

% constrain the string locations to nonoverlapping regions
% of the output buffer
for i = 1:numsegs
    % every location is in range
    locs_ok = locs_ok & minsep <= locs(i) & ...
              locs(i) + size(segments{i},2) + minsep < y_len;

    for j = 1:numsegs
        if i < j
            ij_disjoint = locs(i) + size(segments{i},2) + minsep <= locs(j);
            locs_ok = locs_ok & ij_disjoint;
        end
    end
end

% assert that the target strings appear in the output buffer
p = locs_ok;
for j = 1:numsegs
    segsize = size(segments{j}, 2);
    for k = 1:segsize
        p = p & (y(locs(j) + k - 1) == segments{j}(k));
    end
end

% Here we bound the size of the larger sliding average:
% this has the general effect of forcing the input
% vector to be roughly centered around 0.
p = p & all ( z <= limit ) & all ( z >= -limit );

% We also directly bound the magnitude of the input values
p = p & all ( input <= inputlimit ) & all (input >= -inputlimit );

% Search for a solution!
[c r] = check_sat( p )

% Print the results of the narrow sliding average
q = slide( r.input, width, 1 )

% Print the results of the wide sliding average
w = slide( r.input, width+extra, 1 )

% Print the segments of the output where we expect to find
% the desired strings packed
for i = 1:numsegs
  q( locs(i) : (locs(i)+size(segments{i},2)) )
end

Unfortunately, standard SMT solving techniques will do very poorly on this problem. The linear arithmetic constraint solving gets intermixed with choosing the packing locations in a way that seems to make very little progress. In our experiments, running this all-at-once query for hours yielded no solution. Our hypothesis is that the SMT solver is essentially performing a totally undirected search through the space of possible packing locations, and getting lost in the weeds.

Greedy Packing¶

Instead, we can rely on our domain knowledge about this problem, which indicates that the subproblem involving just the linear arithmetic constraints should be easy for the solver, once the input positions are fixed. Thus, we can approach this problem as a two-phase search: first search for locations at which to pack the target strings, then search for inputs yielding those target strings. Moreover, with a little thinking about the problem, we can conjecture that it is easier to pack strings into the buffer if they are further apart. This is reasonable because the main constraints on this system are local in nature (sliding window averages), and putting more “buffer space” between target string locations should allow more slack in the constraint system, making it easier to solve.

By relying on these insights into the structure of the problem, we are led to try an “incrementally greedy” packing strategy. We start by packing a single string at the first location we can find. Next we try to pack the second string, as close to the first as we can. If we discover our current location yields an unsatisfiable constraint system, we move the current target location deeper into the input buffer, and thus further from other target strings. Once we find a location where the current string can be packed, we move on to the next one. Either we end up in a situation where all the strings have locations, or we run out of room in the buffer. If we run out of room (or hit a predetermined limit), we backtrack and start adding more space between earlier strings.

The nice thing about this strategy is that is requires very little computation to explore the space of packing positions; moreover, the subproblems generated once the locations are fixed are easy to solve. This leads to submitting a large number of problem instances to the solver, each of which is easy.

It turns out that the incrementally greedy search strategy is shockingly effective for this problem. With naive settings for the search parameters, we can find a solution in about 2 minutes. With a little tuning to the search parameters (e.g. minsep = 70 and seachinc = 5) to make the search more aggressive about adding space between strings, we can find solutions in as little as 20 seconds.

The following Grackle code implements the incremental greedy search strategy.

% Parameters to the problem
len        = 1000; % how long is the input stream
width      =    5; % how wide is the narrow sliding avg. window
extra      =   30; % how much wider is the wide sliding avg. window
maxsearch  =   50; % how far forward to search for a location before resetting
limit      =    1; % what is the limit for the wide sliding average?
inputlimit =  300; % maximum distance from 0 an input value can be
minsep     =    1; % minimum amount of separation between strings
searchinc  =    1; % how many spaces to skip when we search foraward

% the strings we want to pack
segments  = { 'hello!asdf' ...
            , 'whatup'  ...
            , 'yall' ...
            , 'howdy', 'pardner' ...
            , 'WHATDO', 'YOUWANT' ...
            , 'howareyou' ...
            , 'my man'
            };
numsegs   = size(segments, 2);

% The symbolic input vector we are searching for
input     = symbolic('input', 1, len, 'integer');

% The vector of locations at which we place the strings
locs      = zeros(1, numsegs+1);

% symbolically calculate the narrow sliding window avg.
y = slide( input, width, 1 );

% symbolically calculate the wide sliding window avg.
z = slide( input, width+extra, 1 );


%% Now begin the location search algorithm

%  1) The outer loop gradually increases the 'minsep' value which
%     determines the minimum amount of separation between packed
%     strings.  It continues until eventually we find a solution.
c = false;
while ( not(c) )
    minsep = minsep + searchinc;

    % 2) The next loop tries to pack each string in turn
    for i = 1:numsegs
        if( i > 1 )
            start = locs(i-1) + minsep + size(segments{i-1},2);
        else
            start = minsep;
        end

        %  3) The third loop starts 'minsep' locations from the end of the
        %     previous string, trying successive locations up to
        %     'maxsearch' away
        offset = start;
        while offset <= start+maxsearch
            locs(i) = offset;
            locs(i+1) = offset + minsep + size(segments{i},2);
            offset = offset + searchinc;

            % display the current location vector
            locs

            % 4) Here we build the assertion that all the strings
            %    up to string i appear in the output
            p = true;
            for j = 1:i
                segsize = size(segments{j}, 2);
                for k = 1:segsize
                    p = p & (y(locs(j) + k - 1) == segments{j}(k));
                end
            end

            % Here we bound the size of the larger sliding average:
            % this has the general effect of forcing the input
            % vector to be roughly centered around 0.
            p = p & all ( z <= limit ) & all ( z >= -limit );

            % We also directly bound the magnitude of the input values
            p = p & all ( input <= inputlimit ) & all (input >= -inputlimit );

            % Try to find a solution
            [c r] = check_sat( p )

            % If we succeed at this step, break out of loop 3 and
            % go on to try the next string.
            if( c )
                break;
            end
        end

        % If we ended the previous loop without a success, we
        % failed to pack the ith string.  Break out of loop 2
        % and start over with an increased 'maxsep'
        if( not(c) )
            break;
        end
    end
end

% Print the results of the narrow sliding average
q = slide( r.input, width, 1 )

% Print the results of the wide sliding average
w = slide( r.input, width+extra, 1 )

% Print the segments of the output where we expect to find
% the desired strings packed
for i = 1:numsegs
  q( locs(i) : (locs(i)+size(segments{i},2)) )
end

Sliding window function¶

For the sake of completeness, the functions used for computing sliding window averages is included below.

% Compute sliding average
% 'width' is the size of the window
% 'shift' is how much to shift the window
% shift must be less than width (ie windows overlap)
function y = slide(x,width,shift)
  nx = size(x,2);
  ny = ceil ((nx-width+1)/shift);
  y = zeros(1,ny);

  i = 1;
  for j = 1:ny
    seg = x(i:(i+width-1));
    y(j) = sum(seg) / width;
    i = i + shift;
  end
end