Boost Solvers Library

From: Pascal Kesseli (pascal_kesseli_at_[hidden])
Date: 2023-09-03 15:32:40

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,