You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
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.
Motivation: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7197060/
This is also something I would be interested in developing.
References
Beta Was this translation helpful? Give feedback.
All reactions