Support for SMT Solver Backends in PuLP

[EthanJamesLew]

PuLP is a powerful Python library for optimization problems, but some users also use it for satisfiability problems, which have constraints but no objective function. In such cases, Satisfiability Modulo Theories (SMT) solvers like Z3 and CVC4 have demonstrated substantial performance improvements over ILP solvers. This community idea proposes adding support for SMT solver backends in PuLP to enhance its functionality for users dealing with satisfiability problems.

• Improved performance: Users can leverage the capabilities of SMT solvers to solve satisfiability problems more efficiently, which can lead to substantial performance improvements.
• Better user experience: With SMT solver support, users can seamlessly switch between optimization and satisfiability problem modes within PuLP, without having to switch to a different tool or library.

Motivation: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7197060/

This is also something I would be interested in developing.

References

Brown, H., Zuo, L., & Gusfield, D. (2020, April). Comparing integer linear programming to SAT-solving for hard problems in computational and systems biology. In Algorithms for Computational Biology: 7th International Conference, AlCoB 2020, Missoula, MT, USA, April 13–15, 2020, Proceedings (pp. 63-76). Cham: Springer International Publishing.