In the course of my research in static program analysis, I have been a contributor to the Bounded Model Checker for C (CBMC - https://github.com/diffblue/cbmc) for quite some time now. Projects like these map static analysis problems to a variety of back-end solvers like SAT, SMT, QBF, etc. What always surprised me is how often tools like CBMC have to come up with an intermediate C++ layer for the various back-end solvers like MiniSAT or Glucose (see https://github.com/diffblue/cbmc/tree/develop/src/solvers/sat). For this reason I am considering to create a unified C++ wrapper for these different solvers, with an initial focus on SAT. I intend to include a naive default DPLL implementation, but the real value for such a library would stem from making the aforementioned third party engines easily accessible. I was wondering whether this would be a fit for a Boost library, but I am uncertain whether: A) There is even interest in the community for this or B) The scope of the library with inherent dependencies on external SAT solvers fits the Boost format Thus I thought I'd drop this message in the mailing list to ask what people think. Thanks,