[prev in list] [next in list] [prev in thread] [next in thread] 

List:       boost
Subject:    [boost] Boost Solvers Library
From:       Pascal Kesseli via Boost <boost () lists ! boost ! org>
Date:       2023-09-03 15:32:40
Message-ID: DB9P194MB1450EF9F0E6D4D920849AE45C2EAA () DB9P194MB1450 ! EURP194 ! PROD ! OUTLOOK ! COM
[Download RAW message or body]

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,

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost


[prev in list] [next in list] [prev in thread] [next in thread]