title: Multiset Partition Using Linear Arithmetic and Z3
body: <p>I have to partition a multiset into two sets who sums are equal.  For example, given the multiset:</p>
  
  <pre><code>1 3 5 1 3 -1 2 0
  </code></pre>
  
  <p>I would output the two sets:</p>
  
  <pre><code>1) 1 3 3
  2) 5 -1 2 1 0
  </code></pre>
  
  <p>both of which sum to 7.</p>
  
  <p>I need to do this using Z3 (smt2 input format) and "Linear Arithmetic Logic", which is defined as:</p>
  
  <pre><code>formula : formula /\ formula | (formula) | atom
     atom : sum op sum
       op : = | &lt;= | &lt;
      sum : term | sum + term
     term : identifier | constant | constant identifier
  </code></pre>
  
  <p>I honestly don't know where to begin with this and any advice at all would be appreciated.</p>
  
  <p>Regards.</p>