sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Documentation.SBV.Examples.Optimization.Production

Description

Solves a simple linear optimization problem

Synopsis

# Documentation

A company makes two products (X and Y) using two machines (A and B).

• Each unit of X that is produced requires 50 minutes processing time on machine A and 30 minutes processing time on machine B.
• Each unit of Y that is produced requires 24 minutes processing time on machine A and 33 minutes processing time on machine B.
• At the start of the current week there are 30 units of X and 90 units of Y in stock. Available processing time on machine A is forecast to be 40 hours and on machine B is forecast to be 35 hours.
• The demand for X in the current week is forecast to be 75 units and for Y is forecast to be 95 units.
• Company policy is to maximise the combined sum of the units of X and the units of Y in stock at the end of the week.

How much of each product should we make in the current week?

We have:

>>> optimize Lexicographic production
Optimal model:
X     = 45 :: Integer
Y     =  6 :: Integer
stock =  1 :: Integer


That is, we should produce 45 X's and 6 Y's, with the final maximum stock of just 1 expected!