Python - Tối ưu hóa hệ thống bất bình đẳng

Question

Tôi đang làm việc trên một chương trình bằng Python, trong đó một phần nhỏ liên quan đến việc tối ưu hóa một hệ phương trình/bất đẳng thức. Lý tưởng nhất, tôi sẽ muốn làm như có thể được thực hiện trong Modelica, viết ra các phương trình và để cho người giải quyết chăm sóc nó.

Hoạt động của trình giải quyết và lập trình tuyến tính là một chút ngoài vùng thoải mái của tôi, nhưng tôi vẫn quyết định thử. Vấn đề là thiết kế chung của chương trình là hướng đối tượng và có nhiều khả năng kết hợp khác nhau để tạo thành các phương trình, cũng như một số phi tuyến tính, vì vậy tôi không thể dịch nó thành một chương trình tuyến tính vấn đề (nhưng tôi có thể sai).

Sau một số nghiên cứu tôi thấy rằng trình giải mã Z3 dường như làm những gì tôi muốn. Tôi đến với điều này (điều này trông giống như một trường hợp điển hình về những gì tôi muốn tối ưu hóa):

from z3 import * 

a = Real('a') 
b = Real('b') 
c = Real('c') 
d = Real('d') 
e = Real('e') 
g = Real('g') 
f = Real('f') 
cost = Real('cost') 

opt = Optimize() 
opt.add(a + b - 350 == 0) 
opt.add(a - g == 0) 
opt.add(c - 400 == 0) 
opt.add(b - d * 0.45 == 0) 
opt.add(c - f - e - d == 0) 
opt.add(d <= 250) 
opt.add(e <= 250) 

opt.add(cost == If(f > 0, f * 50, f * 0.4) + e * 40 + d * 20 + 
    If(g > 0, g * 50, g * 0.54)) 

h = opt.minimize(cost) 
opt.check() 
opt.lower(h) 
opt.model() 

Bây giờ công trình này, và mang lại cho tôi kết quả tôi muốn, mặc dù nó không phải là cực kỳ nhanh (tôi cần phải giải quyết các hệ thống như vậy vài nghìn lần). Nhưng tôi không chắc tôi đang sử dụng đúng công cụ cho công việc (Z3 là một "định lý prover").

API về cơ bản là chính xác những gì tôi cần, nhưng tôi sẽ tò mò nếu các gói khác cho phép một cú pháp tương tự. Hoặc tôi có nên cố gắng xây dựng vấn đề theo một cách khác để cho phép tiếp cận LP chuẩn không? (mặc dù tôi không biết làm thế nào)

Answer 1

Z3 là bộ giải mạnh nhất mà tôi đã tìm thấy cho các hệ phương trình linh hoạt như vậy. Z3 là một sự lựa chọn tuyệt vời ngay bây giờ mà nó được phát hành theo giấy phép MIT.

Có rất nhiều loại công cụ khác nhau với các trường hợp sử dụng chồng chéo. Bạn đã đề cập đến lập trình tuyến tính - cũng có các provers định lý, bộ giải quyết SMT và nhiều loại công cụ khác. Mặc dù tiếp thị chính nó như là một định lý prover, Z3 thường được bán trên thị trường như là một người giải quyết SMT. Hiện tại, những người giải quyết SMT đang dẫn đầu gói giải pháp linh hoạt và tự động của các phương trình đại số và bất đẳng thức cùng với các boolean, reals và integers, và trong thế giới của những người giải quyết SMT, Z3 là vua. Hãy xem the results of the last SMT comp if you want evidence of this. Điều đó đang được nói, nếu phương trình của bạn là tất cả tuyến tính, sau đó bạn cũng có thể tìm thấy hiệu suất tốt hơn với CVC4. Nó không đau để mua sắm xung quanh.

Nếu phương trình của bạn có dạng kiểm soát rất cao (ví dụ, giảm thiểu một số hàm theo một số ràng buộc) thì bạn có thể có hiệu suất tốt hơn bằng cách sử dụng thư viện số như GSL hoặc NAG. Tuy nhiên, nếu bạn thực sự cần sự linh hoạt, thì tôi nghi ngờ bạn sẽ tìm thấy một công cụ tốt hơn Z3.

Answer 2

Giải pháp tốt nhất có thể là sử dụng bộ giải ILP. Vấn đề của bạn có thể được xây dựng như một thể hiện lập trình tuyến tính số nguyên (ILP). Có rất nhiều giải pháp ILP, và một số có thể hoạt động tốt hơn Z3. Đối với chỉ có 7 biến, bất kỳ giải pháp ILP phong nha nên tìm một giải pháp rất nhanh chóng.

Bit khó hiểu duy nhất là các biểu thức có điều kiện (If(...)). Tuy nhiên, như @Erwin Kalvelagen suggests, các điều kiện có thể được xử lý bằng cách sử dụng chia tách. Ví dụ: giới thiệu các biến số fplus và fminus, với các ràng buộc f = fplus - fminus và fplus >= 0 và fminus >= 0. Bây giờ bạn có thể thay thế If(f > 0, f * 50, f * 0.4) bằng 50 * fplus - 0.4 * fminus. Trong trường hợp này, điều đó sẽ tương đương.

Tách biến không phải lúc nào cũng hoạt động. Bạn phải suy nghĩ về việc liệu nó có thể giới thiệu các giải pháp giả hay không (trong đó cả hai số fplus > 0 và fminus > 0). Tuy nhiên, trong trường hợp này, các giải pháp giả mạo sẽ không bao giờ tối ưu - người ta có thể cho thấy rằng giải pháp tối ưu sẽ không bao giờ tối ưu.Do đó, chia tách hoạt động tốt ở đây.

Nếu bạn có một tình huống mà bạn có câu lệnh có điều kiện nhưng phân tách biến không hoạt động, bạn thường có thể sử dụng các kỹ thuật tại https://cs.stackexchange.com/q/12102/755 để xây dựng vấn đề dưới dạng thể hiện của ILP.