Art of Computer Programming Fascicle 5 and Fascicle 6. Maybe Volume 4A (aka: Fascicles 1 through 4), but Volume 4A is more about "regular" combinatorics (grey code, LSFRs, etc. etc.) which don't need a complicated solver. Still, having Volume 4A as reference material is useful when reading Fascicle 5 and 6 (since combinations / permutations / partitions / trees / graphs come up with regularity in Fascicle 5 and 6).
Fascicle 5 discusses "backtrack programming", and has some practical applications of that. Yeah yeah, you get N-Queens (probably no practical application), but also comma-free codes (obvious applications to communications / framing). Overall, Fascicle 5 builds up to the covering problem (https://en.wikipedia.org/wiki/Covering_problems) and practical applications of "covering problems with color" (a new category of problems proposed by Knuth: combining coloring problems and covering problems in one specification. Because his "Dancing Links + Algorithm X" seems to solve covering problems with color very efficiently).
Volume 4A (which contains what was formerly known as Fascicles 1 through 4) contains a huge chapter on bitwise hacks. Which while solved in Volume 4A, "could be solved" with an SMT / SAT solver like Z3.
Fascicle 6 is Knuth's dedicated section on SAT solvers. Its on my todo list... I haven't really done much with the book yet. I'll probably get to it after I finish Fascicle 5 (which seems more applicable to what I'm trying to do)
--------
All of these "puzzles" are probably NP complete, and therefore "translate" to each other very easily. Covering problems are provably NP complete for example: and therefore can be solved with backtracking (aka: Dancing Links on Algorithm X), or an SAT solver like Z3.
SAT specifications (which Z3 solves directly) can also be converted into a covering problem, and therefore solved with Dancing Links / Algorithm X.
Having both techniques "in your pocket" so that you can pick-and-choose the right solver for the right problem (or maybe through the use of experimentation) is probably best. Unless someone solves P =/= NP any time soon, this ad-hoc methodology of "trying different techniques until something works" is our best bet at practically solving "puzzles" like traveling salesman (aka: airline travel), covering problems (aka: scheduling), integer optimization / functional equivalency of bitwise hacks (probably used in theorem proving / Verilog synthesis of circuits) or whatever else pops up in the real world.
--------------
A lot of these SAT / Backtracking problems are over graphs. Practical applications, like graph drawings (think the "dot" program: how to arrange a graph if it is planar... or if it is non-planar, how to arrange the graph such that it has the fewest number of crossings) is a combinatorics problem. So applications pop up in very unusual places: I'd argue that graph layout is a UI problem for example (a planar graph is easier to comprehend: or at least a graph with the fewest number of crossings)
--------
A lot of these problems can be solved with "less powerful" techniques: maximum flow is itself a solved problem for example with numerous applications. Maximum-flow is "less than NP-complete" problem, but one that you might reach for Z3 unnecessarily.
Similarly: planar graph checking is solved and "less than NP-complete" IIRC. But you'll only really know that if you spend a lot of time researching graph theory.
You really want to use Z3 if you have suspicions that your problem is truly NP complete (or if you suspect is NP complete), and that the exhaustive search of all possibilities is your only option. Z3 is then useful because people have worked very, very, very hard on discovering "less-than NP complete" optimizations to subproblems, and can automatically solve these subproblems efficiently.