(120f) Integrating Mixed-Integer Optimisation and Satisfiability Modulo Theories

A major challenge in process systems engineering is integrating: (i) long-term strategic planning decisions, (ii) medium-term tactical planning, and (iii) short-term scheduling [1]. One way to address these multi-scale optimisation problems is by integrating logic and optimisation [2]. For example, a scheduling problem may have two levels: (i) assigning orders to machines and (ii) sequencing orders on each machine [3]. In a minimum cost model, assigning orders to machines is a mixed-integer optimisation problem, sequencing orders is a constraint satisfaction problem. The entire problem may be reformulated as either an optimisation or logic problem, but this misses the chance to use optimisation and logic synergistically.

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) [2], a generalisation of Benders decomposition [6]. 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 [7]. 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.

References

1. Maravelias, C. T. and Sung, C. (2009). Integration of production planning and scheduling: Overview, challenges and opportunities. Comput Chem Eng, 33(12):1919 – 1930.
2. Hooker, J. N. and Ottoson, G. (2003). Logic-based Benders decomposition. Math Progam, 96(1):33–60.
3. 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.
4. 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.
5. 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.
6. Benders, J. F. (1962). Partitioning procedures for solving mixed-variables programming problems. Numerische Mathematik, 4(1):238–252.
7. De Moura, L. and Bjørner, N. (2008). Z3: An Efficient SMT Solver, pages 337–340. Springer.
8. Hooker, J. N. (2007). Planning and scheduling by logic-based Benders decomposition. Oper Res, 55(3):588–602.