I suggest "Programming Languages: Application and Interpretation", available free here: http://cs.brown.edu/courses/cs173/2012/book/ It's an undergraduate-level programming languages class textbook.
Other books burn a lot of time on things like lexing and parsing; this one does not. In the lisp tradition, it assumes s-expressions and gets to the juicy bits of programming language semantics immediately: lexical scope, first class functions, objects, etc.
SMT solvers excel at solving finite sets of equations involving finite or atomic data, like numbers, bitvectors, strings, and arrays of fixed length. They've been very successfully applied in software and hardware verification. They're also the essential tool for a big category of approaches to program synthesis.
This has some overlap with the sorts of numeric constraint solving available in prolog and with non-recursive prolog goals. Prolog however can express turing-complete computation with recursive goals, dynamically allocate data structures of unknown size, etc. that SMT cannot easily encode.
Z3 also has support for datalog-like queries. I don't know much about datalog, but my understanding is that it supports a more limited set of queries than prolog but can solve them more efficiently with a totally different algorithm than prolog's goal-directed depth first search.
Other search algorithms can take up lots of memory to store progress they've made down different paths. Having only one active state also lets you map unification down to efficient low level cpu operations. If you have multiple states, you either have to copy lots of data when you fork the state or you use a persistent data structure but can't use side effects, so everything is a bit slower.
It's a tradeoff though. I work on miniKanren, which is a logic programming language with a complete search that doesn't hit the nontermination issues you mention. The complete search lets us do some pretty cool stuff with program synthesis (though we're not about to put any programmers out of business just yet): https://www.youtube.com/watch?v=er_lLvkklsk
Note that you can implement iterative deepening depth first search on top of prolog if you want a complete search there. Iterative deepening takes a little more time but avoids the memory problems with breath-first. SWI has tools built in to help there: http://www.swi-prolog.org/pldoc/doc_for?object=call_with_dep...
And I believe Ciao implements its iterative deepening library with a meta-interpreter: https://ciao-lang.org/docs/ciao/id_doc.html#0
When I've talked to senior researchers about these problems, they say that they have no problem finding distilled information about new results; they get it from in-person conversations at conferences that they attend frequently. The publishing of distilled research would most benefit low-status, newer researchers (like Ph.D. students), but it needs to be valued by senior researchers to make it into the incentive systems of hiring and grant funding. It seems like a tricky problem to fix the incentives here.
First, a small defense of Racket. Racket has a small core relative to its apparent size; most of the bloat is in optional library code. All the fancy special forms for pattern matching, classes, contracts, etc are just optional macros from the libraries, and everything eventually expands down into this rather small core language:
The default `#lang racket` is a big batteries-included language including all that stuff, but the core `#lang racket/base` isn't very big. I always program in `#lang racket/base` and pull in just the libraries I need. For me the most beautiful part of Racket is this juxtaposition of a small core language and a big extended language implemented through a standard library of macros.
You can also install a distribution of Racket that leaves out bloat like DrRacket, Slideshow and the teaching language packages from the release variants page: https://download.racket-lang.org/releases/6.8/
As to your question, Beautiful Racket appears largely a guide to the language extensibility features that are specific to Racket and not shared by other Scheme systems like Chibi. Things like the `#lang` system, lexer library, and syntax highlighting integration in DrRacket. I imagine you'd get the most benefit out of it by working through it in Racket, and subsequently thinking about how to apply the ideas in other systems like Chibi.