Solving the "Seven Segment Search" Puzzle with Z3

This week I stumbled upon someone wondering whether the second part of the recent Advent of Code puzzle “Seven Segment Search” can be expressed as a constraint satisfaction problem. As attested by the replies: yes, it can. However, I think the question deserves a more extensive discussion than just a few comments in a thread. This post tries to provide a more instructive answer and raise awareness for the tradeoffs or solver misuses some solutions put up with.

I assume that the reader is familiar with mathematical notation and

• just struggles to express the posed problem in a formal, declarative way, or
• is interested in seeing how the SMT solver Z3 can be used to express and solve the problem in several logics. It takes only few steps to get from a quantifier-laden high-level formulation to what is effectively propositional logic.

The Problem Statement

A functioning seven-segment display is supposed to represent digits as follows:

By associating each segment with a character, we can clearly describe which segments are supposed to light up for each digit:

 4
 5
 6
 7
 8
 9
10
11
12
13
14
15

DIGIT_SEGMENTS = {
    0: 'abcefg',
    1: 'cf',
    2: 'acdeg',
    3: 'acdfg',
    4: 'bcdf',
    5: 'abdfg',
    6: 'abdefg',
    7: 'acf',
    8: 'abcdefg',
    9: 'abcdfg'
}

The crux of the Seven Segment Search puzzle is that we are faced with a seven-segment display whose wiring got mixed up. As a result, instead of turning on segments c and f to display a 1, our display may turn on segments a and b instead. We don’t get to see how the wrong wiring looks like though. All we can observe is a sequence of patterns and our task is to make sense of it. That is, to find out which digit each pattern represents:

Once we’ve figured out how to map the observable patterns to the digits they were originally intended to represent, we can use this knowledge to read the number shown on a four-digit seven-segment display that uses the very same wiring:

The decoded number 5353 is the solution to this problem instance. However, Advent of Code is about programming, so – to make people solve the puzzle programmatically – there are actually 200 independent instances that need to be solved and their 4-digit numbers summed up.

Puzzle Input File

The puzzle input file consists of 200 lines – each of which encodes an independent problem instance. The first part of a line describes the ten (unordered) patterns that can be observed on the malfunctioning seven-segment display. The second part represents the four-digit seven-segment display that needs be decoded. The above problem instance is in fact the original introductory example. It may appear as follows in the input file:

acedgfb cdfbe gcdfa fbcad dab cefabd cdfgeb eafb cagedb ab | cdfeb fcadb cdfeb cdbaf

Formalising a Problem Instance

If you give it some thought, it is easy to come up with efficient procedures to solve any problem instance of this puzzle by exploiting domain-specifics like the patterns' numbers of segments. For example, since 1 is the only digit that is displayed by exactly two segments, any observed pattern with just two lit segments must be representing it as well. However, in general, such procedures may require significant alterations and re-analysis of puzzle aspects to exploit even if seemingly small variations are introduced.

Declarative approaches, which merely rely on a description of what a solution to a problem is, rather than how to find it, tend to be less prone to this. Therefore, instead of investing in a solution procedure tailored to a specific problem from the start, it may be sensible to first express the problem in a declarative formalism for which generic solvers exist. If, at some point, the tradeoff between flexibility and performance becomes problematic, one can still look into designing a problem-specific, imperative procedure.

In the following, we will use first-order logic to express the puzzle in a formal, declarative way. This is a reasonably high-level logic which allows us to conveniently express the relations between the problem’s entities, and is amenable to automated theorem proving.

Characterisation in First-Order Logic

Let us start by formalising the thing we know: how each digit maps to a set of segments on a (functioning) seven-segment display. In first-order logic sets are characterised by predicates. For example, if the domain of discourse is $\mathbb{Z}$, predicate $\mathit{neg}(x) := x<0$ chracterises the set of negative integers. Accordingly, to characterise the segments of each digit $d$, we could define 10 predicates $\mathit{segment}_d(s)$. However, it is probably more convenient to let one binary predicate $$ \mathit{digitSegment}:\underset{\overbrace{\\{0,1,2,3,4,5,6,7,8,9\\}}}{\mathit{Digit}}\times \underset{\overbrace{\\{a,b,c,d,e,f,g\\}}}{\mathit{Segment}} $$ characterise the digit’s segments. That is, require the following to hold $$ \tag{1}\mathit{digitSegment}(d,s) \iff s \text{ is a segment of } d $$ for all digits $d$ and segments $s$.

