diff --git a/src/constraints/conversion_2.mod b/src/constraints/conversion_2.mod index b4a8e849b63e34126b15274e51ab05f7e04d7f3f..9f19e2deb32b389593be40c4fd9b532d4005e860 100644 --- a/src/constraints/conversion_2.mod +++ b/src/constraints/conversion_2.mod @@ -142,6 +142,26 @@ int can_obj_leave_loc_only_alone[1..n_moving_obj, 1..n_locations] = ...; int is_fixed_op_planned_in_future[1..n_moving_obj, 1..n_locations, 1..n_intervals] = ...; +// Возможно ли начать операцию в данный интервал (если предположить, что операция длится 1 интервал). +dvar boolean is_op_possible[0..n_operations, 1..n_intervals]; + +// Счётчик ресурсов, которые могут быть потенциально задействованы в операции. +dvar int possible_resources_counter[1..n_resources_counters , 1..n_intervals]; + +dvar boolean is_enough_free_resources[0..n_operations, 1..n_intervals]; + + +dvar boolean can_obj_theoretically_use_cargo_op[0..n_moving_obj, 0..(n_intervals + 1)]; +// Остановился ли объект окончательно, начиная с данного интервала. +dvar boolean is_obj_totally_terminated[0..n_moving_obj, 0..(n_intervals + 1)]; + + +dvar int prev_m_obj_loc[0..n_moving_obj, 0..(n_intervals + 1)] in 1..n_locations; +dvar boolean is_obj_involved_in_useful_operation[0..n_moving_obj, 0..(n_intervals + 1)]; + +// Успел ли объект поучаствовать в полезной операции к концу данного интервала. +dvar boolean is_attended_useful_op_in_cur_loc[0..n_moving_obj, 0..(n_intervals + 1)]; + dvar boolean is_not_terminated[1..(n_intervals + 1)]; minimize sum (i in 1..(n_intervals + 1)) is_not_terminated[i]; @@ -430,171 +450,153 @@ subject to { -// // Оптимизация - сдвиг в начало. -// // Возможно ли начать операцию в данный интервал (если предположить, что операция длится 1 интервал). -// array [0..n_operations, 1..n_intervals] of var bool : is_op_possible; -// -// forall (t in 1..n_intervals) (is_op_possible[0, t] == false); // Фиктивный объект. -// -// // Счётчик ресурсов, которые могут быть потенциально задействованы в операции. -// array [1..n_resources_counters , 1..n_intervals] of var int : possible_resources_counter; -// -// // Определение possible_resources_counter. -// forall (counter in 1..n_resources_counters, t in 1..n_intervals) ( -// possible_resources_counter[counter, t] == sum (obj in objects_of_type[counter_type[counter]]) ( -// (participation_as_resource[obj, t] == 0) && -// (current_moving_operation[obj, t] == 0) && -// (m_obj_loc[obj, t] == operations_resources_start_loc[counter]) -// ) -// ); -// -// // Достаточно ли свободных ресурсов для операции. -// array [0..n_operations, 1..n_intervals] of var bool : is_enough_free_resources; -// -// forall (t in 1..n_intervals) (is_enough_free_resources[0, t] == false); // Фиктивный объект. -// -// forall (op in 1..n_operations, t in 1..n_intervals) ( -// is_enough_free_resources[op, t] == forall (counter in counters_of_operation[op]) ( -// possible_resources_counter[counter, t] >= required_counter_values[counter] -// ) -// ); -// -// // Определение is_op_possible. -// forall (op in 1..n_operations, t in 1..n_intervals) ( -// is_op_possible[op, t] == ( -// (bad_weather[op, t] == false) && // Погода не мешает. -// (m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op]) -// && // Главный объект на месте. -// (current_moving_operation[main_obj_of_operation[op], t] == 0) -// && // Главный объект не участвует в операции перемещеня. -// (is_enough_free_resources[op, t] == true) && // Достаточно свободных ресурсов на нужном месте. -// (forall (conf_op in conflicting_operations[op]) (op_status[conf_op, t] == false)) -// && // Не выполняется ни одной конфликтующей операции. -// (is_moving_operation[op] -> not is_involved_in_cargo_op[main_obj_of_operation[op], t]) -// && // Если это операция перемещения, то главный объект -// // не участвует в операциях погрузки. -// ((is_mooring_op[op] && (operations_destination[op] mod 2 = 0)) -> ( -// current_moored_obj[operations_destination[op], t] = 0) -// ) && // Если это операция пришвартовки, то в этот интервал -// // причал должен быть свободным. -// ((not is_moving_operation[op]) -> ( -// let {1..n_all_storage_sections : m_stor = operations_main_stor[op]; -// 1..n_all_storage_sections : s_stor = operations_secondary_stor[op]; -// int : delta = loading_op_delta_of_main_obj[op]; -// } in -// (storage_used_volume[m_stor, t] + delta >= 0) /\ -// (storage_used_volume[m_stor, t] + delta <= max_storage_vol[m_stor]) /\ -// (storage_used_volume[s_stor, t] - delta >= 0) /\ -// (storage_used_volume[s_stor, t] - delta <= max_storage_vol[s_stor]) -// )) /\ // Если это операция грузообработки, то она не выведет -// // объём берегового хранилища и хранилища судна за -// // границы дозволенного. -// (((not is_moving_operation[op]) /\ (main_obj_start_loc[op] mod 2 = 1)) -> -// ((current_moored_obj[twin_location[main_obj_start_loc[op]], t] = 0) \/ -// (current_moored_obj[twin_location[main_obj_start_loc[op]], t] = main_obj_of_operation[op])) -// ) /\ // Если это операция грузообработки без пришвартовки, -// // то причал должен быть свободен в этот интервал, либо -// // главный объект должен быть уже условно пришвартован. -// (((bunker_of_cargo_op[op] != 0) /\ (op_status[op, t])) -> -// ((m_obj_loc[bunker_of_cargo_op[op], t] = bunker_start_loc[op]) /\ -// (current_moving_operation[bunker_of_cargo_op[op], t] = 0)) -// ) // Бункеровщик (если есть) находится в нужной локации -// // и не участвует в операциях перемещения. -// ) -// ); -// -// // Сам критерий оптимизации - если если операцию можно было начать на 1 интервал раньше, то её нужно начать раньше. -// forall (op in 1..n_operations, t in 2..n_intervals) ( -// (op_start[op, t] /\ (not is_fixed[op, t])) -> not is_op_possible[op, t - 1] -// ); + // Оптимизация - сдвиг в начало. + forall (t in 1..n_intervals) (is_op_possible[0, t] == false); // Фиктивный объект. + + // Определение possible_resources_counter. + forall (counter in 1..n_resources_counters, t in 1..n_intervals) ( + possible_resources_counter[counter, t] == sum (obj in objects_of_type[counter_type[counter]]) ( + (participation_as_resource[obj, t] == 0) && + (current_moving_operation[obj, t] == 0) && + (m_obj_loc[obj, t] == operations_resources_start_loc[counter]) + ) + ); + + // Достаточно ли свободных ресурсов для операции. + + forall (t in 1..n_intervals) (is_enough_free_resources[0, t] == false); // Фиктивный объект. + + forall (op in 1..n_operations, t in 1..n_intervals) ( + is_enough_free_resources[op, t] == and (counter in counters_of_operation[op]) ( + possible_resources_counter[counter, t] >= required_counter_values[counter] + ) + ); + + // Определение is_op_possible. + forall (op in 1..n_operations, t in 1..n_intervals) ( + is_op_possible[op, t] == ( + (bad_weather[op, t] == 0) && // Погода не мешает. + (m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op]) + && // Главный объект на месте. + (current_moving_operation[main_obj_of_operation[op], t] == 0) + && // Главный объект не участвует в операции перемещеня. + (is_enough_free_resources[op, t] == true) && // Достаточно свободных ресурсов на нужном месте. + (and (conf_op in conflicting_operations[op]) (op_status[conf_op, t] == false)) + && // Не выполняется ни одной конфликтующей операции. + ((is_moving_operation[op] == 1) => is_involved_in_cargo_op[main_obj_of_operation[op], t] == false) + && // Если это операция перемещения, то главный объект + // не участвует в операциях погрузки. + (((is_mooring_op[op] == 1) && (operations_destination[op] mod 2 == 0)) => ( + current_moored_obj[operations_destination[op], t] == 0) + ) && // Если это операция пришвартовки, то в этот интервал + // причал должен быть свободным. + ((is_moving_operation[op] == 0) => ( + (storage_used_volume[operations_main_stor[op], t] + loading_op_delta_of_main_obj[op] >= 0) && + (storage_used_volume[operations_main_stor[op], t] + loading_op_delta_of_main_obj[op] <= max_storage_vol[operations_main_stor[op]]) && + (storage_used_volume[operations_secondary_stor[op], t] - loading_op_delta_of_main_obj[op] >= 0) && + (storage_used_volume[operations_secondary_stor[op], t] - loading_op_delta_of_main_obj[op] <= max_storage_vol[operations_secondary_stor[op]]) + )) && // Если это операция грузообработки, то она не выведет + // объём берегового хранилища и хранилища судна за + // границы дозволенного. + (((is_moving_operation[op] == 0) && (main_obj_start_loc[op] mod 2 == 1)) => + ((current_moored_obj[twin_location[main_obj_start_loc[op]], t] == 0) || + (current_moored_obj[twin_location[main_obj_start_loc[op]], t] == main_obj_of_operation[op])) + ) && // Если это операция грузообработки без пришвартовки, + // то причал должен быть свободен в этот интервал, либо + // главный объект должен быть уже условно пришвартован. + (((bunker_of_cargo_op[op] != 0) && (op_status[op, t] == 0)) => + ((m_obj_loc[bunker_of_cargo_op[op], t] == bunker_start_loc[op]) && + (current_moving_operation[bunker_of_cargo_op[op], t] == 0)) + ) // Бункеровщик (если есть) находится в нужной локации + // и не участвует в операциях перемещения. + ) + ); + + // Сам критерий оптимизации - если если операцию можно было начать на 1 интервал раньше, то её нужно начать раньше. + forall (op in 1..n_operations, t in 2..n_intervals) ( + ((op_start[op, t] == 1) && (is_fixed[op, t] == 0)) => (is_op_possible[op, t - 1] == 0) + ); // Оптимизация - судно возвращается откуда перед этим пришло -> оно сделало или делает что-то "полезное". -// array [0..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : prev_m_obj_loc; -// array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_involved_in_useful_operation; -// -// constraint forall (t in 0..(n_intervals + 1)) (prev_m_obj_loc[0, t] = 1); -// constraint forall (t in 0..(n_intervals + 1)) (is_obj_involved_in_useful_operation[0, t] = false); -// -// // Определение prev_m_obj_loc -// constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( -// (m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) -> (prev_m_obj_loc[obj, t] = m_obj_loc[obj, t - 1]) -// ); -// constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( -// (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t]) -> (prev_m_obj_loc[obj, t] = prev_m_obj_loc[obj, t - 1]) -// ); -// constraint forall (obj in 1..n_moving_obj) (prev_m_obj_loc[obj, 0] = m_obj_loc[obj, 0]); -// -// // Определение is_obj_involved_in_useful_operation -// constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( -// is_obj_involved_in_useful_operation[obj, t] = ( -// (participation_as_resource[obj, t] != 0) -// \/ (exists (op in related_cargo_op[obj]) (op_status[op, t])) -// \/ (is_obj_involved_in_fixed_op[obj, t]) -// \/ (exists (op in related_unmooring_op[obj]) (op_status[op, t])) -// ) -// ); -// constraint forall (obj in 1..n_moving_obj) (is_obj_involved_in_useful_operation[obj, 0] = false); -// -// // Успел ли объект поучаствовать в полезной операции к концу данного интервала. -// array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_attended_useful_op_in_cur_loc; -// // Определение is_attended_useful_op_in_cur_loc -// constraint forall (t in 0..(n_intervals + 1)) (is_attended_useful_op_in_cur_loc[0, t] = false); -// -// constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( -// is_attended_useful_op_in_cur_loc[obj, t] = ( -// (is_attended_useful_op_in_cur_loc[obj, t - 1] /\ (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t])) // Предыдущее значение в текущей локации. -// \/ -// is_obj_involved_in_useful_operation[obj, t] -// \/ -// is_obj_involved_in_useful_operation[obj, t - 1] // Учитывает случай когда операция перемещения, из-за которой объект попал в локацию была нужна. -// ) -// ); -// -// // Сама оптимизация - если объект -// constraint forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) ( -// ((m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) /\ (prev_m_obj_loc[obj, t - 1] == m_obj_loc[obj, t]) -// ) -> is_attended_useful_op_in_cur_loc[obj, t - 1] -// ); - -// // Оптимизация - если объект не может совершить в данной локации операции без выхода за границы хранилища, а так же если он -// // может уйти только своим ходом, то он либо уходит немедленно, либо остаётся на месте навсегда. -// -// array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : can_obj_theoretically_use_cargo_op; -// // Определение can_obj_theoretically_use_cargo_op. -// constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( -// can_obj_theoretically_use_cargo_op[obj, t] = ( -// is_sections_of_moving_obj_empty[obj] -// \/ -// exists (section in sections_of_moving_obj[obj]) ( -// (storage_used_volume[section, t - 1] + min_positive_cargo_val[section, main_location[m_obj_loc[obj, t]]] <= max_storage_vol[section]) -// \/ (storage_used_volume[section, t - 1] + max_negative_cargo_val[section, main_location[m_obj_loc[obj, t]]] >= 0) -// ) -// ) -// ); -// constraint forall (t in 0..(n_intervals + 1)) (can_obj_theoretically_use_cargo_op[0, t] = false); -// constraint forall (obj in 1..n_moving_obj) (can_obj_theoretically_use_cargo_op[obj, 0] = false); -// -// // Остановился ли объект окончательно, начиная с данного интервала. -// array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_totally_terminated; -// constraint forall (obj in 1..n_moving_obj) (is_obj_totally_terminated[obj, n_intervals + 1] = true); -// constraint forall (t in 0..(n_intervals + 1)) (is_obj_totally_terminated[0, t] = true); -// -// constraint forall (obj in 1..n_moving_obj, t in 0..n_intervals) ( -// is_obj_totally_terminated[obj, t] = ( -// (current_moving_operation[obj, t] = 0) -// /\ (not is_involved_in_cargo_op[obj, t]) -// /\ (is_obj_totally_terminated[obj, t + 1]) -// ) -// ); -// -// // Само ограничение. -// constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( -// ( (can_obj_leave_loc_only_alone[obj, m_obj_loc[obj, t]]) -// /\ (not can_obj_theoretically_use_cargo_op[obj, t]) -// /\ (not is_fixed_op_planned_in_future[obj, m_obj_loc[obj, t], t]) -// ) -> -// (is_obj_totally_terminated[obj, t] \/ (current_moving_operation[obj, t] != 0)) -// ); + forall (t in 0..(n_intervals + 1)) (prev_m_obj_loc[0, t] == 1); + forall (t in 0..(n_intervals + 1)) (is_obj_involved_in_useful_operation[0, t] == 0); + + // Определение prev_m_obj_loc + forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( + (m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) => (prev_m_obj_loc[obj, t] == m_obj_loc[obj, t - 1]) + ); + forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( + (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t]) => (prev_m_obj_loc[obj, t] == prev_m_obj_loc[obj, t - 1]) + ); + forall (obj in 1..n_moving_obj) (prev_m_obj_loc[obj, 0] == m_obj_loc[obj, 0]); + + // Определение is_obj_involved_in_useful_operation + forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( + is_obj_involved_in_useful_operation[obj, t] == ( + (participation_as_resource[obj, t] != 0) + || (or (op in related_cargo_op[obj]) (op_status[op, t] == 1)) + || (is_obj_involved_in_fixed_op[obj, t] == 1) + || (or (op in related_unmooring_op[obj]) (op_status[op, t] == 1)) + ) + ); + forall (obj in 1..n_moving_obj) (is_obj_involved_in_useful_operation[obj, 0] == 0); + + // Определение is_attended_useful_op_in_cur_loc + forall (t in 0..(n_intervals + 1)) (is_attended_useful_op_in_cur_loc[0, t] == 0); + + forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( + is_attended_useful_op_in_cur_loc[obj, t] == ( + ((is_attended_useful_op_in_cur_loc[obj, t - 1] == 1) && (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t])) // Предыдущее значение в текущей локации. + || + (is_obj_involved_in_useful_operation[obj, t] == 1) + || + (is_obj_involved_in_useful_operation[obj, t - 1] == 1) // Учитывает случай когда операция перемещения, из-за которой объект попал в локацию была нужна. + ) + ); + + // Сама оптимизация - если объект + forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) ( + ((m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) && (prev_m_obj_loc[obj, t - 1] == m_obj_loc[obj, t]) + ) => (is_attended_useful_op_in_cur_loc[obj, t - 1] == 1) + ); + + // Оптимизация - если объект не может совершить в данной локации операции без выхода за границы хранилища, а так же если он + // может уйти только своим ходом, то он либо уходит немедленно, либо остаётся на месте навсегда. + + // Определение can_obj_theoretically_use_cargo_op. + forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( + can_obj_theoretically_use_cargo_op[obj, t] == ( + (is_sections_of_moving_obj_empty[obj] == 1) + || + or (section in sections_of_moving_obj[obj]) ( + (storage_used_volume[section, t - 1] + min_positive_cargo_val[section, main_location[m_obj_loc[obj, t]]] <= max_storage_vol[section]) + || (storage_used_volume[section, t - 1] + max_negative_cargo_val[section, main_location[m_obj_loc[obj, t]]] >= 0) + ) + ) + ); + forall (t in 0..(n_intervals + 1)) (can_obj_theoretically_use_cargo_op[0, t] == false); + forall (obj in 1..n_moving_obj) (can_obj_theoretically_use_cargo_op[obj, 0] == false); + + + forall (obj in 1..n_moving_obj) (is_obj_totally_terminated[obj, n_intervals + 1] == true); + forall (t in 0..(n_intervals + 1)) (is_obj_totally_terminated[0, t] == true); + + forall (obj in 1..n_moving_obj, t in 0..n_intervals) ( + is_obj_totally_terminated[obj, t] == ( + (current_moving_operation[obj, t] == 0) + && (is_involved_in_cargo_op[obj, t] == 0) + && (is_obj_totally_terminated[obj, t + 1] == 1) + ) + ); + + // Само ограничение. + forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( + ( (can_obj_leave_loc_only_alone[obj, m_obj_loc[obj, t]] == 1) + && (can_obj_theoretically_use_cargo_op[obj, t] == 0) + && (is_fixed_op_planned_in_future[obj, m_obj_loc[obj, t], t] == 0) + ) => + ((is_obj_totally_terminated[obj, t] == 1) || (current_moving_operation[obj, t] != 0)) + ); // Критерий оптимизации // В конце всё остановится. @@ -624,5 +626,8 @@ execute { writeln("participation_as_resource = ", participation_as_resource, ";"); writeln("is_involved_in_cargo_op = ", is_involved_in_cargo_op, ";"); + + + writeln("is_op_possible = ", is_op_possible, ";"); }