lis_cp(S, Res,Z) =>
  Len = S.len,
  X = new_list(Len),
  X :: 0..1,

  increasing_except_0($[X[I]*S[I] : I in 1..Len]),
  Z #= sum(X),

  solve($[max(Z)],X),
  % Extract the found LIS
  Res = [S[I] : I in 1..Len, X[I] == 1].

%
% Ensures that array A is (strictly) increasing if we disregard any 0's
%
increasing_except_0(A) =>
  N = A.len,
  foreach(I in 1..N, J in I+1..N)
    (A[I] #!= 0 #/\ A[J] #!= 0) #=> (A[I] #< A[J])
  end.