Not sure how concrete/practical you'd consider this, but here's one:
In last year's Advent of Code programming contest, one of the trickier problems involved taking a collection of points in 3D space, each of which has a "range" defined by Manhattan distance, and finding the location that is "in range" of the maximum number of them.
Now, this isn't a theoretically intractable problem. Each point defines the center of an octahedral volume of space, and by repeatedly slicing each volume using the others' boundaries, you can partition the entire space into something like O(N^3) disjoint pieces. You can then enumerate these pieces to determine which one is contained in the largest number of octahedra. But actually implementing this is tricky; each piece ends up having an irregular polyhedral shape, and calculating the geometry of their boundaries would be non-trivial.
Instead, some of the participants noticed out that you could represent the constraints as a formula:
and then just feed it to a SAT/SMT solver such as Z3. This is probably less computationally efficient, but in practice it runs reasonably quickly, and it's vastly easier to code. (The Advent of Code scoring system is based almost entirely on the time taken to come up with a correct solution, so it strongly favors solutions that are quick to implement.)
In last year's Advent of Code programming contest, one of the trickier problems involved taking a collection of points in 3D space, each of which has a "range" defined by Manhattan distance, and finding the location that is "in range" of the maximum number of them.
Now, this isn't a theoretically intractable problem. Each point defines the center of an octahedral volume of space, and by repeatedly slicing each volume using the others' boundaries, you can partition the entire space into something like O(N^3) disjoint pieces. You can then enumerate these pieces to determine which one is contained in the largest number of octahedra. But actually implementing this is tricky; each piece ends up having an irregular polyhedral shape, and calculating the geometry of their boundaries would be non-trivial.
Instead, some of the participants noticed out that you could represent the constraints as a formula:
and then just feed it to a SAT/SMT solver such as Z3. This is probably less computationally efficient, but in practice it runs reasonably quickly, and it's vastly easier to code. (The Advent of Code scoring system is based almost entirely on the time taken to come up with a correct solution, so it strongly favors solutions that are quick to implement.)Here's one such solution: https://www.reddit.com/r/adventofcode/comments/a8s17l/2018_d...