Logic Made Linear

An integer program speaks only in linear inequalities, and yet it can be made to say things that look nothing like arithmetic. Two puzzles from a second collection of Hartmann’s show the range. In Circuit Scramble the constraints are logic gates, and the trick is that each of AND, OR, XOR and NOT can be pinned down by a handful of inequalities on zero-one variables. In Binary Sudoku the awkward rule is that no two rows may be alike, an inequality between whole rows, and that too comes down to linear constraints once a row is read as a number. Both puzzles are really lessons in translation: take a condition the solver cannot state directly and find the inequalities that mean the same thing.

Circuit Scramble

The app shows a small logic circuit, a few inputs feeding a tree of gates up to one output. Each input is a switch, on or off, and the output lamp lights when the circuit evaluates to true. The player flips switches until it lights, and the score is the number of flips, so the question is the fewest changes from the starting position that turn the output on.

Variables

A binary variable carries the logical state of every node, input or gate alike, $$x_i = 1 \iff \text{node } i \text{ is true}.$$

Gates as inequalities

Each gate ties its output node to its inputs. The four kinds each have a linear reading, exact on zero-one variables. For an AND, the output is one exactly when both inputs are; for an OR, when at least one is; the XOR is one when the inputs disagree; the NOT simply flips: $$\begin{array}{ll} \text{AND } y = a \wedge b: & y \le a,\ y \le b,\ y \ge a + b - 1, \\ \text{OR } y = a \vee b: & y \ge a,\ y \ge b,\ y \le a + b, \\ \text{XOR } y = a \oplus b: & y \le a + b,\ y \ge a - b,\ y \ge b - a,\ y \le 2 - a - b, \\ \text{NOT } y = \neg a: & y = 1 - a . \end{array}$$ The output node is required true, $x_{\text{out}} = 1$, and the objective counts the switches moved. A switch that starts off contributes its new value $x_i$; one that starts on contributes $1 - x_i$; so with $s_i$ the starting state, $$\min \ \sum_{i \,\text{an input}} \bigl( x_i \ \text{if}\ s_i = 0,\ \text{else}\ 1 - x_i \bigr) .$$

from ortools.sat.python import cp_model

def solve_circuit(gates, output, inputs, init):
    m = cp_model.CpModel()
    nodes = set(inputs) | {g[0] for g in gates}
    x = {i: m.NewBoolVar("") for i in nodes}
    for out, op, a, b in gates:
        if op == "AND":
            m.Add(x[out] <= x[a])
            m.Add(x[out] <= x[b])
            m.Add(x[out] >= x[a] + x[b] - 1)
        elif op == "OR":
            m.Add(x[out] >= x[a])
            m.Add(x[out] >= x[b])
            m.Add(x[out] <= x[a] + x[b])
        elif op == "XOR":
            m.Add(x[out] <= x[a] + x[b])
            m.Add(x[out] >= x[a] - x[b])
            m.Add(x[out] >= x[b] - x[a])
            m.Add(x[out] <= 2 - x[a] - x[b])
        elif op == "NOT":
            m.Add(x[out] == 1 - x[a])
    m.Add(x[output] == 1)
    m.Minimize(sum(x[i] if init[i] == 0 else 1 - x[i]
                   for i in inputs))
    s = cp_model.CpSolver()
    s.Solve(m)
    return int(s.ObjectiveValue()), {i: s.Value(x[i])
                                     for i in inputs}

Take a circuit on six inputs, each gate written as its output node, its kind, and its one or two feeding nodes: $$\begin{array}{rcl} g_7 &=& x_1 \wedge x_2 \\ g_8 &=& x_3 \oplus x_4 \\ g_9 &=& g_8 \wedge x_5 \\ g_{10} &=& g_7 \vee g_9 \\ g_{11} &=& \neg\, x_6 \\ g_{12} &=& g_{10} \wedge g_{11} \end{array}$$ with $g_{12}$ the output. The switches start at $x_1 \dots x_6 = 0, 0, 0, 1, 0, 1$, and the output is then off. The model finds that two switches are needed and no fewer: turn input $5$ on and input $6$ off. With those, $g_8 = x_3 \oplus x_4 = 1$ flows through $g_9 = g_8 \wedge x_5 = 1$ and $g_{10} = 1$, while $g_{11} = \neg x_6 = 1$, so $g_{12} = 1$ and the lamp lights. A sweep over all sixty-four input settings confirms two is the minimum and that this is the only two-switch fix.

This is the same move as the lie-detector of an earlier chapter, where a logical AND was linearised to catch a liar; here the whole grammar of gates is laid out, with the XOR the one worth a second look. Its four inequalities say that $y$ and the pair $a, b$ cannot take the three forbidden patterns, leaving exactly the four where the output matches the parity of the inputs.

Binary Sudoku

Binary Sudoku, sold also as Binairo or Takuzu, fills an $n \times n$ grid ($n$ even) with zeros and ones. Three rules hold. Each row and each column carries as many ones as zeros. No three cells in a line, across or down, share a value. And no two rows are identical, nor any two columns. A scatter of givens fixes the start.

Variables and the first two rules

