title: Constraint against a median
body: <p>I'm trying to solve a satisfiabilty problem over integers using z3py where one of my constraints requires that the value of each variable in an array be greater than the median of the last eleven variables.  Right now, I'm encoding the constraint like:</p>
  
  <blockquote>
    <p>PbLe( ((v[i] &lt;= v[i-11],1),...(v[i] &lt;= v[i-1],1)), 6) </p>
  </blockquote>
  
  <p>And this seems to be causing the solver to use a tremendous amount of memory. I assume the PbLe is getting converted to disjunctive normal form on the backend or something similar and causing a large blowup in the size of the expression.</p>
  
  <p>Is there a more efficient way to express a 'greater than a rolling median' for values in an array in z3?</p>