Blocked clause decomposition is implemented in, I think, two SAT preprocessors in SAT solvers, both are C++. There are about three to five different articles on

Blocked clause decomposition is implemented in, I think, two SAT preprocessors in SAT solvers, both are C++. There are about three to five different articles on the topic. For LLM to implement BCD in Haskell it needs to be able to translate between Haskell and C++ and it is well beyond trivial.