Building automated reasoners from smaller building blocks is harder than in the case of conventional software because any modular development technique has to be worked out at a model-theoretic level first. In the case of constraint solvers, since each solver decides satisfiability with respect to a specific constraint theory, to combine solvers first of all means to combine their theories.
The known methods in the field have been essentially limited to component procedures whose underlying theories are disjoint. Using a novel model-theoretic approach, I have instead developed a general combination framework which includes several of the known combination results and methods and extends them significantly to the case of non-disjoint component theories.
This dissertation originated from the work I did for my Master's thesis, where I integrated a well-know combination procedure by Nelson and Oppen into the Constrain Logic Programming scheme by Jaffar and Lassez. Part of the work of the dissertation was carried over in the context of two parallel collaborations with Franz Baader of the Technical University of Aachen, Germany, and Christophe Ringeissen of CNRS/INRIA, France. The work with them is described in a number of technical reports and refereed publications. See my publications page for more details and online versions of the papers.