We’d like to have a similar characterisation of the mapping of digits to segments on the broken seven-segment display, but that can’t be stated directly as it depends on the (unknown) permutation of segments, or wires, if you will. Therefore, to first model the permutation, we introduce an uninterpreted function $$ \mathit{Perm}:\mathit{Segment}\to\mathit{Segment} $$ but restrict the possible interpretations of $\mathit{Perm}$ to permutations only. This is achieved by requiring the function to be bijective: $$ \tag{2}\forall s,s'\in\mathit{Segment}\ldotp s = s' \iff \mathit{Perm}(s) = \mathit{Perm}(s') $$

Based on that we can now characterise the permuted digit segments $$ \mathit{PermDigitSegment}:\mathit{Digit}\times \mathit{Segment} $$ by specifying that $\mathit{Perm}(s)$ must be a permuted segment of $d$ iff $s$ is a segment of $d$ on the functioning display: $$ \tag{3}\mathit{PermDigitSegment}(d,\mathit{Perm}(s)) \iff \mathit{digitSegment}(d,s) $$

Note that so far we’ve only formalised aspects that are common to all problem instances. Even the permutation $\mathit{Perm}$, which differs from instance to instance, could be introduced without referring to instance-specific details.

What distinguishes an instance are the ten patterns that can be observed on the (malfunctioning) display, i.e. the first part of each line of the input file. Just as $\mathit{digitSegment}$ characterises the segments behind each possible digit, the idea here is to introduce a predicate $$ \mathit{patternSegment}: \underset{\overbrace{\\{0,1,2,3,4,5,6,7,8,9\\}}}{\mathit{Index}} \times \mathit{Segment} $$ to characterise the segments behind each of the ten observable patterns. That is, assert for all indices $i$ and segments $s$ that $$ \tag{4}\mathit{patternSegment}(i,s) \iff s \text{ is a segment of the $i$-th pattern}. $$

The only thing that remains to be formalised is the relation between the observed patterns and the other “objects”. That’s the actual puzzle. What we know from the puzzle description is that each of the observable patterns matches the permuted segments of some digit. Therefore, there must be a “decoding function” $$ \mathit{Idx2dig}: \mathit{Index} \to \mathit{Digit} $$ which maps each observed pattern – more precisely its index $i$ – in such a way to a digit $d$ that the permuted segments of $d$ correspond to the observed pattern. Similar to $(3)$, we can constrain $\mathit{Idx2dig}$ to behave like this by specifying that $s$ must be a permuted segment of digit $\mathit{Idx2dig}(i)$ iff $s$ is a segment of the $i$-th observed pattern $$ \tag{5}\mathit{PermDigitSegment}(\mathit{Idx2dig}(i),s) \iff \mathit{patternSegment}(i,s) $$ for all indices $i$ and segments $s$.

The Characterisation at a Glance

Overall, we end up with the following constraints $$ \begin{aligned} \mathit{digitSegment}(d,s) &\iff s \text{ is a segment of } d\\ s = s' &\iff \mathit{Perm}(s) = \mathit{Perm}(s')\\ \mathit{PermDigitSegment}(d,\mathit{Perm}(s)) &\iff \mathit{digitSegment}(d,s)\\ \mathit{patternSegment}(i,s) &\iff s \text{ is a segment of the $i$-th pattern}\\ \mathit{PermDigitSegment}(\mathit{Idx2dig}(i),s) &\iff \mathit{patternSegment}(i,s) \end{aligned} $$ for all $d\in\mathit{Digit}$, $s,s'\in\mathit{Segment}$, and indices $i\in\mathit{Index}$.

If we now manage to find an interpretation of the uninterpreted symbols that satisfies all these constraints, the particular puzzle instance will be solved. We can then simply use $\mathit{Idx2dig}$ to map the patterns on the malfunctioning four-digit seven-segment display back to digits, or use $\mathit{Perm}$ to undo the permutation of segments.

Solving the Puzzle via Z3

While there are many solvers, formalisms, and technologies that we can leverage to obtain a satisfying interpretation of the above constraints, this post illustrates how to do it with the SMT solver Z3. More precisely, with its Python bindings.

Domains

To express the above predicates we first have to introduce the domains, or Sorts, our values will be from. Finite domains of unrelated values can be created via EnumSort, and that’s exactly the kind of values we’re dealing with in the puzzle. Since we will also need to convert between these values and their Python counterparts – int for digits and indices, and str for segments – we accompany each domain with corresponding mappings:

