SMT-for-IN3070/committees.org

SMT for IN3070

At the Department of Informatics (University of Oslo), all exams are corrected by a committee consisting of two examiners. For large courses, there are often many examiners where some wants to correct more than others. The administration is responsible for forming these committees. Sometimes there are additional constraints on what examiners can form a committee (the typical example being that two examiners are professors and two are master students).

Before digitizing exams at the department, the administration would have physical copies of the exam to distribute. This would actually make it easier to form the committees, because the constraints could be handled on the fly. When digitized, the problem would essentially turn into a math problem which is not particularly easy to solve.

This is an actual email (in Norwegian) forwarded to me from someone in the administration:

Mine mattekunnskaper er tydeligvis fraværende. Jeg klarer ikke finne en fornuftig løsning på dette:

A	160
B	150
C	110
D	60
E	60
F	30

Det er snakk om sensur i inf1300 med 283 besvarelser. D og E kan ikke rette mot hverandre. De bør helst rette mot B eller C.

Har du et bra forslag til meg? Jeg blir GAL. Det var bedre før, da jeg hadde besvarelsene fysisk å kunne telle ark.

Har du mulighet til å hjelpe en stakkar?

Takk

Being programmers who have recently heard of this thing called SMT-solving, we happily research the subject in trying to find a general solution to this cry for help.

Satisfiability modulo theories (SMT)

Satisfiability refers to solving satisfiability problems, i.e. given a first order logical formula $\phi$, decide whether or not there exists a model $\mathcal{M}$ such that $\mathcal{M} \models \phi$. In general, this is an undecidable problem. However, there are theories within first order logic that are decidable. SMT solvers can produce models that satisfy a set of formulas for many useful theories, some of which are satisfiable. It is natural to think of SMT as a generalization of SAT, which is satisfiability for propositional logic.

The solver we will be using is Z3.

Theories

Example of theories can be the theory of booleans (or propositional logic), integers or real numbers with equations and inequations, or other common programming concepts like arrays or bitvectors. Z3 supports solving constraint problems in such theories. More formally, we define theories as follows:

A theory is a set of first order logic formulas, closed under implication.

We can imagine how this might work. The natural numbers can, for instance, be expressed with the Peano axioms.

1. $\forall x \in \mathbb{N} \ (0 \neq S ( x ))$
2. $\forall x, y \in \mathbb{N} \ (S( x ) = S( y ) \Rightarrow x = y)$
3. $\forall x \in \mathbb{N} \ (x + 0 = x )$
4. $\forall x, y \in \mathbb{N} \ (x + S( y ) = S( x + y ))$
5. $\forall x \in \mathbb{N} \ (x \cdot 0 = 0)$
6. $\forall x, y \in \mathbb{N} \ (x \cdot S ( y ) = x \cdot y + x )$

In addition, one axiom is added to formalize induction. Because a theory is closed under implication, the theory consists of all true first-order propositions that follows from these axioms, which corresponds to the true propositions about natural numbers.

However, in Z3, we don't see such axioms; they just provide the formal justification for implementing special solvers for problem domains like natural numbers other commonly used theories. In Z3, we could write something like this:

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (< 0 a b c))

(assert (= (+ (* a a) (* b b)) (* c c)))

(check-sat)
(get-model)

This encodes two constraints

• $0 < a < b < c$
• $a^2 + b^2 = c^2$

where $a,b,c$ are whole numbers. Then we ask Z3 to produce a model $\mathcal{M}$ such that $\mathcal{M} \models (0 < a < b < c) \land (a^2 + b^2 = c^2)$, which outputs:

sat
(model
  (define-fun c () Int
    5)
  (define-fun b () Int
    4)
  (define-fun a () Int
    3)
)

The first line sat indicates that the formula is satisfiable, and produce a model where $a^\mathcal{M}=3$, $b^\mathcal{M}=4$ and $c^\mathcal{M}=5$.

Note that we would get a different answer if we declared the constant symbols as real numbers, because Z3 would use the theory for reals to satisfy the constraints.

Many-sorted first order logic

Z3 implements SMT-LIB, a standardized syntax and semantics for SMT solvers. It's underlying logic is a Many-sorted first order logic, where values must have an associated sort (which is a basic form of type). Think of it as partitioning the domain, where each sort corresponds to a part. A signature in a many-sorted first logic is defined as follows.

