# 3. Wood workshop, linear programming and Leonid Kantorovich
Vấn đề đặt ra như sau: Giả sử, bạn làm việc cho một xưởng gỗ, bạn có nguồn cung cấp phôi gỗ hình chữ nhật, 6\*13 inch hoặc mét hoặc bất kỳ đơn vị nào bạn sử dụng.
Một phôi (hay còn khối gỗ) 6\*13:
Bạn muốn tạo 800 hình chữ nhật có kích thước 4\*5 và 400 hình chữ nhật kích thước 2\*3:
Để cắt một mảnh dưới dạng hình chữ nhật A/B, bạn có thể cắt phôi 6\*13 theo 4 cách. Hay nói cách khác bạn có thể đặt hình chữ nhật A/B trên hình chữ nhật 6\*13 theo 4 cách:
Bây giờ vấn đề là cắt giảm nào là hiệu quả nhất? Làm sao để sử dụng số lượng phôi ít nhất càng tốt.
Đây là vấn đề tối ưu hóa và tôi có thể giải quyết nó bằng z3:
{% code overflow="wrap" %}
```python
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) # tổng các cách cắt là tổng phôi cần tìm
s.add(cut_A >=0) # điều kiện tiên quyết
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) # mỗi cách sẽ ra số lượng kích A/B khác nhau thì tổng lại phải thỏa mãn yêu cầu
s.add(out_B==cut_A*1 + cut_B*6 + cut_C*9 + cut_D*13)
s.add(out_A==800) # set điều kiện output
s.add(out_B==400)
s.minimize(workpieces_total) #ép điều kiện để workpieces nhỏ nhất.
print (s.check())
print (s.model())
```
{% endcode %}
Kết quả:
```
sat
[cut_B = 25,
cut_D = 0,
cut_A = 250,
out_B = 400,
out_A = 800,
workpieces_total = 275,
cut_C = 0]
```
Vậy là ta cần tối thiểu là 275 phôi kích thước 6\*13 để được cắt thành 800 tấm hình chữ kích thước 4\*5 và 400 tấm hình chữ nhật kích thước 2\*3.
Nếu sử dụng SMT-LIB 2.x thì ta chỉ cần lưu ý một số câu lệnh sau:
```
(bvuge ... ()) ; uge là until greater equal
(bvmul_no_overflow ... ()) ; nó là nhân nhưng không bị lỗi tràn bộ nhớ
(minimize ...) ; là tìm giá trị nhỏ nhất của cái gì đó
```
---
# Agent Instructions: Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter:
```
GET https://viettaliii.gitbook.io/home/education/reverse-engineering/symbolic-analysis/sat-smt-by-example/equations/3.-wood-workshop-linear-programming-and-leonid-kantorovich.md?ask=
```
The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.