Optimization Modulo Theory (OMT) extends Satisfiability Modulo Theories (SMT) by incorporating optimization objectives.
- Z3
- CVC5
- Yices-QS
- Bitwuzla
- The OBV-BS algorithm
- The FM algorithm
- The RC2 algorithm
- Off-the-shelf MaxSAT solvers
https://github.com/FlorentAvellaneda/EvalMaxSAT
- Linear search
- Binary search
Exiting OMT solvers?
- Z3 (to MaxSAT?)
- OptiMathSAT
- ...
Improvements to the OBV-BS algorithm
- Variable Polarity Setting: prefer 1 over 0 during the search?
The relevant API (NOTE: some SAT solvers in pysat do not support this API)
def set_phases(self, literals=[]):
"""
Sets polarities of a given list of variables.
"""
TBD: to see how to use this API...
- Sebastiani, R., & Tomasi, S. (2015). Optimization in SMT with LA(Q) cost functions. In International Conference on Principles and Practice of Constraint Programming (pp. 484-498). Springer, Cham.
- Bjørner, N., Phan, A. D., & Fleckenstein, L. (2015). νZ-an optimizing SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 194-199). Springer, Berlin, Heidelberg.
- Martins, R., Manquinho, V. M., & Lynce, I. (2014). Open-WBO: A modular MaxSAT solver. In International Conference on Theory and Applications of Satisfiability Testing (pp. 438-445). Springer, Cham.