17
18
19
20
21
22
23
24
25
26
27
28
29
30

# Domain (and converters) to represent Digits
DigitSort, digits = EnumSort('Digit', ('0', '1', '2', '3', '4', '5', '6', '7', '8', '9'))
def mk_digit(i: int): return digits[i]
digit2int = {d: int(str(d)) for d in digits}

# Domain (and converters) to index/identify the ten observable patterns
IndexSort, indices = EnumSort('Index', ('0', '1', '2', '3', '4', '5', '6', '7', '8', '9'))
def mk_index(i: int): return indices[i]
index2int = {i: int(str(i)) for i in indices}

# Domain (and converters) to represent segments/wires
SegmentSort, segments = EnumSort('Segment', ('a', 'b', 'c', 'd', 'e', 'f', 'g'))
def mk_segment(char: str): return segments[ord(char) - ord('a')]
segment2char = {s: str(s) for s in segments}

Of course it is possible to use IntSort and StringSort to model digits, indices and segments instead of introducing dedicated finite domains, and some of the suggested approaches do resort to this. However, when doing so one must be aware of the implications.

For example, to exploit problem-specifics, one of the posted solutions features integer addition in its constraints. The result of this is that the characterisation ends up in a more complex fragment of first-order logic than necessary – in quantifier-free linear integer arithmetic (QF_LIA). This, in turn, forces SMT solvers to employ more complex techniques than necessary to solve the puzzle. However, if higher-level modelling better captures the semantics of the problem, it may pay off to use a more expressive (sub-)logic – even if reduction to a less expressive one is possible. One should just be careful to not add such complexity inadvertently. Otherwise, one can quickly end up expressing a decidable problem in terms of an undecidable one.

Solving the Puzzle Incrementally

To solve the overall puzzle, we have to solve the 200 independent problem instances described in the input file and combine their solutions. Although it is possible to construct and solve the instances' constraints independently, as most of the suggested solutions do, it is more efficient to avoid starting from scratch 200 times. Closer inspection of constraints $(1)–(5)$ shows that the instances' formalisations only differ in $(4)$, i.e. the definition of $\mathit{patternSegment}$. Therefore, a simple way to avoid starting from scratch is by first adding the core constraints $(1)–(3),(5)$ to the solver’s stack of constraints and then iteratively checking satisfiability with each of the 200 variants of $(4)$ swapped in at the top of the stack.

The following encoding-agnostic procedure implements the suggested approach. It uses the scope management operations push and pop to replace the definition of $\mathit{patternSegment}$ between satisfiability checks. When a satisfying interpretation – a so called model – is found, we can inspect it to learn how the observed patterns map to digits:

53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72

def solve_puzzle(filename: str, encoder: PuzzleEncoder):
    s = SolverFor(encoder.logic())
    s.add(encoder.encode_core())

    # Solve problem instance encoded in each line of the input file & sum the decoded output
    acc = 0
    for line in open(filename).read().splitlines():
        observed_patterns, output = parse_line(line)

        s.push()
        s.add(encoder.encode_variant(observed_patterns))
        assert s.check() == sat, 'Cannot find satisfying interpretation'
        idx2dig = encoder.interpret(s.model())
        s.pop()

        # Decode and add output value to accumulator
        output_digits = [idx2dig[observed_patterns.index(pattern)] for pattern in output]
        acc += sum(d * factor for d, factor in zip(output_digits, [1000, 100, 10, 1]))

    return acc

The procedure is encoding-agnostic, in the sense that it only expects the characterisation code to implement the following self-explanatory interface:

33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

class PuzzleEncoder:
    """Characterises the decoding problem posed in a line of the puzzle input."""

    def logic(self) -> str:
        """The logic that the produced encoding is in."""
        pass

    def encode_core(self) -> list[ExprRef]:
        """Characterise the part common to all decoding problems."""
        pass

    def encode_variant(self, patterns: list[str]) -> list[ExprRef]:
        """Characterise the distinctive part of a decoding problem, i.e. the observed patterns."""
        pass

    def interpret(self, model: ModelRef) -> list[int]:
        """Interpret the model to extract the mapping 'observed pattern index -> represented digit'."""
        pass

As you can hopefully see, using an SMT solver incrementally is pretty straight forward in the context of this puzzle. Although we’ve just started, our SMT-based puzzle solver is almost finished already. It merely remains to provide a concrete implementation of PuzzleEncoder.