One binary per cell, $x_{ij} \in \{0, 1\}$, the value written there. The balance rule is a sum, and the no-three rule is a window of three forced to hold at least one of each value, that is, to sum to one or two: $$\sum_j x_{ij} = \tfrac{n}{2} \ (\forall i), \qquad \sum_i x_{ij} = \tfrac{n}{2} \ (\forall j),$$ $$1 \le x_{ij} + x_{i,j+1} + x_{i,j+2} \le 2,$$ and the same for every vertical triple.

Distinctness as an inequality

The third rule is the interesting one, because “these two rows differ” is not something a linear solver states directly. Read each row as a binary number, $$R_i = \sum_{j} 2^{\,j-1} x_{ij},$$ so two rows are equal exactly when their numbers are. Now $R_i \ne R_k$ is forced the way a solver forces an either-or: a binary $y_{ik}$ chooses which row is the larger, and a big constant $M = 2^{n}$ switches the two bounds on and off, $$R_i - R_k \ge 1 - M\,(1 - y_{ik}), \qquad R_k - R_i \ge 1 - M\,y_{ik} .$$ When $y_{ik} = 1$ the first bound bites and $R_i > R_k$; when $y_{ik} = 0$ the second does and $R_k > R_i$; either way the rows are unequal. The same device on the column numbers keeps the columns apart. Stated this way it is pure linear programming. The listing says the identical thing in the solver’s own idiom: bind each row and column to its number and ask that all the row numbers be different, and all the column numbers too.

from ortools.sat.python import cp_model

def solve_binairo(n, givens):
    m = cp_model.CpModel()
    x = {(i, j): m.NewBoolVar("")
         for i in range(n) for j in range(n)}
    for i in range(n):
        m.Add(sum(x[i, j] for j in range(n)) == n // 2)
        m.Add(sum(x[j, i] for j in range(n)) == n // 2)
        for j in range(n - 2):
            m.Add(x[i, j] + x[i, j + 1] + x[i, j + 2] >= 1)
            m.Add(x[i, j] + x[i, j + 1] + x[i, j + 2] <= 2)
            m.Add(x[j, i] + x[j + 1, i] + x[j + 2, i] >= 1)
            m.Add(x[j, i] + x[j + 1, i] + x[j + 2, i] <= 2)
    rows = [m.NewIntVar(0, (1 << n) - 1, "") for _ in range(n)]
    cols = [m.NewIntVar(0, (1 << n) - 1, "") for _ in range(n)]
    for i in range(n):
        m.Add(rows[i] == sum((1 << j) * x[i, j]
                             for j in range(n)))
        m.Add(cols[i] == sum((1 << j) * x[j, i]
                             for j in range(n)))
    m.AddAllDifferent(rows)
    m.AddAllDifferent(cols)
    for (i, j), b in givens.items():
        m.Add(x[i, j] == b)
    s = cp_model.CpSolver()
    s.Solve(m)
    return [[s.Value(x[i, j]) for j in range(n)]
            for i in range(n)]

Here is a six-by-six start, a dot for an empty cell: $$\begin{array}{cccccc} 1 & \cdot & \cdot & \cdot & 1 & \cdot \\ \cdot & \cdot & 1 & \cdot & \cdot & 0 \\ \cdot & 1 & \cdot & 1 & \cdot & \cdot \\ 0 & \cdot & \cdot & \cdot & 1 & \cdot \\ \cdot & \cdot & 1 & \cdot & \cdot & 1 \\ \cdot & 1 & \cdot & 0 & \cdot & \cdot \end{array}$$ Twelve givens, two to a row, and the three rules close the rest to a single grid: $$\begin{array}{cccccc} 1 & 0 & 0 & 1 & 1 & 0 \\ 1 & 0 & 1 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 & 0 & 1 \\ 0 & 1 & 0 & 1 & 1 & 0 \\ 1 & 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 1 & 0 & 0 & 1 \end{array}$$ An independent count finds no second filling. Every row holds three of each digit, no run of three repeats, and the six rows, read as the numbers $25, 21, 42, 26, 37, 38$, are all different, as are the six columns.

Both puzzles took a condition that is not arithmetic, a logic gate or a demand that two things differ, and replaced it with inequalities that admit exactly the same zero-one solutions. That replacement is most of what modelling is: not the sums that come easily, but the rules that do not, rewritten until the solver can read them.

Sources. Circuit Scramble and Binary Sudoku, with four further apps (Starbattle, V3ck, Monodot, and a knight’s tour), are modelled by Sönke Hartmann, Puzzle—More Logic Puzzle Apps Solved by Mathematical Programming, INFORMS Transactions on Education volume $20$, number $1$ ($2019$), pages $49$–$55$, which gives the gate linearisations used here and the binary-encoding device for the row-and-column inequality. The circuit and the Binary Sudoku grid are the present chapter’s own instances; the two-switch minimum and the unique filling are each produced and checked by the models above. The AND-linearisation appears earlier in this book in the lie-detector puzzle. Hartmann credits the Circuit Scramble app to Rob van Staalduinen of Suborbital Games (Canada); Binary Sudoku, known as Binairo or Takuzu, runs in many apps (Mr. Binairo, LogiBrain Binary and others), as he notes.