A signature $\Sigma = (S, F, P)$ consists of a countable set of

• Sorts $S$.
• Function symbols $F$, where each member is a function symbol $f$ with an associated type $s_1 \times \dots \times s_n \to s$, where $s \in S$ and $s_1, \dots, s_n \in S$. Constants are simply zero-arity function symbols.
• Predicate symbols $P$, where each predicate has an associated type $s_1 \times \dots \times s_n$. We assume an equality $=_s$ predicate with type $s \times s$ for all sorts in $S$.

The equality relation will be denoted $=$, letting the sort remain implicit.

For example, the signature for the integers can be formalized as $\Sigma_{int} = (S_{Int}, F_{Int}, P_{Int})$ where

• $S_{Int} = \{Int\}$
• $F_{Int} = \{0, 1, +, -, *\}$ where the constant symbols $0, 1$ has a type signature $\to Int$ and the function symbols $+,-,*$ has a type signature $Int \times Int \to Int$.
• $P_{Int} = \{<, =\}$ where the predicate symbols $<, =$ has type signature $Int \times Int$.

In Z3, the type signature of function- and predicate symbols informs Z3 of what theory it should apply.

Back to the problem

We have 283 exams. Every exam must be corrected by a committee consisting of two examiners. Each examiner has an associated capacity of exams they want to correct. Examiners D and E can't be in the same committee, and should rather be in committee with B or C. We prefer a smaller number of committees.

We use the Python API for Z3. Install with:

 pip install z3-solver

Create a Python file and populate it with:

from z3 import *

This allows us to generate instances with Python that Z3 can solve.

Instances

Let's formulate an instance as a four-tuple $(N, C, S, A)$ where

• $N$ is the number of exams to correct
• $C$ is a list of capacities, where each examiner is identified by their position of the list
• $S$ is a mapping from a single examiner to a set of examiners they should form a committee with
• $A$ is a symmetric relation, relating examiners that we should avoid placing in the same committee

We define a committee as a set of exactly two examiners (identified by their index in the list of capacities).

The code below suggests a Python representation of a problem instance. It is, as you must have noticed, blurred (until you click it). This is to encourage the reader to solve the problem on their own, and emphasize that what will be presented is a mere suggestion on how to attack the problem.

def example_instance():
    N = 283
    #    A    B    C    D   E   F
    C = [160, 150, 110, 60, 60, 30]
    S = {3 : {1, 2}, 4 : {1, 2}}
    A = {frozenset([3, 4])}
    return (N, C, S, A)

Constraint modeling

We need to capture our intention with first-order logic formulas, and preferably quantifier-free. In the context of SMT-solving, quantifier-free means that we only try to solve a set of constraints where no variable is bound by a quantifier; these are usually much easier to solve. Rather, we use a finite set of constant symbols, with some associated sort, and try to find an interpretation for them.

The end result needs to be a set of committees, where each committee consists of two examiners with a number of exams to correct. An important part of finding a reasonable encoding is to balance what part of the problem should be solved with Python and what should be solved by the SMT-solver. My experience is that a good rule of thumb is to move as much structural complexity to Python and encode the Z3 instance with simple structures.

Modeling committees

A natural encoding could be modeling a committee as an integer constant, where the value assigned to a committee corresponds to the number of exams they correct. If the committee don't are not assigned any exams, we discard it completely. It is quite easy to compute all possible committees, and make one integer constant for each of them.

Let's write a function that takes a list of capacities, and return a dictionary, associating committees to their corresponding integer constant. Remember that we represent a committee as a set of exactly two examiners.

def committees(C):
    cs = {frozenset([i,j])
          for i in range(len(C))
          for j in range(i+1, len(C))}
    return {c : Int(str(c)) for c in cs}

Capacity constraints

Now we must ensure that no examiner receives more exams than their capacity. Given an examiner $i$, where $0 <= i < |C|$, we let $c_i$ denote the set of all committees $i$ participates in. Then $\sum{c_i} <= C[i]$, i.e. the sum of the exams corrected by committees in $c_i$ does not exceed the capacity of the examiner $i$. We write a function that encodes these constraints.