High-level Encoding

The most obvious solution is to just use the means Z3 provides to express the characterisation we came up with above.

It is handy to keep the symbols that we use in our encoding around, e.g. to reference them in the encoding functions, or to look up their interpretation later. Therefore, we declare these symbols as members of the encoder. What may catch you by surprise is that, following the SMT-LIB standard, there is no special way to create a predicate in Z3. Instead, predicates are understood as functions with a Boolean result:

75
76
77
78
79
80
81
82
83
84
85
86

class HighLevelEncoder(PuzzleEncoder):
    """A high-level encoding featuring quantifiers, uninterpreted functions and finite domains"""

    def __init__(self):
        self.digit_segment = Function('digitSegment', DigitSort, SegmentSort, BoolSort())
        self.perm = Function('Perm', SegmentSort, SegmentSort)
        self.perm_digit_segment = Function('PermDigitSegment', DigitSort, SegmentSort, BoolSort())
        self.pattern_segment = Function('patternSegment', IndexSort, SegmentSort, BoolSort())
        self.idx2dig = Function('Idx2dig', IndexSort, DigitSort)

    def logic(self) -> str:
        return 'UF'  # more precisely 'UFFD' but that's not known to Z3

Besides the standard logics Z3 supports several others. However, instead of guesswork, I find it the easiest to just look up the strings that map to supported (sub-)logics.

With the Python bindings, the expressions that represent our core constraints look very similar to the original ones. What stands out is that, in contrast to our formalisation, the variables we quantify over must be created beforehand. Furthermore, in code, the right-hand side of $(1)$ is a bit less readable than the $s \text{ is a segment of }d$ (cf. lines 96-98):

 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117

def encode_core(self) -> list[ExprRef]:
    res = []

    # Characterise digitSegment according to DIGIT_SEGMENTS
    d = Const('d', DigitSort)
    s = Const('s', SegmentSort)
    res.append(
        ForAll([d, s],
               self.digit_segment(d, s) == Or([
                   And(d == mk_digit(dig), Or([s == mk_segment(char) for char in string]))
                   for dig, string in DIGIT_SEGMENTS.items()])))

    # Perm should be a bijection
    s_prime = Const("s'", SegmentSort)
    res.append(ForAll([s, s_prime],
                      (s == s_prime) == (self.perm(s) == self.perm(s_prime))))

    # Characterise how PermDigitSegment derives from digitSegment and Perm, i.e.
    # PermDigitSegment(d, Perm(s)) == digitSegment(d, s)
    res.append(
        ForAll([d, s],
               self.perm_digit_segment(d, self.perm(s)) == self.digit_segment(d, s)))

    # Require Idx2dig to be correct wrt. its role as "decoding function", i.e.
    # PermDigitSegment(Idx2dig(i), s) == patternSegment(i, s)
    i = Const('i', IndexSort)
    res.append(ForAll([i, s],
                      self.perm_digit_segment(self.idx2dig(i), s) == self.pattern_segment(i, s)))

    return res

Since the constraints $(1)$ and $(4)$ have the same form, encode_variant looks a lot like lines 91–98 from encode_core:

119
120
121
122
123
124
125
126
127
128
129
130
131

def encode_variant(self, patterns: list[str]) -> list[ExprRef]:
    res = []

    # Characterise `patternSegment` according to `patterns`
    i = Const('i', IndexSort)
    s = Const('s', SegmentSort)
    res.append(
        ForAll([i, s],
               self.pattern_segment(i, s) == Or([
                   And(i == mk_index(idx), Or([s == mk_segment(char) for char in string]))
                   for idx, string in enumerate(patterns)])))

    return res

When our constraints are determined to be satisfiable, the returned model contains – among other things – the information how $\mathit{Idx2dig}$ maps indices to digits. Since only the encoder needs to know how exactly the encoding works, i.e. solve_puzzle shouldn’t have to deal with the declared symbols, interpret looks up in the model what each input is mapped to and returns the findings as a plain list of integers. The integer at index $i$ denotes the digit encoded by the $i$-th observed pattern:

133
134

def interpret(self, model: ModelRef) -> list[int]:
    return [digit2int[model.eval(self.idx2dig(i))] for i in indices]

At this point you can give our puzzle solver a try. Just make sure to pass an instance of HighLevelEncoder to solve_puzzle. This naïve solution isn’t exactly fast, taking roughly 30s, but comping up with it didn’t require much thought beyond the original formalisation. Let’s see whether this can be improved by switching to a less expressive (sub-)logic.

