From 2b2c076fbcebcfe825fccb9e4cb53e4ef4d8a970 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=D0=9A=D0=B8=D1=81=D0=B5=D0=BB=D1=91=D0=B2=20=D0=92=D0=BB?= =?UTF-8?q?=D0=B0=D0=B4=D0=B8=D1=81=D0=BB=D0=B0=D0=B2?= Date: Sun, 3 Feb 2019 18:49:52 +0300 Subject: [PATCH] =?UTF-8?q?refactoring=20=D0=B8=20=D0=BE=D0=B3=D1=80=D0=B0?= =?UTF-8?q?=D0=BD=D0=B8=D1=87=D0=B5=D0=BD=D0=B8=D1=8F=20=D0=BD=D0=B0=20?= =?UTF-8?q?=D1=82=D0=B8=D0=BF=D0=B8=D0=B7=D0=B8=D1=80=D0=BE=D0=B2=D0=B0?= =?UTF-8?q?=D0=BD=D0=BD=D1=8B=D0=B9=20=D1=81=D0=BB=D1=83=D1=87=D0=B0=D0=B9?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/constraints/conversion_2.mzn | 336 ++++++++++++++++++++----------- src/inport/Testing.java | 2 +- 2 files changed, 219 insertions(+), 119 deletions(-) diff --git a/src/constraints/conversion_2.mzn b/src/constraints/conversion_2.mzn index 666436b..71ad496 100644 --- a/src/constraints/conversion_2.mzn +++ b/src/constraints/conversion_2.mzn @@ -13,7 +13,10 @@ int : moving_op_of_obj_max_size; array [1..n_moving_obj] of 0..moving_op_of_obj_max_size : moving_op_of_obj_sizes; array [1..n_moving_obj, 1..moving_op_of_obj_max_size] of 1..n_operations : moving_op_of_obj; % Операции перемещения затрагивающие данный объект. -array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..moving_op_of_obj_max_size : current_moving_operation; % Текущая операция операция перемещения, в которой задействован данный объект. +% Определение current_moving_operation. + % Текущая операция операция перемещения, в которой задействован данный объект. + array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..moving_op_of_obj_max_size : current_moving_operation; + % Текущая операция лежит в множестве тех, которые затрагивают данный объект. constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( current_moving_operation[obj, t] <= moving_op_of_obj_sizes[obj] @@ -30,7 +33,10 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..moving_op_of_obj_max_siz (exists (op_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, op_no], t])) ); -array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement_before_start; % Находится ли объект в движении перед началом интервала. +% Определение is_m_obj_in_movement_before_start. + % Находится ли объект в движении перед началом интервала. + array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement_before_start; + % В начале никто не движется. constraint forall (obj in 1..n_moving_obj) (not is_m_obj_in_movement_before_start[obj, 0]); % Перед первым интервалом все тоже стоят на месте. @@ -47,8 +53,9 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement array [1..n_operations] of 1..n_locations : operations_destination; % Локация в которой окажется объект после завершения операции. -% Теперь m_obj_loc означает где объект стоит или куда он движется перед началом определённого интервала. -array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; % Moving object location. +% Определение m_obj_loc. + % Местоположение объекта или пункт назначения (если объект движется) перед началом определённого интервала. + array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; % За фиктивный нулевой интервал объект не успевает ничего сделать с начальным положением. constraint forall (obj in 1..n_moving_obj) ( m_obj_loc[obj, 1] = m_obj_loc[obj, 0] @@ -65,139 +72,232 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; ); % Начальное состояние. -array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc; -constraint forall (i in 1..n_moving_obj) (m_obj_loc[i, 0] = initial_m_obj_loc[i]); + array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc; + constraint forall (i in 1..n_moving_obj) (m_obj_loc[i, 0] = initial_m_obj_loc[i]); % Конечное состояние. -array [1..n_moving_obj] of var 0..n_locations : final_m_obj_loc; -constraint forall (i in 1..n_moving_obj) ( - (final_m_obj_loc[i] != 0) -> - (m_obj_loc[i, n_intervals + 1] = final_m_obj_loc[i]) -); - -constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); % Краевые значения. + array [1..n_moving_obj] of var 0..n_locations : final_m_obj_loc; + constraint forall (i in 1..n_moving_obj) ( + (final_m_obj_loc[i] != 0) -> + (m_obj_loc[i, n_intervals + 1] = final_m_obj_loc[i]) + ); -% Определение op_start и op_fin. -constraint forall (op in 1..n_operations, j in {0, n_intervals + 1}) - (op_start[op, j] = false /\ op_fin[op, j] = false); -constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = (op_status[i, j] /\ not op_status[i, j - 1])); -constraint forall (i in 1..n_operations, j in 1..n_intervals ) (op_fin [i, j] = (op_status[i, j] /\ not op_status[i, j + 1])); +% Определение op_status, op_start и op_fin. + constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); % Краевые значения. + + constraint forall (op in 1..n_operations, j in {0, n_intervals + 1}) + (op_start[op, j] = false /\ op_fin[op, j] = false); + constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = (op_status[i, j] /\ not op_status[i, j - 1])); + constraint forall (i in 1..n_operations, j in 1..n_intervals ) (op_fin [i, j] = (op_status[i, j] /\ not op_status[i, j + 1])); + +% Связь ресурсов с операцией и основным объектом. + % Операции, которые могут задействовать данный объект как ресурс. + array [1..n_moving_obj] of set of 1..n_operations : operations_that_used_obj_as_resource; + + % Главный объект (субъект) операции. + array [1..n_operations] of 1..n_moving_obj : main_obj_of_operation; + + % Является ли данная операция операцией перемещения. + array [1..n_operations] of bool : is_moving_operation; + + % Операция, в которой участвует данный объект как ресурс. + array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_operations : participation_as_resource; + + % Граничные значения. + constraint forall (obj in 1..n_moving_obj) (participation_as_resource[obj, 0] = 0); + constraint forall (obj in 1..n_moving_obj) (participation_as_resource[obj, n_intervals + 1] = 0); + + % Только те операции, которые затрагивают данный объект. + constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( + participation_as_resource[obj, t] in operations_that_used_obj_as_resource[obj] + ); + + % Связь с текущими операциями перемещения. + % Если объект задействован в операции перемещения, то participation_as_resource и + % current_moving_operation должны указывать на одну и ту же операцию. + % { Если объект движется, и движется как ресурс, то participation_as_resource должен отображать этот факт. } + constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( + (current_moving_operation[obj, t] != 0) -> ( + (moving_op_of_obj[obj, current_moving_operation[obj, t]] in operations_that_used_obj_as_resource[obj]) + -> + (participation_as_resource[obj, t] = moving_op_of_obj[obj, current_moving_operation[obj, t]]) + ) + ); + % { Если объект участвует как ресурс в операции перемещения, то это согласованно с current_moving_operation, + % иначе (как ресурс в погрузке) - он должен стоять на месте. } + constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( + (participation_as_resource[obj, t] != 0) -> ( + if (is_moving_operation[participation_as_resource[obj, t]]) then + (participation_as_resource[obj, t] = moving_op_of_obj[obj, current_moving_operation[obj, t]]) + else + current_moving_operation[obj, t] = 0 + end + ) + ); + % { Объект участвует где-то в качестве ресурса - соответствующая операция обязана быть активной. } + constraint forall (obj in n_moving_obj, t in 1..n_intervals) ( + (participation_as_resource[obj, t] != 0) -> op_status[participation_as_resource[obj, t], t] + ); + % От начала операции и до конца её ресурсы не могут измениться (в том числе и для погрузки). + constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals - 1)) ( + if participation_as_resource[obj, t] != 0 then + op_status[participation_as_resource[obj, t], t + 1] -> ( + participation_as_resource[obj, t + 1] = participation_as_resource[obj, t] + ) + else true + end + ); + + int : n_resources_types; % Количество различных типов ресурсов. + array [1..n_resources_types] of set of 1..n_moving_obj : objects_of_type; % Все объекты конкретного типа. + + int : n_resources_counters; % Количество счётчиков ресурсов. + % Счётчик ресурсов. + array [1..n_resources_counters , 1..n_intervals] of var int : resources_counter; + array [1..n_resources_counters] of 1..n_resources_types : counter_type; % Типы ресурсов, за которыми следят счётчики. + array [1..n_resources_counters] of 1..n_operations : operation_of_counter; % Операция, которой принадлежит данный счётчик. + array [1..n_resources_counters] of int : required_counter_values; % Необходимые значения на счётчиках ресурсов для выполнения операции. + array [1..n_operations] of set of 1..n_resources_counters : counters_of_operation; % Счётчики, которые относятся к данной операции. + + % Участие всех необходимых ресурсов в операции. + constraint forall (t in 1..n_intervals, op in 1..n_operations, counter in counters_of_operation[op]) ( + op_status[op, t] -> (resources_counter[counter, t] = required_counter_values[counter]) + ); -% Непрерывность перемещения и швартовки. -array [1..n_operations] of int : operations_duration; -array [1..n_operations] of bool : is_continuous_operation; - -constraint forall (i in 1..n_operations where is_continuous_operation[i]) ( - let {var int : len = operations_duration[i]} in - (forall (j in 1..(n_intervals - len + 1)) ( - (op_start[i, j] == 1) -> ( - (forall (k in 1..(len - 1)) (op_status[i, j + k])) - /\ - (not op_status[i, j + len]) + % Определение resources_counter. + constraint forall (counter in 1..n_resources_counters, t in 1..n_intervals) ( + resources_counter[counter, t] = sum (obj in objects_of_type[counter_type[counter]]) ( + participation_as_resource[obj] = operation_of_counter[counter] ) - )) /\ - (forall (j in (n_intervals - len + 2)..(n_intervals + 1)) (op_start[i, j] == false)) -); + ); -% Наличие всех ресурсов на месте во время начала операции перемещения. +% Наличие всех объектов на месте во время начала операции перемещения + готовность к началу. + % Требуемое положение конкретных типов объектов в момент начала операций. + array [1..n_resources_counters] of 1..n_locations : operations_resources_start_loc; + + % Требуемое положение главного объекта в момент начала операций. + array [1..n_operations] of 1..n_locations : main_obj_start_loc; + + % Наличие и готовность всех ресурсов. + constraint forall ( + op in 1..n_operations, + t in 1..n_intervals, + counter in counters_of_operation[op], + obj in objects_of_type[counter_type[counter]] + where (participation_as_resource[obj, t] = op)) ( + op_start[op, t] -> ((m_obj_loc[obj, t] == operations_resources_start_loc[counter]) /\ + (not is_m_obj_in_movement_before_start[obj, t])) + ); -int : operations_resources_max_size; -array [1..n_operations] of 0..operations_resources_max_size : operations_resources_sizes; -array [1..n_operations, 1..operations_resources_max_size] of 1..n_moving_obj : operations_resources; -array [1..n_operations, 1..operations_resources_max_size] of 0..n_locations : operations_resources_start_loc; % Положения ресурсов в момент начала операции. + % Наличие и готовность главных объектов (субъектов). + constraint forall (op in 1..n_operations, t in 1..n_intervals) ( + op_start[op, t] -> ((m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op]) /\ + (not is_m_obj_in_movement_before_start[main_obj_of_operation[op], t])) + ); -constraint forall (op in 1..n_operations, t in 1..n_intervals) ( - forall (op_res_id in 1..operations_resources_sizes[op]) ( - (op_start[op, t]) -> ((m_obj_loc[operations_resources[op, op_res_id], t] == operations_resources_start_loc[op, op_res_id]) /\ - (not is_m_obj_in_movement_before_start[operations_resources[op, op_res_id], t])) - ) -); +% Непрерывность перемещения и швартовки. + array [1..n_operations] of int : operations_duration; + array [1..n_operations] of bool : is_continuous_operation; + + constraint forall (i in 1..n_operations where is_continuous_operation[i]) ( + let {var int : len = operations_duration[i]} in + (forall (j in 1..(n_intervals - len + 1)) ( + (op_start[i, j] == 1) -> ( + (forall (k in 1..(len - 1)) (op_status[i, j + k])) + /\ + (not op_status[i, j + len]) + ) + )) /\ + (forall (j in (n_intervals - len + 2)..(n_intervals + 1)) (op_start[i, j] == false)) + ); % Конфликтующие операции. -int : n_conflicting_op; + int : n_conflicting_op; -array [1..n_conflicting_op] of 1..n_operations : confl_op_1; -array [1..n_conflicting_op] of 1..n_operations : confl_op_2; + array [1..n_conflicting_op] of 1..n_operations : confl_op_1; + array [1..n_conflicting_op] of 1..n_operations : confl_op_2; -constraint forall (t in 0..(n_intervals + 1), i in 1..n_conflicting_op) ( - op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t] -); + constraint forall (t in 0..(n_intervals + 1), i in 1..n_conflicting_op) ( + op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t] + ); % Окна непогоды. -int : n_bad_weather_windows; -array [1..n_bad_weather_windows] of 1..n_operations : bw_op; -array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_start; -array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно. + int : n_bad_weather_windows; + array [1..n_bad_weather_windows] of 1..n_operations : bw_op; + array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_start; + array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно. -constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) ( - op_status[bw_op[i], t] == false -); + constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) ( + op_status[bw_op[i], t] == false + ); % Грузообработка. -int : n_cargo_types; -int : n_obj_with_storage; -array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of var int : storage_used_volume; % Первые n_moving_obj соответствуют наполненности соответствующих движущихся объектов. - -% Ограничения на вместимость. -array [1..n_obj_with_storage] of int : max_storage_vol; -constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1)) ( % Масимальный объём. - sum (cargo in 1..n_cargo_types) (storage_used_volume[storage, t, cargo]) <= max_storage_vol[storage] -); -constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1), cargo in 1..n_cargo_types) ( % Неотрицательность объёма. - 0 <= storage_used_volume[storage, t, cargo] -); - -% Ограничения на граничные значения. -array [1..n_obj_with_storage, 1..n_cargo_types] of int : initial_storage_vol; -array [1..n_obj_with_storage, 1..n_cargo_types] of int : final_storage_vol; - -constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Initial values. - storage_used_volume[storage, 0, cargo] = initial_storage_vol[storage, cargo] -); - -constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Final values. - if final_storage_vol[storage, cargo] >= 0 then - storage_used_volume[storage, n_intervals + 1, cargo] == final_storage_vol[storage, cargo] - else true - endif -); - -% Изменение грузов в хранилищах. -array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of int : cargo_flows; - -int : n_loading_op; - -array [1..n_loading_op] of int : loading_op_delta; -array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций. - -int : involved_operations_max_size; -array [1..n_obj_with_storage, 1..n_cargo_types] of 0..involved_operations_max_size : involved_operations_sizes; -array [1..n_obj_with_storage, 1..n_cargo_types, 1..involved_operations_max_size] of 1..n_loading_op : involved_operations; - -constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, t in 1..(n_intervals + 1)) ( - storage_used_volume[storage, t, cargo] == ( - storage_used_volume[storage, t - 1, cargo] + - cargo_flows[storage, t, cargo] + - sum (inv_op_no in 1..involved_operations_sizes[storage, cargo]) ( - loading_op_delta[involved_operations[storage, cargo, inv_op_no]] * - op_status[loading_op_n[involved_operations[storage, cargo, inv_op_no]], t] - ) - ) -); + int : n_cargo_types; + int : n_obj_with_storage; + array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of var int : storage_used_volume; % Первые n_moving_obj соответствуют наполненности соответствующих движущихся объектов. + + % Ограничения на вместимость. + array [1..n_obj_with_storage] of int : max_storage_vol; + % Масимальный объём. + constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1)) ( + sum (cargo in 1..n_cargo_types) (storage_used_volume[storage, t, cargo]) <= max_storage_vol[storage] + ); + % Неотрицательность объёма. + constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1), cargo in 1..n_cargo_types) ( + 0 <= storage_used_volume[storage, t, cargo] + ); + + % Ограничения на граничные значения. + array [1..n_obj_with_storage, 1..n_cargo_types] of int : initial_storage_vol; + array [1..n_obj_with_storage, 1..n_cargo_types] of int : final_storage_vol; + + constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Initial values. + storage_used_volume[storage, 0, cargo] = initial_storage_vol[storage, cargo] + ); + + constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Final values. + if final_storage_vol[storage, cargo] >= 0 then + storage_used_volume[storage, n_intervals + 1, cargo] == final_storage_vol[storage, cargo] + else true + endif + ); + + % Изменение грузов в хранилищах. + array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of int : cargo_flows; + + int : n_loading_op; + + array [1..n_loading_op] of int : loading_op_delta; + array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций. + + int : involved_operations_max_size; + array [1..n_obj_with_storage, 1..n_cargo_types] of 0..involved_operations_max_size : involved_operations_sizes; + array [1..n_obj_with_storage, 1..n_cargo_types, 1..involved_operations_max_size] of 1..n_loading_op : involved_operations; + + constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, t in 1..(n_intervals + 1)) ( + storage_used_volume[storage, t, cargo] == ( + storage_used_volume[storage, t - 1, cargo] + + cargo_flows[storage, t, cargo] + + sum (inv_op_no in 1..involved_operations_sizes[storage, cargo]) ( + loading_op_delta[involved_operations[storage, cargo, inv_op_no]] * + op_status[loading_op_n[involved_operations[storage, cargo, inv_op_no]], t] + ) + ) + ); % Критерий оптимизации -array [0..(n_intervals + 1)] of var bool : is_not_terminated; -constraint (is_not_terminated[0] == false /\ is_not_terminated[n_intervals + 1] == false); - -constraint forall (t in 1..n_intervals) ( - is_not_terminated[t] == ( - (exists (op in 1..n_operations) (op_status[op, t])) - \/ - is_not_terminated[t + 1] - ) -); - -solve minimize sum(is_not_terminated); + array [0..(n_intervals + 1)] of var bool : is_not_terminated; + constraint (is_not_terminated[0] == false /\ is_not_terminated[n_intervals + 1] == false); + + constraint forall (t in 1..n_intervals) ( + is_not_terminated[t] == ( + (exists (op in 1..n_operations) (op_status[op, t])) + \/ + is_not_terminated[t + 1] + ) + ); + + solve minimize sum(is_not_terminated); output [show(sum(is_not_terminated)), "\n", show(op_status), "\n\n", diff --git a/src/inport/Testing.java b/src/inport/Testing.java index 02784e8..56c8e34 100644 --- a/src/inport/Testing.java +++ b/src/inport/Testing.java @@ -60,7 +60,7 @@ public class Testing { int exitCode = process.waitFor(); assert exitCode == 0; - BufferedReader br=new BufferedReader(new InputStreamReader(process.getInputStream())); + BufferedReader br = new BufferedReader(new InputStreamReader(process.getInputStream())); String output = br.lines().collect(Collectors.joining("\n")); if (output.trim().equals("=====UNSATISFIABLE=====")) { -- GitLab