def capacity_constraint(comms, C):
    return [sum(comms[c] for c in comms if i in c) <= C[i]
            for i in range(len(C))]

Because we are modeling committees as integers, we have to be careful not to allow committees correcting a negative number of exams.

def non_negative_constraint(comms):
    return [0 <= comms[c] for c in comms]

Committee constraints

The $S$ relation is sort of odd. That one examiner should form a committee with someone they relate to by $S$. This is not an absolute requirement, which is not ideal for a satisfiability problem, so we will ignore this constraint for now. The $A$ relation is similar, but clearer. For any pair $(i,j) \in A$, we don't form a committee consisting of those examiners.

def avoid_correct_with_constraint(comms, A):
    return [comms[frozenset([i, j])] == 0 for i, j in A]

All exams are corrected constraint

Each committee correct their exams two times (once by each examiner), so if the sum of all the committees is $N$, then all exams have been corrected twice (presumably by two different examiners). Let's encode that as a constraint.

def all_corrected_constraint(comms, N):
    return sum(comms.values()) == N

Invoking Z3

Now that we have functions that model our problem, we can invoke Z3.

def check_instance(instance):
    N, C, S, A = instance
    comms = committees(C)

    s = Solver()

    s.add(capacity_constraint(comms, C))
    s.add(non_negative_constraint(comms))
    s.add(all_corrected_constraint(comms, N))
    s.add(avoid_correct_with_constraint(comms, A))

    s.check()
    return s.model()

Calling check_instance(example_instance()) returns a model:

[frozenset({2, 4}) = 0,
 frozenset({0, 2}) = 0,
 frozenset({2, 3}) = 0,
 frozenset({1, 3}) = 0,
 frozenset({2, 5}) = 0,
 frozenset({3, 5}) = 0,
 frozenset({0, 5}) = 13,
 frozenset({1, 2}) = 110,
 frozenset({4, 5}) = 0,
 frozenset({1, 5}) = 17,
 frozenset({0, 3}) = 60,
 frozenset({0, 4}) = 60,
 frozenset({0, 1}) = 23,
 frozenset({3, 4}) = 0,
 frozenset({1, 4}) = 0]

This is not especially readable, so let's write a quick (and completely unreadable) prettyprinter.

def prettyprint(instance, m):
    N, C, S, A = instance
    comms = committees(C)
    exams = [sum(m[comms[c]].as_long() for c in comms if i in c)
             for i in range(len(C))]
    examiners = '\n'.join(['%s: %d/%d' % (chr(ord('A') + i), exams[i], C[i])
                           for i in range(len(C))])
    cs = [(c, m[comms[c]].as_long()) for c in sorted(comms, key=sorted)]
    csstr = '\n'.join([', '.join(map(lambda i: chr(ord('A') + i),
                                     sorted(c))) + ': ' + str(cv)
                       for c, cv in cs if cv > 0])
    print(examiners + '\n\n' + csstr)

This outputs the something like:

A: 156/160
B: 150/150
C: 110/110
D: 60/60
E: 60/60
F: 30/30

A, B: 23
A, D: 60
A, E: 60
A, F: 13
B, C: 110
B, F: 17

Note the something like. There are multiple ways to satisfy this set of constraints, and Z3 only provide some solution (if one exists).

Optimization

So far, we have found a way to model the problem and satisfy the constraints. However, it is preferable to have fewer committees, because all committees have to discuss the exams, causing administrative overhead. Z3 also provides optimization, meaning that we can find a smallest or largest solution for numeric theories. The underlying theory for optimization is MaxSMT.

Minimize committees

In our case, we want to minimize the number of committees. First we write a function to find the number of committees which we will soon minimize.

def number_of_committees(comms):
    return sum(If(0 < comms[c], 1, 0) for c in comms)

Now we can invoke Z3, using an Optimize instance and adding our minimization constraint.

def optimize_instance(instance):
    N, C, S, A = instance
    comms = committees(C)

    o = Optimize()

    o.add(capacity_constraint(comms, C))
    o.add(non_negative_constraint(comms))
    o.add(all_corrected_constraint(comms, N))
    o.add(avoid_correct_with_constraint(comms, A))

    o.minimize(number_of_committees(comms))

    o.check()
    return o.model()

