Skip to content

GitLab

C
Conversion
Commit 2b2c076f authored by Vladislav Kiselev's avatar Vladislav Kiselev
Browse files
Options

refactoring и ограничения на типизированный случай

parent ef1aa7f0
Hide whitespace changes
Inline Side-by-side
Showing with 219 additions and 119 deletions
src/constraints/conversion_2.mzn
View file @ 2b2c076f
...@@ -13,7 +13,10 @@ int : moving_op_of_obj_max_size; ...@@ -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] 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, 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)) ( 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] 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 ...@@ -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])) (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]); 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 ...@@ -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; % Локация в которой окажется объект после завершения операции. array [1..n_operations] of 1..n_locations : operations_destination; % Локация в которой окажется объект после завершения операции.
% Теперь m_obj_loc означает где объект стоит или куда он движется перед началом определённого интервала. % Определение m_obj_loc.
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; % Moving object location. % Местоположение объекта или пункт назначения (если объект движется) перед началом определённого интервала.
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) ( constraint forall (obj in 1..n_moving_obj) (
m_obj_loc[obj, 1] = m_obj_loc[obj, 0] 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; ...@@ -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; 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]); 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; array [1..n_moving_obj] of var 0..n_locations : final_m_obj_loc;
constraint forall (i in 1..n_moving_obj) ( constraint forall (i in 1..n_moving_obj) (
(final_m_obj_loc[i] != 0) -> (final_m_obj_loc[i] != 0) ->
(m_obj_loc[i, n_intervals + 1] = final_m_obj_loc[i]) (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); % Краевые значения.
% Определение op_start и op_fin. % Определение op_status, op_start и op_fin.
constraint forall (op in 1..n_operations, j in {0, n_intervals + 1}) constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); % Краевые значения.
(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 (op in 1..n_operations, j in {0, n_intervals + 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_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])
);
% Непрерывность перемещения и швартовки. % Определение resources_counter.
array [1..n_operations] of int : operations_duration; constraint forall (counter in 1..n_resources_counters, t in 1..n_intervals) (
array [1..n_operations] of bool : is_continuous_operation; resources_counter[counter, t] = sum (obj in objects_of_type[counter_type[counter]]) (
participation_as_resource[obj] = operation_of_counter[counter]
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))
);
% Наличие всех ресурсов на месте во время начала операции перемещения. % Наличие всех объектов на месте во время начала операции перемещения + готовность к началу.
% Требуемое положение конкретных типов объектов в момент начала операций.
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; constraint forall (op in 1..n_operations, t in 1..n_intervals) (
array [1..n_operations, 1..operations_resources_max_size] of 1..n_moving_obj : operations_resources; op_start[op, t] -> ((m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op]) /\
array [1..n_operations, 1..operations_resources_max_size] of 0..n_locations : operations_resources_start_loc; % Положения ресурсов в момент начала операции. (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]) ( array [1..n_operations] of int : operations_duration;
(op_start[op, t]) -> ((m_obj_loc[operations_resources[op, op_res_id], t] == operations_resources_start_loc[op, op_res_id]) /\ array [1..n_operations] of bool : is_continuous_operation;
(not is_m_obj_in_movement_before_start[operations_resources[op, op_res_id], t]))
) 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_1;
array [1..n_conflicting_op] of 1..n_operations : confl_op_2; 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) ( 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] op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t]
); );
% Окна непогоды. % Окна непогоды.
int : n_bad_weather_windows; int : n_bad_weather_windows;
array [1..n_bad_weather_windows] of 1..n_operations : bw_op; 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_start;
array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно. 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]) ( constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) (
op_status[bw_op[i], t] == false op_status[bw_op[i], t] == false
); );
% Грузообработка. % Грузообработка.
int : n_cargo_types; int : n_cargo_types;
int : n_obj_with_storage; 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, 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; 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)) (
); 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] % Неотрицательность объёма.
); 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; % Ограничения на граничные значения.
array [1..n_obj_with_storage, 1..n_cargo_types] of int : initial_storage_vol;
constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Initial values. array [1..n_obj_with_storage, 1..n_cargo_types] of int : final_storage_vol;
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) ( % 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] constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Final values.
else true if final_storage_vol[storage, cargo] >= 0 then
endif 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_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of int : cargo_flows;
array [1..n_loading_op] of int : loading_op_delta; int : n_loading_op;
array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций.
array [1..n_loading_op] of int : loading_op_delta;
int : involved_operations_max_size; array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций.
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; int : involved_operations_max_size;
array [1..n_obj_with_storage, 1..n_cargo_types] of 0..involved_operations_max_size : involved_operations_sizes;
constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, t in 1..(n_intervals + 1)) ( array [1..n_obj_with_storage, 1..n_cargo_types, 1..involved_operations_max_size] of 1..n_loading_op : involved_operations;
storage_used_volume[storage, t, cargo] == (
storage_used_volume[storage, t - 1, cargo] + constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, t in 1..(n_intervals + 1)) (
cargo_flows[storage, t, cargo] + storage_used_volume[storage, t, cargo] == (
sum (inv_op_no in 1..involved_operations_sizes[storage, cargo]) ( storage_used_volume[storage, t - 1, cargo] +
loading_op_delta[involved_operations[storage, cargo, inv_op_no]] * cargo_flows[storage, t, cargo] +
op_status[loading_op_n[involved_operations[storage, cargo, inv_op_no]], t] 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; 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 (is_not_terminated[0] == false /\ is_not_terminated[n_intervals + 1] == false);
constraint forall (t in 1..n_intervals) ( constraint forall (t in 1..n_intervals) (
is_not_terminated[t] == ( is_not_terminated[t] == (
(exists (op in 1..n_operations) (op_status[op, t])) (exists (op in 1..n_operations) (op_status[op, t]))
\/ \/
is_not_terminated[t + 1] is_not_terminated[t + 1]
) )
); );
solve minimize sum(is_not_terminated); solve minimize sum(is_not_terminated);
output [show(sum(is_not_terminated)), "\n", output [show(sum(is_not_terminated)), "\n",
show(op_status), "\n\n", show(op_status), "\n\n",
......
src/inport/Testing.java
View file @ 2b2c076f
...@@ -60,7 +60,7 @@ public class Testing { ...@@ -60,7 +60,7 @@ public class Testing {
int exitCode = process.waitFor(); int exitCode = process.waitFor();
assert exitCode == 0; 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")); String output = br.lines().collect(Collectors.joining("\n"));
if (output.trim().equals("=====UNSATISFIABLE=====")) { if (output.trim().equals("=====UNSATISFIABLE=====")) {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment