2017-09-11 11 views
0

Z3を使用してジョブショップスケジューリングの問題をモデル化しようとしています。具体的には、それぞれに他のタスクの依存関係があるかもしれない一連のタスクがあるとしましょう。次に、最後のタスク、つまりメイクパンをスケジューリングする時間を最小限に抑えたいと考えています。Z3を使用してスケジューリング問題のメイパンを最小化する

他のジョブに依存しますが、フォワード依存関係がないジョブが複数ある可能性があります(つまり、ジョブはこのジョブに依存しません).Z3の単純な最小操作では不十分な場合があります。そして、Z3はリスト上の最大関数を認めません。

これを解決するために、私はすべてのそのようなジョブに依存する偽のジョブを追加し、このジョブのスケジューリングの時間を最小化することを検討しています。私は多くの仕事に制約を加える必要があるので、このアプローチがスケーラブルであるかどうか疑問です。

これは唯一のアプローチですか、それとも他のよりエレガントな手段ですか?

+1

解決しようとしている問題の具体例を追加できますか?特に、照会時に認識されているジョブの数は? –

答えて

0

maxを定義するには、iteというチェーンを使用します。正確にいくつの仕事があるかをあなたが知っていると仮定します。ここをクリックしてください:Use Z3 and SMT-LIB to get a maximum of two values

関連する問題