Mid-level Encoding

Although quantifiers facilitate concise characterisation they are also a source of complexity – especially in the context of small finite domains. Therefore, in the next step, we will bring our constraints into a quantifier-free fragment of first-order logic.

Dropping the quantifiers does not entail any changes to the declared symbols, but the new encoder should communicate that the constraints it produces are free of quantifiers:

137
138
139
140
141
142
143
144
145
146
147
148

class MidLevelEncoder(PuzzleEncoder):
    """A quantifier-free mid-level encoding featuring uninterpreted functions and finite domains"""

    def __init__(self):
        self.digit_segment = Function('digitSegment', DigitSort, SegmentSort, BoolSort())
        self.perm = Function('Perm', SegmentSort, SegmentSort)
        self.perm_digit_segment = Function('PermDigitSegment', DigitSort, SegmentSort, BoolSort())
        self.pattern_segment = Function('patternSegment', IndexSort, SegmentSort, BoolSort())
        self.idx2dig = Function('Idx2dig', IndexSort, DigitSort)

    def logic(self) -> str:
        return 'QF_UFDT'  # more precisely 'QF_UFFD' but that's not known to Z3

The approach to get rid of a forall quantifier is simple: just explicitly enumerate the values and assert the nested constraint for each. This leaves us with an increased number of constraints but spares Z3 the necessity of dealing with quantifiers:

150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172

def encode_core(self) -> list[ExprRef]:
    res = []

    # Characterise digitSegment according to DIGIT_SEGMENTS
    for d, s in product(digits, segments):
        expected = segment2char[s] in DIGIT_SEGMENTS[digit2int[d]]
        res.append(self.digit_segment(d, s) == expected)

    # Perm should be a bijection
    for s, other in product(segments, segments):
        res.append((s == other) == (self.perm(s) == self.perm(other)))

    # Characterise how PermDigitSegment derives from digitSegment and Perm, i.e.
    # PermDigitSegment(d, Perm(s)) == digitSegment(d, s)
    for d, s in product(digits, segments):
        res.append(self.perm_digit_segment(d, self.perm(s)) == self.digit_segment(d, s))

    # Require Idx2dig to be correct wrt. its role as "decoding function", i.e.
    # PermDigitSegment(Idx2dig(i), s) == patternSegment(i, s)
    for i, s in product(indices, segments):
        res.append(self.perm_digit_segment(self.idx2dig(i), s) == self.pattern_segment(i, s))

    return res

Aside from the substitution of quantification by iteration, the code is effectively the same as in our first encoder. I find this version to be even more readable that the previous one, mostly because it is so easy to express $s \text{ is a segment of }d$ for a concrete pair $(d,s)$.

The rest of the encoder does not provide any new insights and is only shown for the sake of completeness:

174
175
176
177
178
179
180
181
182
183
184
185

def encode_variant(self, patterns: list[str]) -> list[ExprRef]:
    res = []

    # Characterise `patternSegment` according to `patterns`
    for i, seg in product(indices, segments):
        expected = segment2char[seg] in patterns[index2int[i]]
        res.append(self.pattern_segment(i, seg) == expected)

    return res

def interpret(self, model: ModelRef) -> list[int]:
    return [digit2int[model.eval(self.idx2dig(i))] for i in indices]

Now, try running solve_puzzle with this new encoder. It turns out that moving to a quantifier-free fragment of first-order logic reduces the runtime significantly (to ~6s). One might wonder whether going even lower will yield similar performance gains.

Low-level Encoding

Similar to quantifiers, uninterpreted functions introduce some complexity but do not add any expressivity that is essential to our characterisation. If our constraints were free of both quantifiers and uninterpreted functions they’d be effectively propositional. In fact, Z3 wouldn’t even reach for SMT procedures but directly employ its SAT solver.

Now, how do we get rid of the uninterpreted functions? Since all of our functions have finite domains, it is possible to introduce symbolic values to replace each possible function application in our constraints. That is, for each function and input, we introduce a variable to denote the result. This of course impacts the symbols we declare. For example, where we previously used an uninterpreted function $$ \mathit{digitSegment}:\mathit{Digit}\times\mathit{Segment}\to\mathbb{B} $$ to represent the predicate $\mathit{digitSegment}:\mathit{Digit}\times\mathit{Segment}$, we now have a Boolean variable for each pair $(d,s)\in\mathit{Digit}\times\mathit{Segment}$:

