Multiset Partition Using Linear Arithmetic and Z3

Question

I have to partition a multiset into two sets who sums are equal. For example, given the multiset:

1 3 5 1 3 -1 2 0

I would output the two sets:

1) 1 3 3
2) 5 -1 2 1 0

both of which sum to 7.

I need to do this using Z3 (smt2 input format) and "Linear Arithmetic Logic", which is defined as:

formula : formula /\ formula | (formula) | atom
   atom : sum op sum
     op : = | <= | <
    sum : term | sum + term
   term : identifier | constant | constant identifier

I honestly don't know where to begin with this and any advice at all would be appreciated.

Regards.

Answer 1

Here is an idea:

1- Create a 0-1 integer variable c_i for each element. The idea is c_i is zero if element is in the first set, and 1 if it is in the second set. You can accomplish that by saying that 0 <= c_i and c_i <= 1.

2- The sum of the elements in the first set can be written as 1*(1 - c_1) + 3*(1 - c_2) + ... +

3- The sum of the elements in the second set can be written as 1*c1 + 3*c2 + ...

Answer 2

While SMT-Lib2 is quite expressive, it's not the easiest language to program in. Unless you have a hard requirement that you have to code directly in SMTLib2, I'd recommend looking into other languages that have higher-level bindings to SMT solvers. For instance, both Haskell and Scala have libraries that allow you to script SMT solvers at a much higher level. Here's how to solve your problem using the Haskell, for instance: https://gist.github.com/1701881.

The idea is that these libraries allow you to code at a much higher level, and then perform the necessary translation and querying of the SMT solver for you behind the scenes. (If you really need to get your hands onto the SMTLib encoding of your problem, you can use these libraries as well, as they typically come with the necessary API to dump the SMTLib they generate before querying the solver.)

While these libraries may not offer everything that Z3 gives you access to via SMTLib, they are much easier to use for most practical problems of interest.