有沒有辦法在C＃中使用Z3求解器的最大化/最小化目標？

Question

我正在尋找一種方法來使用.NET API將最小化/最大化目標添加到Z3解算器。有什麼辦法嗎？

感謝您的幫助和聖誕快樂:-)

Answer 1

您可以使用該方法MkOptimize從上下文對象來創建一個優化的對象。然後，您可以將約束和目標函數添加到此對象。該文件包含Optimize.cs這些方法：https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/Optimize.cs

上就http://lonelypad.blogspot.dk/2014/08/f-and-linear-programming-introduction.html使用從F＃的API（它使用相同的.NET API，作爲C＃）的教程。它從http://rise4fun.com/Z3Opt/tutorial/guide連接。