[Math][Python][Z3] Wood workshop, linear programming and Leonid Kantorovich

Let's say, you work at wood workshop. You have a supply of rectangular wood workpieces, 6*13 inches, or meters, or whatever unit you use:

Workpiece (6*13 inches):

.............
.............
.............
.............
.............
.............

You need to produce 800 rectangles of 4*5 size:

Output A (4*5, we need 800 of these):

.....
.....
.....
.....

... and 400 rectangles of 2*3 size:

Output B (2*3, we need 400 of these):

...
...

To cut a piece as A/B rectangles, you can cut a 6*13 workpiece in 4 ways. Or, to put it in another way, you can place A/B rectangles on 6*13 rectanlge in 4 ways:

Cut A (Output A: 3, Output B: 1):

--------444--
11112222444--
1111222233333
1111222233333
1111222233333
1111222233333

Cut B (Output A: 2, Output B: 6):

333444555666-
333444555666-
1111122222777
1111122222777
1111122222888
1111122222888

Cut C (Output A: 1, Output B: 9):

----222555888
1111222555888
1111333666999
1111333666999
1111444777000
1111444777000

Cut D (Output A: 0, Output B: 13):

1133557799bbb
1133557799bbb
1133557799ccc
22446688aaccc
22446688aaddd
22446688aaddd

Now the problem. Which cuts are most efficient? You want to consume as little workpieces as possible.

This is optimization problem and I can solve it this with Z3:

from z3 import *

s=Optimize()

workpieces_total=Int('workpieces_total')
cut_A, cut_B, cut_C, cut_D=Ints('cut_A cut_B cut_C cut_D')
out_A, out_B=Ints('out_A out_B')

s.add(workpieces_total==cut_A+cut_B+cut_C+cut_D)

s.add(cut_A>=0)
s.add(cut_B>=0)
s.add(cut_C>=0)
s.add(cut_D>=0)

s.add(out_A==cut_A*3 + cut_B*2 + cut_C*1)
s.add(out_B==cut_A*1 + cut_B*6 + cut_C*9 + cut_D*13)

s.add(out_A==800)
s.add(out_B==400)

s.minimize(workpieces_total)

print s.check()
print s.model()

sat
[cut_B = 25,
 cut_D = 0,
 cut_A = 250,
 out_B = 400,
 out_A = 800,
 workpieces_total = 275,
 cut_C = 0]

So you need to cut 250 workpieces in A's way and 25 pieces in B's way, this is the most optimal way.

Also, the problem is small enough to be solved by my toy bit-blaster MK85, thanks to Open-WBO MaxSAT solver:

(declare-fun workpieces_total () (_ BitVec 16))
(declare-fun cut_A () (_ BitVec 16))
(declare-fun cut_B () (_ BitVec 16))
(declare-fun cut_C () (_ BitVec 16))
(declare-fun cut_D () (_ BitVec 16))
(declare-fun out_A () (_ BitVec 16))
(declare-fun out_B () (_ BitVec 16))

(assert (bvuge cut_A (_ bv0 16)))
(assert (bvuge cut_B (_ bv0 16)))
(assert (bvuge cut_C (_ bv0 16)))
(assert (bvuge cut_D (_ bv0 16)))

(assert (bvuge out_A (_ bv800 16)))
(assert (bvuge out_B (_ bv400 16)))

(assert (= workpieces_total (bvadd cut_A cut_B cut_C cut_D)))

(assert (= out_A (bvadd
		(bvmul_no_overflow cut_A (_ bv3 16))
		(bvmul_no_overflow cut_B (_ bv2 16))
		cut_C
		)
	)
)

(assert (= out_B (bvadd
		cut_A
		(bvmul_no_overflow cut_B (_ bv6 16))
		(bvmul_no_overflow cut_C (_ bv9 16))
		(bvmul_no_overflow cut_D (_ bv13 16))
		)
	)
)

(minimize workpieces_total)

(check-sat)
(get-model)

The result:

sat
(model
	(define-fun cut_A () (_ BitVec 16) (_ bv250 16)) ; 0xfa
	(define-fun cut_B () (_ BitVec 16) (_ bv25 16)) ; 0x19
	(define-fun cut_C () (_ BitVec 16) (_ bv0 16)) ; 0x0
	(define-fun cut_D () (_ BitVec 16) (_ bv0 16)) ; 0x0
	(define-fun out_A () (_ BitVec 16) (_ bv800 16)) ; 0x320
	(define-fun out_B () (_ BitVec 16) (_ bv400 16)) ; 0x190
	(define-fun workpieces_total () (_ BitVec 16) (_ bv275 16)) ; 0x113
)

The task I solved I've found in Leonid Kantorovich's book "The Best Uses of Economic Resources" (1959). And these are 5 pages with the task and solution (in Russian).

Leonid Kantorovich was indeed consulting plywood factory in 1939 about optimal use of materials. And this is how linear programming (LP) and integer linear programming (ILP) has emerged.


→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.