(120f) Integrating Mixed-Integer Optimisation and Satisfiability Modulo Theories
Hybrid optimisation/logic approaches have been developed combining mixed-integer linear programming (MILP) and constraint programming (CP) [3, 4, 5]. The hybrid formulations usually use logic-based Benders decomposition (LBBD) , a generalisation of Benders decomposition . The principles of Benders decomposition remain: we have a master problem and a subproblem which generates cuts if the solution from the master problem is infeasible. Differently from classical Benders decomposition, LBBD requires a logic proof deriving an objective bound.
But CP requires specialised, bespoke constraints. We consider modifying the hybrid method by replacing CP with satisfiability modulo theories (SMT). SMT is a constraint satisfaction technique combining propositional satisfiability with a background theory . A background theory is a set of axioms and symbols, e.g. the theory of arithmetic. An SMT solver consists of a satisfiability solver and a theory solver. The idea is to leverage the strength and robustness of modern satisfiability solvers to search for a feasible solution. The modelling framework exposed by SMT allows for Boolean variables to be used with background theory variables, e.g z â (x â¥ 0) where x is continuous and z is Boolean, so SMT is a natural choice when logical decisions form a part of the system being modelled.
For a test set of 335 scheduling problems, we computationally compare pure CP, MILP, and SMT approaches to LBBD methods combining (i) MILP/CP and (ii) MILP/SMT. We find that the MILP/CP and MILP/SMT logic-based Benders decomposition approaches work very well on a minimum cost model for scheduling and perform significantly better than any of CP, MILP, or SMT alone. But the hybrid MILP/CP and MILP/SMT methods are weaker than CP, MILP, SMT on a minimum makespan model.
We further discuss the computational and modelling trade-offs between CP and SMT. In particular, we show how logic-based modelling can be used to manage symmetry and degeneracy in applications such as bin packing and scheduling. Our work is supported by extensive computational testing on large-scale instances.
- Maravelias, C. T. and Sung, C. (2009). Integration of production planning and scheduling: Overview, challenges and opportunities. Comput Chem Eng, 33(12):1919 â 1930.
- Hooker, J. N. and Ottoson, G. (2003). Logic-based Benders decomposition. Math Progam, 96(1):33â60.
- Jain, V. and Grossmann, I. E. (2001). Algorithms for Hybrid MILP/CP Models for a Class of Optimization Problems. INFORMS J Comput, 13(4):258â276.
- Li, H. and Womer, K. (2008). Scheduling projects with multi-skilled personnel by a hybrid MILP/CP Benders decomposition algorithm. J Sched, 12(3):281â298.
- Sitek, P. (2014). A hybrid CP/MP approach to supply chain modelling, optimization and analysis. In Computer Science and Information Systems (FedCSIS), pages 1345â1352.
- Benders, J. F. (1962). Partitioning procedures for solving mixed-variables programming problems. Numerische Mathematik, 4(1):238â252.
- De Moura, L. and BjÃ¸rner, N. (2008). Z3: An Efficient SMT Solver, pages 337â340. Springer.
- Hooker, J. N. (2007). Planning and scheduling by logic-based Benders decomposition. Oper Res, 55(3):588â602.