188
189
190
191
192
193
194
195
196
197
198
199

class LowLevelEncoder(PuzzleEncoder):
    """A quantifier-free low-level encoding featuring finite domains. Effectively a SAT instance."""

    def __init__(self):
        self.digit_segment = {(d, s): Bool(f'digitSegment({d},{s})') for d, s in product(digits, segments)}
        self.perm = {s: Const(f'Perm({s})', SegmentSort) for s in segments}
        self.perm_digit_segment = {(d, s): Bool(f'PermDigitSegment({d},{s})') for d, s in product(digits, segments)}
        self.pattern_segment = {(i, s): Bool(f'patternSegment({i},{s})') for i, s in product(indices, segments)}
        self.idx2dig = {i: Const(f'Idx2dig({i})', DigitSort) for i in indices}

    def logic(self) -> str:
        return 'QF_FD'

We can now use the freshly introduced variables within our constraints, in place of the original function applications. This does complicate constraints where we previously had nested function applications, such as $(3)$ and $(5)$. Here, the idea is similar to the alternative formulation of $(3)$: we constrain the result of the outer function application depending on the result of the nested function application. However, without uninterpreted functions, some constraint simplification opportunities may become more obvious, too. Since the domain and value range of $\mathit{perm}$ are equal the bijectivity constraint can be simplified to “distinct applications of $\mathit{perm}$ return distinct segments”:

201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224

def encode_core(self) -> list[ExprRef]:
    res = []

    # Characterise digitSegment according to DIGIT_SEGMENTS
    for d, s in product(digits, segments):
        expected = segment2char[s] in DIGIT_SEGMENTS[digit2int[d]]
        res.append(self.digit_segment[(d, s)] == expected)

    # Perm should be a bijection
    res.append(Distinct(list(self.perm.values())))

    # Characterise how PermDigitSegment derives from digitSegment and Perm, i.e.
    # PermDigitSegment(d, Perm(s)) == digitSegment(d, s)
    for s, perm_s, d in product(segments, segments, digits):
        res.append(Implies(self.perm[s] == perm_s,
                           self.perm_digit_segment[(d, perm_s)] == self.digit_segment[(d, s)]))

    # Require Idx2dig to be correct wrt. its role as "decoding function", i.e.
    # PermDigitSegment(Idx2dig(i), s) == patternSegment(i, s)
    for i, d, s in product(indices, digits, segments):
        res.append(Implies(self.idx2dig[i] == d,
                           self.perm_digit_segment[(d, s)] == self.pattern_segment[(i, s)]))

    return res

As with the previous encodings, the rest of the code holds no surprises and is merely listed for the sake of completeness:

226
227
228
229
230
231
232
233
234
235
236
237

def encode_variant(self, patterns: list[str]) -> list[ExprRef]:
    res = []

    # Characterise `patternSegment` according to `patterns`
    for i, s in product(indices, segments):
        expected = segment2char[s] in patterns[index2int[i]]
        res.append(self.pattern_segment[(i, s)] == expected)

    return res

def interpret(self, model: ModelRef) -> list[int]:
    return [digit2int[model.eval(self.idx2dig[i])] for i in indices]

This is where we stop tweaking the encoding. You will find that running solve_puzzle with an instance of LowLevelEncoder again reduces the runtime significantly (to ~1s).

Do Try This at Home

Interestingly, if the LowLevelEncoder is used, each check in solve_puzzle takes only about 500µs. So why does solve_puzzle take 1s? That’s an order of magnitude longer than 200 times 500µs! Well, running a profiler shows that most time is wasted in the bindings – specifically in ExprRef.__eq__.

There are several things you can do to squeeze out better execution times:

• Now that you’ve seen how to express the constraints with the Python bindings, give the bindings for C++ – or some other language with less overhead than Python – a try.
• Avoid recreating the constraints for each variant. They have the same form anyway. Instead, try to come up with a way to leverage solving under assumptions, i.e. delete encode_variant and rather communicate the observed patterns by passing appropriate assumptions to the check function.
• Alternatively, instead of solving each of the 200 problem instances separately, try to combine them all into a single set of constraints. A single invocation of check shall suffice to solve the complete puzzle.
• Assuming you do implement the above suggestion, try feeding the constraints to a dedicated SAT solver for another performance gain. Have a look at this section from a previous post, if you need some guidance on how to do this.