Using z3 to try to solve Feedback Arc Set for Tournaments

I’ve been meaning to check out Z3 for a while - it’s an open source theorem prover from Microsoft with great looking Python bindings. I’m partly interested just out of pure curiousity, partly because there are some interesting potential applications for Hypothesis (it’s currently unclear to me how possible those are - the architecture of Hypothesis is not well set up for concolic testing, nor are the semantics of Python, but still).

Anyway, I thought I’d turn it loose on my favourite evil problem, feedback arc set for tournaments. It’s at that weird boundary where what you want is sortof a SAT solver and sortof an integer linear programming solver. There’s some suggestion that using hybrid approaches would be better than either, but I haven’t really found any easily usable hybrid solvers (there’s a fork of minisat that might work. It’s on my TODO list)

Anyway, basically what we do with z3 is that we create the initial problem, ask it for a feasible solution, then successively ask it to improve on that feasible solution until it no longer can. Here’s the code:

import z3
from itertools import permutations
from functools import total_ordering


@total_ordering
class ModelKey(object):
    def __init__(self, model, variables, i):
        self.model = model
        self.variables = variables
        self.i = i

def eq(self, other): return isinstance(other, ModelKey) and other.i == self.i

def lt(self, other): if other.i == self.i: return False elif self.i < other.i: return self.model[self.variables[self.i, other.i]].as_long() > 0 else: return self.model[self.variables[other.i, self.i]].as_long() == 0

MAX_PROBLEM_SIZE = 500


def feedback_arc_set(problem):
    problem = [
        v for v in problem if v[0] != v[1]
    ]
    if not problem:
        return []
    n = 0
    forward_total = 0
    backward_total = 0
    for i, j, w in problem:
        if min(i, j) < 0:
            raise ValueError("Invalid index %d < 0" % (min(i, j),))
        if max(i, j) > MAX_PROBLEM_SIZE:
            raise ValueError("Invalid index %d > %d" % (
                max(i, j), MAX_PROBLEM_SIZE))
        n = max(n, i, j)
        if i < j:
            forward_total += w
        elif j < i:
            backward_total += w
    n += 1

solver = z3.Solver()

variables = {} for i in range(n): for j in range(i + 1, n): v = z3.Int(‘x_%d_%d’ % (i, j)) variables[i, j] = v variables[j, i] = 1 - v solver.add(v >= 0) solver.add(v <= 1)

for i, j, k in permutations(range(n), 3): solver.add( variables[i, j] + variables[j, k] + variables[k, i] <= 2 ) score = z3.Int(‘score’)

solver.add(score == sum( variables[j, i] * w for i, j, w in problem ))

There is definitely an ordering with score <= best_score.

We successively try to improve it until we no longer can.

best_score = min(forward_total, backward_total) while True: print(“Current best: %d” % (best_score,)) solver.push() solver.add(score < best_score) if solver.check() == z3.unsat: solver.pop() break else: best_score = solver.model()[score].as_long()

solver.add(score <= best_score) result = solver.check() assert result == z3.sat, solver model = solver.model() result = list(range(n)) result.sort(key=lambda i: ModelKey(model, variables, i))

return best_score, result

The good: z3 was extremely easy to use. The API was pleasant, reasonably intuitive, and basically did what I expected.

The bad: This solution is strictly worse than a solution which just generates a massive LP file and hands it off to lp_solve. So although it was very easy to solve this problem with z3, z3 appears not to be well suited to it. Z3 struggled at n = 15 and seemed to get stuck at n = 20.

This shouldn’t necessarily be considered indicative that Z3 is “bad”. This is a problem with a lot of constraints (O(n^3)), so it’s probably not representative of the sort of things Z3 is good at, and it is representative of the sort of things that lp_solve is good at. So I’m not really deriving any lessons from the fact that Z3 wasn’t very good at this problem . I’m more interested in the fact that it was super easy to use, so I really should look at using it more in future.