  Finding solution values for unknowns in Boolean equations was a principal
reasoning mode in the Algebra of Logic of the 19th century. Schr\"oder
investigated it as "Aufl\"osungsproblem" ("solution problem"). It is closely
related to the modern notion of Boolean unification. Today it is commonly
presented in an algebraic setting, but seems potentially useful also in
knowledge representation based on predicate logic. We show that it can be
modeled on the basis of first-order logic extended by second-order
quantification. A wealth of classical results transfers, foundations for
algorithms unfold, and connections with second-order quantifier elimination and
Craig interpolation show up. Although for first-order inputs the set of
solutions is recursively enumerable, the development of constructive methods
remains a challenge. We identify some cases that allow constructions, most of
them based on Craig interpolation, and show a method to take vocabulary
restrictions on solution components into account.