There is still more than one way to satisfy this model, but we are guaranteed to get a minimal number of committees (which is 6 in our example).

A: 160/160
B: 150/150
C: 110/110
D: 56/60
E: 60/60
F: 30/30

A, B: 57
A, D: 43
A, E: 60
B, C: 93
C, F: 17
D, F: 13

Dealing with should

Remember $S$, which maps examiners to other examiners they should form a committee with. With optimization, we now have a way of expressing that some solution is more preferable than another. One way to model this is maximizing the number of exams given to committees that consists of an examiner $i$ that should be in a committee with examiner $j$. We want this for all such pairs $i,j$, and can achieve this by summing all such committees.

def should_correct_with_weight(comms, S, C):
    return sum(comms[frozenset([i, j])] for i in S for j in S[i])

When adding multiple optimization objectives (or goals), Z3 defaults to order the objectives lexicographically, i.e. in the order they appear. If we place the minimization of committees before the should_correct_with_weight, then we still are guaranteed to get a minimal number of committees.

def optimize_instance(instance):
    N, C, S, A = instance
    comms = committees(C)

    o = Optimize()

    o.add(capacity_constraint(comms, C))
    o.add(non_negative_constraint(comms))
    o.add(all_corrected_constraint(comms, N))
    o.add(avoid_correct_with_constraint(comms, A))

    o.minimize(number_of_committees(comms))
    o.maximize(should_correct_with_weight(comms, S, C))

    o.check()
    return o.model()

A: 156/160
B: 150/150
C: 110/110
D: 60/60
E: 60/60
F: 30/30

A, B: 90
A, C: 43
A, F: 23
B, E: 60
C, D: 60
C, F: 7

Optimize for capacities

Maybe we can try to satisfy (🙃) all the examiners by trying to close the gap between their capacity and the number of exams they end up correcting. Usually at the Department, there is quite a lot of flex in these capacities; if you are willing to correct $50$ exams, then you will most likely be okey with correcting $40$ and actually willing to correct $52$. Therefore, we can try to add some slack to the capacity.

In reality, the numbers from the original email were

A	158
B	150
C	108
D	60
E	60
F	15

But when we add them up, it turns out that they only have capacity to correct $551$ exams (and we need $2*N = 566$).

We create a new instance with the original values.

def original_instance():
    N = 283
    #    A    B    C    D   E   F
    C = [158, 150, 108, 60, 60, 15]
    S = {3 : {1, 2}, 4 : {1, 2}}
    A = {frozenset([3, 4])}
    return (N, C, S, A)

Now we can compute a "badness"-score (or weight) for the examiners capacities, rather than just stating we cannot surpass their capacity.

def capacity_slack(comms, i, C):
    a = sum(comms[c] for c in comms if i in c)
    return If(a > C[i], a - C[i], C[i] - a)

For the total weight of the capacities, we try to just sum the weights for each examiner.

def capacity_weight(comms, C):
    return sum(capacity_slack(comms, i, C) for i in range(len(C)))

We can now add all of the optimization objectives, stating that it most important to respect the capacities of the examiners, then prefer a small number of committees, and lastly the should requirement from the previous section.

def optimize_instance(instance):
    N, C, S, A = instance
    comms = committees(C)

    o = Optimize()

    o.add(non_negative_constraint(comms))
    o.add(all_corrected_constraint(comms, N))
    o.add(avoid_correct_with_constraint(comms, A))

    o.minimize(capacity_weight(comms, C))
    o.minimize(number_of_committees(comms))
    o.maximize(should_correct_with_weight(comms, S, C))

    o.check()
    return o.model()

We now get something like:

A: 158/160
B: 158/150
C: 110/110
D: 65/60
E: 60/60
F: 15/30

A, B: 158
C, D: 65
C, E: 45
E, F: 15

If we were to prioritize the should requirement over minimizing the number of committees, then we would get something like:

A: 158/160
B: 158/150
C: 109/110
D: 65/60
E: 60/60
F: 16/30

A, B: 98
A, C: 44
A, F: 16
B, E: 60
C, D: 65

COMMENT Local variables