From 948edc58dae8b2e745304f30e6b69c5edf30b17e Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 15 Apr 2025 21:12:48 +0200 Subject: [PATCH] update julia wrapper --- .../src/moi_wrapper/Type_wrappers.jl | 10 +++++----- .../sat/sat_parameters_pb.jl | 18 +++++++++--------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/ortools/julia/ORTools.jl/src/moi_wrapper/Type_wrappers.jl b/ortools/julia/ORTools.jl/src/moi_wrapper/Type_wrappers.jl index 3abc46ae6a..a7debbc3e0 100644 --- a/ortools/julia/ORTools.jl/src/moi_wrapper/Type_wrappers.jl +++ b/ortools/julia/ORTools.jl/src/moi_wrapper/Type_wrappers.jl @@ -933,7 +933,7 @@ mutable struct SatParameters <: AbstractSatParameters exploit_objective::Bool probing_period_at_root::Int64 use_probing_search::Bool - use_shaving_in_probing_search::Bool + shaving_deterministic_time_in_probing_search::Float64 shaving_search_deterministic_time::Float64 use_objective_lb_search::Bool use_objective_shaving_search::Bool @@ -1154,8 +1154,8 @@ mutable struct SatParameters <: AbstractSatParameters exploit_objective = true, probing_period_at_root = Int64(0), use_probing_search = false, - use_shaving_in_probing_search = true, - shaving_search_deterministic_time = Float64(0.001), + shaving_deterministic_time_in_probing_search = Float64(0.001), + shaving_search_deterministic_time = Float64(0.1), use_objective_lb_search = false, use_objective_shaving_search = false, pseudo_cost_reliability_threshold = Int64(100), @@ -1375,7 +1375,7 @@ mutable struct SatParameters <: AbstractSatParameters exploit_objective, probing_period_at_root, use_probing_search, - use_shaving_in_probing_search, + shaving_deterministic_time_in_probing_search, shaving_search_deterministic_time, use_objective_lb_search, use_objective_shaving_search, @@ -1603,7 +1603,7 @@ function to_proto_struct( sat_parameters.exploit_objective, sat_parameters.probing_period_at_root, sat_parameters.use_probing_search, - sat_parameters.use_shaving_in_probing_search, + sat_parameters.shaving_deterministic_time_in_probing_search, sat_parameters.shaving_search_deterministic_time, sat_parameters.use_objective_lb_search, sat_parameters.use_objective_shaving_search, diff --git a/ortools/julia/ORToolsGenerated.jl/src/genproto/operations_research/sat/sat_parameters_pb.jl b/ortools/julia/ORToolsGenerated.jl/src/genproto/operations_research/sat/sat_parameters_pb.jl index 2a3a91305f..295154ce01 100644 --- a/ortools/julia/ORToolsGenerated.jl/src/genproto/operations_research/sat/sat_parameters_pb.jl +++ b/ortools/julia/ORToolsGenerated.jl/src/genproto/operations_research/sat/sat_parameters_pb.jl @@ -199,7 +199,7 @@ struct SatParameters <: var"##AbstractSatParameters" exploit_objective::Bool probing_period_at_root::Int64 use_probing_search::Bool - use_shaving_in_probing_search::Bool + shaving_deterministic_time_in_probing_search::Float64 shaving_search_deterministic_time::Float64 use_objective_lb_search::Bool use_objective_shaving_search::Bool @@ -263,8 +263,8 @@ struct SatParameters <: var"##AbstractSatParameters" mip_max_valid_magnitude::Float64 mip_drop_tolerance::Float64 end -PB.default_values(::Type{SatParameters}) = (;name = "", preferred_variable_order = var"SatParameters.VariableOrder".IN_ORDER, initial_polarity = var"SatParameters.Polarity".POLARITY_FALSE, use_phase_saving = true, polarity_rephase_increment = Int32(1000), random_polarity_ratio = Float64(0.0), random_branches_ratio = Float64(0.0), use_erwa_heuristic = false, initial_variables_activity = Float64(0.0), also_bump_variables_in_conflict_reasons = false, minimization_algorithm = var"SatParameters.ConflictMinimizationAlgorithm".RECURSIVE, binary_minimization_algorithm = var"SatParameters.BinaryMinizationAlgorithm".BINARY_MINIMIZATION_FIRST, subsumption_during_conflict_analysis = true, clause_cleanup_period = Int32(10000), clause_cleanup_target = Int32(0), clause_cleanup_ratio = Float64(0.5), clause_cleanup_protection = var"SatParameters.ClauseProtection".PROTECTION_NONE, clause_cleanup_lbd_bound = Int32(5), clause_cleanup_ordering = var"SatParameters.ClauseOrdering".CLAUSE_ACTIVITY, pb_cleanup_increment = Int32(200), pb_cleanup_ratio = Float64(0.5), minimize_with_propagation_restart_period = Int32(10), minimize_with_propagation_num_decisions = Int32(1000), variable_activity_decay = Float64(0.8), max_variable_activity_value = Float64(1e100), glucose_max_decay = Float64(0.95), glucose_decay_increment = Float64(0.01), glucose_decay_increment_period = Int32(5000), clause_activity_decay = Float64(0.999), max_clause_activity_value = Float64(1e20), restart_algorithms = Vector{var"SatParameters.RestartAlgorithm".T}(), default_restart_algorithms = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART", restart_period = Int32(50), restart_running_window_size = Int32(50), restart_dl_average_ratio = Float64(1.0), restart_lbd_average_ratio = Float64(1.0), use_blocking_restart = false, blocking_restart_window_size = Int32(5000), blocking_restart_multiplier = Float64(1.4), num_conflicts_before_strategy_changes = Int32(0), strategy_change_increase_ratio = Float64(0.0), max_time_in_seconds = Float64(Inf), max_deterministic_time = Float64(Inf), max_number_of_conflicts = Int64(9223372036854775807), max_memory_in_mb = Int64(10000), absolute_gap_limit = Float64(1e-4), relative_gap_limit = Float64(0.0), random_seed = Int32(1), permute_variable_randomly = false, permute_presolve_constraint_order = false, use_absl_random = false, log_search_progress = false, log_frequency_in_seconds = Float64(-1), model_reduction_log_frequency_in_seconds = Float64(5), log_subsolver_statistics = false, log_prefix = "", log_to_stdout = true, log_to_response = false, use_pb_resolution = false, minimize_reduction_during_pb_resolution = false, count_assumption_levels_in_lbd = true, presolve_bve_threshold = Int32(500), presolve_bve_clause_weight = Int32(3), probing_deterministic_time_limit = Float64(1), presolve_probing_deterministic_time_limit = Float64(30.0), presolve_blocked_clause = true, presolve_use_bva = true, presolve_bva_threshold = Int32(1), max_presolve_iterations = Int32(3), cp_model_presolve = true, cp_model_probing_level = Int32(2), cp_model_use_sat_presolve = true, use_sat_inprocessing = false, detect_table_with_cost = false, table_compression_level = Int32(2), expand_alldiff_constraints = false, expand_reservoir_constraints = true, disable_constraint_expansion = false, encode_complex_linear_constraint_with_integer = false, merge_no_overlap_work_limit = Float64(1e12), merge_at_most_one_work_limit = Float64(1e8), presolve_substitution_level = Int32(1), presolve_extract_integer_enforcement = false, presolve_inclusion_work_limit = Int64(100000000), ignore_names = true, infer_all_diffs = true, find_big_linear_overlap = true, num_workers = Int32(0), num_search_workers = Int32(0), min_num_lns_workers = Int32(2), subsolvers = Vector{String}(), extra_subsolvers = Vector{String}(), ignore_subsolvers = Vector{String}(), subsolver_params = Vector{SatParameters}(), interleave_search = false, interleave_batch_size = Int32(0), share_objective_bounds = true, share_level_zero_bounds = true, share_binary_clauses = true, debug_postsolve_with_full_solver = false, debug_max_num_presolve_operations = Int32(0), debug_crash_on_bad_hint = false, use_optimization_hints = true, minimize_core = true, find_multiple_cores = true, cover_optimization = true, max_sat_assumption_order = var"SatParameters.MaxSatAssumptionOrder".DEFAULT_ASSUMPTION_ORDER, max_sat_reverse_assumption_order = false, max_sat_stratification = var"SatParameters.MaxSatStratificationAlgorithm".STRATIFICATION_DESCENT, propagation_loop_detection_factor = Float64(10.0), use_precedences_in_disjunctive_constraint = true, max_size_to_create_precedence_literals_in_disjunctive = Int32(60), use_strong_propagation_in_disjunctive = false, use_overload_checker_in_cumulative = false, use_timetable_edge_finding_in_cumulative = false, use_hard_precedences_in_cumulative = false, exploit_all_precedences = false, use_disjunctive_constraint_in_cumulative = true, use_timetabling_in_no_overlap_2d = false, use_energetic_reasoning_in_no_overlap_2d = false, use_pairwise_reasoning_in_no_overlap_2d = false, use_dual_scheduling_heuristics = true, linearization_level = Int32(1), boolean_encoding_level = Int32(1), max_domain_size_when_encoding_eq_neq_constraints = Int32(16), max_num_cuts = Int32(10000), cut_level = Int32(1), only_add_cuts_at_level_zero = false, add_objective_cut = false, add_cg_cuts = true, add_mir_cuts = true, add_zero_half_cuts = true, add_clique_cuts = true, max_all_diff_cut_size = Int32(64), add_lin_max_cuts = true, max_integer_rounding_scaling = Int32(600), add_lp_constraints_lazily = true, root_lp_iterations = Int32(2000), min_orthogonality_for_lp_constraints = Float64(0.05), max_cut_rounds_at_level_zero = Int32(1), max_consecutive_inactive_count = Int32(100), cut_max_active_count_value = Float64(1e10), cut_active_count_decay = Float64(0.8), cut_cleanup_target = Int32(1000), new_constraints_batch_size = Int32(50), search_branching = var"SatParameters.SearchBranching".AUTOMATIC_SEARCH, hint_conflict_limit = Int32(10), repair_hint = false, fix_variables_to_their_hinted_value = false, exploit_integer_lp_solution = true, exploit_all_lp_solution = true, exploit_best_solution = false, exploit_relaxation_solution = false, exploit_objective = true, probing_period_at_root = Int64(0), use_probing_search = false, use_shaving_in_probing_search = true, shaving_search_deterministic_time = Float64(0.001), use_objective_lb_search = false, use_objective_shaving_search = false, pseudo_cost_reliability_threshold = Int64(100), optimize_with_core = false, optimize_with_lb_tree_search = false, binary_search_num_conflicts = Int32(-1), optimize_with_max_hs = false, test_feasibility_jump = false, feasibility_jump_max_num_values_scanned = Int64(4096), feasibility_jump_protect_linear_feasibility = true, feasibility_jump_decay = Float64(1.0), feasibility_jump_var_randomization_probability = Float64(0.0), feasibility_jump_var_perburbation_range_ratio = Float64(0.2), feasibility_jump_enable_restarts = true, num_violation_ls = Int32(0), violation_ls_perturbation_period = Int32(100), shared_tree_num_workers = Int32(0), use_shared_tree_search = false, shared_tree_worker_objective_split_probability = Float64(0.5), shared_tree_max_nodes_per_worker = Int32(128), shared_tree_split_strategy = var"SatParameters.SharedTreeSplitStrategy".SPLIT_STRATEGY_AUTO, enumerate_all_solutions = false, keep_all_feasible_solutions_in_presolve = false, fill_tightened_domains_in_response = false, fill_additional_solutions_in_response = false, instantiate_all_variables = true, auto_detect_greater_than_at_least_one_of = true, stop_after_first_solution = false, stop_after_presolve = false, stop_after_root_propagation = false, use_lns_only = false, solution_pool_size = Int32(3), use_rins_lns = true, use_feasibility_pump = true, use_lb_relax_lns = false, fp_rounding = var"SatParameters.FPRoundingMethod".PROPAGATION_ASSISTED, diversify_lns_params = false, randomize_search = false, search_randomization_tolerance = Int64(0), use_optional_variables = false, use_exact_lp_reason = true, use_branching_in_lp = false, use_combined_no_overlap = false, catch_sigint_signal = true, use_implied_bounds = true, polish_lp_solution = false, convert_intervals = true, symmetry_level = Int32(2), new_linear_propagation = false, linear_split_size = Int32(100), mip_max_bound = Float64(1e7), mip_var_scaling = Float64(1.0), mip_scale_large_domain = false, mip_automatically_scale_variables = true, only_solve_ip = false, mip_wanted_precision = Float64(1e-6), mip_max_activity_exponent = Int32(53), mip_check_precision = Float64(1e-4), mip_compute_true_objective_bound = true, mip_max_valid_magnitude = Float64(1e30), mip_drop_tolerance = Float64(1e-16)) -PB.field_numbers(::Type{SatParameters}) = (;name = 171, preferred_variable_order = 1, initial_polarity = 2, use_phase_saving = 44, polarity_rephase_increment = 168, random_polarity_ratio = 45, random_branches_ratio = 32, use_erwa_heuristic = 75, initial_variables_activity = 76, also_bump_variables_in_conflict_reasons = 77, minimization_algorithm = 4, binary_minimization_algorithm = 34, subsumption_during_conflict_analysis = 56, clause_cleanup_period = 11, clause_cleanup_target = 13, clause_cleanup_ratio = 190, clause_cleanup_protection = 58, clause_cleanup_lbd_bound = 59, clause_cleanup_ordering = 60, pb_cleanup_increment = 46, pb_cleanup_ratio = 47, minimize_with_propagation_restart_period = 96, minimize_with_propagation_num_decisions = 97, variable_activity_decay = 15, max_variable_activity_value = 16, glucose_max_decay = 22, glucose_decay_increment = 23, glucose_decay_increment_period = 24, clause_activity_decay = 17, max_clause_activity_value = 18, restart_algorithms = 61, default_restart_algorithms = 70, restart_period = 30, restart_running_window_size = 62, restart_dl_average_ratio = 63, restart_lbd_average_ratio = 71, use_blocking_restart = 64, blocking_restart_window_size = 65, blocking_restart_multiplier = 66, num_conflicts_before_strategy_changes = 68, strategy_change_increase_ratio = 69, max_time_in_seconds = 36, max_deterministic_time = 67, max_number_of_conflicts = 37, max_memory_in_mb = 40, absolute_gap_limit = 159, relative_gap_limit = 160, random_seed = 31, permute_variable_randomly = 178, permute_presolve_constraint_order = 179, use_absl_random = 180, log_search_progress = 41, log_frequency_in_seconds = 212, model_reduction_log_frequency_in_seconds = 218, log_subsolver_statistics = 189, log_prefix = 185, log_to_stdout = 186, log_to_response = 187, use_pb_resolution = 43, minimize_reduction_during_pb_resolution = 48, count_assumption_levels_in_lbd = 49, presolve_bve_threshold = 54, presolve_bve_clause_weight = 55, probing_deterministic_time_limit = 226, presolve_probing_deterministic_time_limit = 57, presolve_blocked_clause = 88, presolve_use_bva = 72, presolve_bva_threshold = 73, max_presolve_iterations = 138, cp_model_presolve = 86, cp_model_probing_level = 110, cp_model_use_sat_presolve = 93, use_sat_inprocessing = 163, detect_table_with_cost = 216, table_compression_level = 217, expand_alldiff_constraints = 170, expand_reservoir_constraints = 182, disable_constraint_expansion = 181, encode_complex_linear_constraint_with_integer = 223, merge_no_overlap_work_limit = 145, merge_at_most_one_work_limit = 146, presolve_substitution_level = 147, presolve_extract_integer_enforcement = 174, presolve_inclusion_work_limit = 201, ignore_names = 202, infer_all_diffs = 233, find_big_linear_overlap = 234, num_workers = 206, num_search_workers = 100, min_num_lns_workers = 211, subsolvers = 207, extra_subsolvers = 219, ignore_subsolvers = 209, subsolver_params = 210, interleave_search = 136, interleave_batch_size = 134, share_objective_bounds = 113, share_level_zero_bounds = 114, share_binary_clauses = 203, debug_postsolve_with_full_solver = 162, debug_max_num_presolve_operations = 151, debug_crash_on_bad_hint = 195, use_optimization_hints = 35, minimize_core = 50, find_multiple_cores = 84, cover_optimization = 89, max_sat_assumption_order = 51, max_sat_reverse_assumption_order = 52, max_sat_stratification = 53, propagation_loop_detection_factor = 221, use_precedences_in_disjunctive_constraint = 74, max_size_to_create_precedence_literals_in_disjunctive = 229, use_strong_propagation_in_disjunctive = 230, use_overload_checker_in_cumulative = 78, use_timetable_edge_finding_in_cumulative = 79, use_hard_precedences_in_cumulative = 215, exploit_all_precedences = 220, use_disjunctive_constraint_in_cumulative = 80, use_timetabling_in_no_overlap_2d = 200, use_energetic_reasoning_in_no_overlap_2d = 213, use_pairwise_reasoning_in_no_overlap_2d = 251, use_dual_scheduling_heuristics = 214, linearization_level = 90, boolean_encoding_level = 107, max_domain_size_when_encoding_eq_neq_constraints = 191, max_num_cuts = 91, cut_level = 196, only_add_cuts_at_level_zero = 92, add_objective_cut = 197, add_cg_cuts = 117, add_mir_cuts = 120, add_zero_half_cuts = 169, add_clique_cuts = 172, max_all_diff_cut_size = 148, add_lin_max_cuts = 152, max_integer_rounding_scaling = 119, add_lp_constraints_lazily = 112, root_lp_iterations = 227, min_orthogonality_for_lp_constraints = 115, max_cut_rounds_at_level_zero = 154, max_consecutive_inactive_count = 121, cut_max_active_count_value = 155, cut_active_count_decay = 156, cut_cleanup_target = 157, new_constraints_batch_size = 122, search_branching = 82, hint_conflict_limit = 153, repair_hint = 167, fix_variables_to_their_hinted_value = 192, exploit_integer_lp_solution = 94, exploit_all_lp_solution = 116, exploit_best_solution = 130, exploit_relaxation_solution = 161, exploit_objective = 131, probing_period_at_root = 142, use_probing_search = 176, use_shaving_in_probing_search = 204, shaving_search_deterministic_time = 205, use_objective_lb_search = 228, use_objective_shaving_search = 253, pseudo_cost_reliability_threshold = 123, optimize_with_core = 83, optimize_with_lb_tree_search = 188, binary_search_num_conflicts = 99, optimize_with_max_hs = 85, test_feasibility_jump = 240, feasibility_jump_max_num_values_scanned = 245, feasibility_jump_protect_linear_feasibility = 246, feasibility_jump_decay = 242, feasibility_jump_var_randomization_probability = 247, feasibility_jump_var_perburbation_range_ratio = 248, feasibility_jump_enable_restarts = 250, num_violation_ls = 244, violation_ls_perturbation_period = 249, shared_tree_num_workers = 235, use_shared_tree_search = 236, shared_tree_worker_objective_split_probability = 237, shared_tree_max_nodes_per_worker = 238, shared_tree_split_strategy = 239, enumerate_all_solutions = 87, keep_all_feasible_solutions_in_presolve = 173, fill_tightened_domains_in_response = 132, fill_additional_solutions_in_response = 194, instantiate_all_variables = 106, auto_detect_greater_than_at_least_one_of = 95, stop_after_first_solution = 98, stop_after_presolve = 149, stop_after_root_propagation = 252, use_lns_only = 101, solution_pool_size = 193, use_rins_lns = 129, use_feasibility_pump = 164, use_lb_relax_lns = 255, fp_rounding = 165, diversify_lns_params = 137, randomize_search = 103, search_randomization_tolerance = 104, use_optional_variables = 108, use_exact_lp_reason = 109, use_branching_in_lp = 139, use_combined_no_overlap = 133, catch_sigint_signal = 135, use_implied_bounds = 144, polish_lp_solution = 175, convert_intervals = 177, symmetry_level = 183, new_linear_propagation = 224, linear_split_size = 256, mip_max_bound = 124, mip_var_scaling = 125, mip_scale_large_domain = 225, mip_automatically_scale_variables = 166, only_solve_ip = 222, mip_wanted_precision = 126, mip_max_activity_exponent = 127, mip_check_precision = 128, mip_compute_true_objective_bound = 198, mip_max_valid_magnitude = 199, mip_drop_tolerance = 232) +PB.default_values(::Type{SatParameters}) = (;name = "", preferred_variable_order = var"SatParameters.VariableOrder".IN_ORDER, initial_polarity = var"SatParameters.Polarity".POLARITY_FALSE, use_phase_saving = true, polarity_rephase_increment = Int32(1000), random_polarity_ratio = Float64(0.0), random_branches_ratio = Float64(0.0), use_erwa_heuristic = false, initial_variables_activity = Float64(0.0), also_bump_variables_in_conflict_reasons = false, minimization_algorithm = var"SatParameters.ConflictMinimizationAlgorithm".RECURSIVE, binary_minimization_algorithm = var"SatParameters.BinaryMinizationAlgorithm".BINARY_MINIMIZATION_FIRST, subsumption_during_conflict_analysis = true, clause_cleanup_period = Int32(10000), clause_cleanup_target = Int32(0), clause_cleanup_ratio = Float64(0.5), clause_cleanup_protection = var"SatParameters.ClauseProtection".PROTECTION_NONE, clause_cleanup_lbd_bound = Int32(5), clause_cleanup_ordering = var"SatParameters.ClauseOrdering".CLAUSE_ACTIVITY, pb_cleanup_increment = Int32(200), pb_cleanup_ratio = Float64(0.5), minimize_with_propagation_restart_period = Int32(10), minimize_with_propagation_num_decisions = Int32(1000), variable_activity_decay = Float64(0.8), max_variable_activity_value = Float64(1e100), glucose_max_decay = Float64(0.95), glucose_decay_increment = Float64(0.01), glucose_decay_increment_period = Int32(5000), clause_activity_decay = Float64(0.999), max_clause_activity_value = Float64(1e20), restart_algorithms = Vector{var"SatParameters.RestartAlgorithm".T}(), default_restart_algorithms = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART", restart_period = Int32(50), restart_running_window_size = Int32(50), restart_dl_average_ratio = Float64(1.0), restart_lbd_average_ratio = Float64(1.0), use_blocking_restart = false, blocking_restart_window_size = Int32(5000), blocking_restart_multiplier = Float64(1.4), num_conflicts_before_strategy_changes = Int32(0), strategy_change_increase_ratio = Float64(0.0), max_time_in_seconds = Float64(Inf), max_deterministic_time = Float64(Inf), max_number_of_conflicts = Int64(9223372036854775807), max_memory_in_mb = Int64(10000), absolute_gap_limit = Float64(1e-4), relative_gap_limit = Float64(0.0), random_seed = Int32(1), permute_variable_randomly = false, permute_presolve_constraint_order = false, use_absl_random = false, log_search_progress = false, log_frequency_in_seconds = Float64(-1), model_reduction_log_frequency_in_seconds = Float64(5), log_subsolver_statistics = false, log_prefix = "", log_to_stdout = true, log_to_response = false, use_pb_resolution = false, minimize_reduction_during_pb_resolution = false, count_assumption_levels_in_lbd = true, presolve_bve_threshold = Int32(500), presolve_bve_clause_weight = Int32(3), probing_deterministic_time_limit = Float64(1), presolve_probing_deterministic_time_limit = Float64(30.0), presolve_blocked_clause = true, presolve_use_bva = true, presolve_bva_threshold = Int32(1), max_presolve_iterations = Int32(3), cp_model_presolve = true, cp_model_probing_level = Int32(2), cp_model_use_sat_presolve = true, use_sat_inprocessing = false, detect_table_with_cost = false, table_compression_level = Int32(2), expand_alldiff_constraints = false, expand_reservoir_constraints = true, disable_constraint_expansion = false, encode_complex_linear_constraint_with_integer = false, merge_no_overlap_work_limit = Float64(1e12), merge_at_most_one_work_limit = Float64(1e8), presolve_substitution_level = Int32(1), presolve_extract_integer_enforcement = false, presolve_inclusion_work_limit = Int64(100000000), ignore_names = true, infer_all_diffs = true, find_big_linear_overlap = true, num_workers = Int32(0), num_search_workers = Int32(0), min_num_lns_workers = Int32(2), subsolvers = Vector{String}(), extra_subsolvers = Vector{String}(), ignore_subsolvers = Vector{String}(), subsolver_params = Vector{SatParameters}(), interleave_search = false, interleave_batch_size = Int32(0), share_objective_bounds = true, share_level_zero_bounds = true, share_binary_clauses = true, debug_postsolve_with_full_solver = false, debug_max_num_presolve_operations = Int32(0), debug_crash_on_bad_hint = false, use_optimization_hints = true, minimize_core = true, find_multiple_cores = true, cover_optimization = true, max_sat_assumption_order = var"SatParameters.MaxSatAssumptionOrder".DEFAULT_ASSUMPTION_ORDER, max_sat_reverse_assumption_order = false, max_sat_stratification = var"SatParameters.MaxSatStratificationAlgorithm".STRATIFICATION_DESCENT, propagation_loop_detection_factor = Float64(10.0), use_precedences_in_disjunctive_constraint = true, max_size_to_create_precedence_literals_in_disjunctive = Int32(60), use_strong_propagation_in_disjunctive = false, use_overload_checker_in_cumulative = false, use_timetable_edge_finding_in_cumulative = false, use_hard_precedences_in_cumulative = false, exploit_all_precedences = false, use_disjunctive_constraint_in_cumulative = true, use_timetabling_in_no_overlap_2d = false, use_energetic_reasoning_in_no_overlap_2d = false, use_pairwise_reasoning_in_no_overlap_2d = false, use_dual_scheduling_heuristics = true, linearization_level = Int32(1), boolean_encoding_level = Int32(1), max_domain_size_when_encoding_eq_neq_constraints = Int32(16), max_num_cuts = Int32(10000), cut_level = Int32(1), only_add_cuts_at_level_zero = false, add_objective_cut = false, add_cg_cuts = true, add_mir_cuts = true, add_zero_half_cuts = true, add_clique_cuts = true, max_all_diff_cut_size = Int32(64), add_lin_max_cuts = true, max_integer_rounding_scaling = Int32(600), add_lp_constraints_lazily = true, root_lp_iterations = Int32(2000), min_orthogonality_for_lp_constraints = Float64(0.05), max_cut_rounds_at_level_zero = Int32(1), max_consecutive_inactive_count = Int32(100), cut_max_active_count_value = Float64(1e10), cut_active_count_decay = Float64(0.8), cut_cleanup_target = Int32(1000), new_constraints_batch_size = Int32(50), search_branching = var"SatParameters.SearchBranching".AUTOMATIC_SEARCH, hint_conflict_limit = Int32(10), repair_hint = false, fix_variables_to_their_hinted_value = false, exploit_integer_lp_solution = true, exploit_all_lp_solution = true, exploit_best_solution = false, exploit_relaxation_solution = false, exploit_objective = true, probing_period_at_root = Int64(0), use_probing_search = false, shaving_deterministic_time_in_probing_search = true, shaving_search_deterministic_time = Float64(0.001), use_objective_lb_search = false, use_objective_shaving_search = false, pseudo_cost_reliability_threshold = Int64(100), optimize_with_core = false, optimize_with_lb_tree_search = false, binary_search_num_conflicts = Int32(-1), optimize_with_max_hs = false, test_feasibility_jump = false, feasibility_jump_max_num_values_scanned = Int64(4096), feasibility_jump_protect_linear_feasibility = true, feasibility_jump_decay = Float64(1.0), feasibility_jump_var_randomization_probability = Float64(0.0), feasibility_jump_var_perburbation_range_ratio = Float64(0.2), feasibility_jump_enable_restarts = true, num_violation_ls = Int32(0), violation_ls_perturbation_period = Int32(100), shared_tree_num_workers = Int32(0), use_shared_tree_search = false, shared_tree_worker_objective_split_probability = Float64(0.5), shared_tree_max_nodes_per_worker = Int32(128), shared_tree_split_strategy = var"SatParameters.SharedTreeSplitStrategy".SPLIT_STRATEGY_AUTO, enumerate_all_solutions = false, keep_all_feasible_solutions_in_presolve = false, fill_tightened_domains_in_response = false, fill_additional_solutions_in_response = false, instantiate_all_variables = true, auto_detect_greater_than_at_least_one_of = true, stop_after_first_solution = false, stop_after_presolve = false, stop_after_root_propagation = false, use_lns_only = false, solution_pool_size = Int32(3), use_rins_lns = true, use_feasibility_pump = true, use_lb_relax_lns = false, fp_rounding = var"SatParameters.FPRoundingMethod".PROPAGATION_ASSISTED, diversify_lns_params = false, randomize_search = false, search_randomization_tolerance = Int64(0), use_optional_variables = false, use_exact_lp_reason = true, use_branching_in_lp = false, use_combined_no_overlap = false, catch_sigint_signal = true, use_implied_bounds = true, polish_lp_solution = false, convert_intervals = true, symmetry_level = Int32(2), new_linear_propagation = false, linear_split_size = Int32(100), mip_max_bound = Float64(1e7), mip_var_scaling = Float64(1.0), mip_scale_large_domain = false, mip_automatically_scale_variables = true, only_solve_ip = false, mip_wanted_precision = Float64(1e-6), mip_max_activity_exponent = Int32(53), mip_check_precision = Float64(1e-4), mip_compute_true_objective_bound = true, mip_max_valid_magnitude = Float64(1e30), mip_drop_tolerance = Float64(1e-16)) +PB.field_numbers(::Type{SatParameters}) = (;name = 171, preferred_variable_order = 1, initial_polarity = 2, use_phase_saving = 44, polarity_rephase_increment = 168, random_polarity_ratio = 45, random_branches_ratio = 32, use_erwa_heuristic = 75, initial_variables_activity = 76, also_bump_variables_in_conflict_reasons = 77, minimization_algorithm = 4, binary_minimization_algorithm = 34, subsumption_during_conflict_analysis = 56, clause_cleanup_period = 11, clause_cleanup_target = 13, clause_cleanup_ratio = 190, clause_cleanup_protection = 58, clause_cleanup_lbd_bound = 59, clause_cleanup_ordering = 60, pb_cleanup_increment = 46, pb_cleanup_ratio = 47, minimize_with_propagation_restart_period = 96, minimize_with_propagation_num_decisions = 97, variable_activity_decay = 15, max_variable_activity_value = 16, glucose_max_decay = 22, glucose_decay_increment = 23, glucose_decay_increment_period = 24, clause_activity_decay = 17, max_clause_activity_value = 18, restart_algorithms = 61, default_restart_algorithms = 70, restart_period = 30, restart_running_window_size = 62, restart_dl_average_ratio = 63, restart_lbd_average_ratio = 71, use_blocking_restart = 64, blocking_restart_window_size = 65, blocking_restart_multiplier = 66, num_conflicts_before_strategy_changes = 68, strategy_change_increase_ratio = 69, max_time_in_seconds = 36, max_deterministic_time = 67, max_number_of_conflicts = 37, max_memory_in_mb = 40, absolute_gap_limit = 159, relative_gap_limit = 160, random_seed = 31, permute_variable_randomly = 178, permute_presolve_constraint_order = 179, use_absl_random = 180, log_search_progress = 41, log_frequency_in_seconds = 212, model_reduction_log_frequency_in_seconds = 218, log_subsolver_statistics = 189, log_prefix = 185, log_to_stdout = 186, log_to_response = 187, use_pb_resolution = 43, minimize_reduction_during_pb_resolution = 48, count_assumption_levels_in_lbd = 49, presolve_bve_threshold = 54, presolve_bve_clause_weight = 55, probing_deterministic_time_limit = 226, presolve_probing_deterministic_time_limit = 57, presolve_blocked_clause = 88, presolve_use_bva = 72, presolve_bva_threshold = 73, max_presolve_iterations = 138, cp_model_presolve = 86, cp_model_probing_level = 110, cp_model_use_sat_presolve = 93, use_sat_inprocessing = 163, detect_table_with_cost = 216, table_compression_level = 217, expand_alldiff_constraints = 170, expand_reservoir_constraints = 182, disable_constraint_expansion = 181, encode_complex_linear_constraint_with_integer = 223, merge_no_overlap_work_limit = 145, merge_at_most_one_work_limit = 146, presolve_substitution_level = 147, presolve_extract_integer_enforcement = 174, presolve_inclusion_work_limit = 201, ignore_names = 202, infer_all_diffs = 233, find_big_linear_overlap = 234, num_workers = 206, num_search_workers = 100, min_num_lns_workers = 211, subsolvers = 207, extra_subsolvers = 219, ignore_subsolvers = 209, subsolver_params = 210, interleave_search = 136, interleave_batch_size = 134, share_objective_bounds = 113, share_level_zero_bounds = 114, share_binary_clauses = 203, debug_postsolve_with_full_solver = 162, debug_max_num_presolve_operations = 151, debug_crash_on_bad_hint = 195, use_optimization_hints = 35, minimize_core = 50, find_multiple_cores = 84, cover_optimization = 89, max_sat_assumption_order = 51, max_sat_reverse_assumption_order = 52, max_sat_stratification = 53, propagation_loop_detection_factor = 221, use_precedences_in_disjunctive_constraint = 74, max_size_to_create_precedence_literals_in_disjunctive = 229, use_strong_propagation_in_disjunctive = 230, use_overload_checker_in_cumulative = 78, use_timetable_edge_finding_in_cumulative = 79, use_hard_precedences_in_cumulative = 215, exploit_all_precedences = 220, use_disjunctive_constraint_in_cumulative = 80, use_timetabling_in_no_overlap_2d = 200, use_energetic_reasoning_in_no_overlap_2d = 213, use_pairwise_reasoning_in_no_overlap_2d = 251, use_dual_scheduling_heuristics = 214, linearization_level = 90, boolean_encoding_level = 107, max_domain_size_when_encoding_eq_neq_constraints = 191, max_num_cuts = 91, cut_level = 196, only_add_cuts_at_level_zero = 92, add_objective_cut = 197, add_cg_cuts = 117, add_mir_cuts = 120, add_zero_half_cuts = 169, add_clique_cuts = 172, max_all_diff_cut_size = 148, add_lin_max_cuts = 152, max_integer_rounding_scaling = 119, add_lp_constraints_lazily = 112, root_lp_iterations = 227, min_orthogonality_for_lp_constraints = 115, max_cut_rounds_at_level_zero = 154, max_consecutive_inactive_count = 121, cut_max_active_count_value = 155, cut_active_count_decay = 156, cut_cleanup_target = 157, new_constraints_batch_size = 122, search_branching = 82, hint_conflict_limit = 153, repair_hint = 167, fix_variables_to_their_hinted_value = 192, exploit_integer_lp_solution = 94, exploit_all_lp_solution = 116, exploit_best_solution = 130, exploit_relaxation_solution = 161, exploit_objective = 131, probing_period_at_root = 142, use_probing_search = 176, shaving_deterministic_time_in_probing_search = 204, shaving_search_deterministic_time = 205, use_objective_lb_search = 228, use_objective_shaving_search = 253, pseudo_cost_reliability_threshold = 123, optimize_with_core = 83, optimize_with_lb_tree_search = 188, binary_search_num_conflicts = 99, optimize_with_max_hs = 85, test_feasibility_jump = 240, feasibility_jump_max_num_values_scanned = 245, feasibility_jump_protect_linear_feasibility = 246, feasibility_jump_decay = 242, feasibility_jump_var_randomization_probability = 247, feasibility_jump_var_perburbation_range_ratio = 248, feasibility_jump_enable_restarts = 250, num_violation_ls = 244, violation_ls_perturbation_period = 249, shared_tree_num_workers = 235, use_shared_tree_search = 236, shared_tree_worker_objective_split_probability = 237, shared_tree_max_nodes_per_worker = 238, shared_tree_split_strategy = 239, enumerate_all_solutions = 87, keep_all_feasible_solutions_in_presolve = 173, fill_tightened_domains_in_response = 132, fill_additional_solutions_in_response = 194, instantiate_all_variables = 106, auto_detect_greater_than_at_least_one_of = 95, stop_after_first_solution = 98, stop_after_presolve = 149, stop_after_root_propagation = 252, use_lns_only = 101, solution_pool_size = 193, use_rins_lns = 129, use_feasibility_pump = 164, use_lb_relax_lns = 255, fp_rounding = 165, diversify_lns_params = 137, randomize_search = 103, search_randomization_tolerance = 104, use_optional_variables = 108, use_exact_lp_reason = 109, use_branching_in_lp = 139, use_combined_no_overlap = 133, catch_sigint_signal = 135, use_implied_bounds = 144, polish_lp_solution = 175, convert_intervals = 177, symmetry_level = 183, new_linear_propagation = 224, linear_split_size = 256, mip_max_bound = 124, mip_var_scaling = 125, mip_scale_large_domain = 225, mip_automatically_scale_variables = 166, only_solve_ip = 222, mip_wanted_precision = 126, mip_max_activity_exponent = 127, mip_check_precision = 128, mip_compute_true_objective_bound = 198, mip_max_valid_magnitude = 199, mip_drop_tolerance = 232) function PB.decode(d::PB.AbstractProtoDecoder, ::Type{<:SatParameters}) name = "" @@ -423,7 +423,7 @@ function PB.decode(d::PB.AbstractProtoDecoder, ::Type{<:SatParameters}) exploit_objective = true probing_period_at_root = Int64(0) use_probing_search = false - use_shaving_in_probing_search = true + shaving_deterministic_time_in_probing_search = Float64(0.001) shaving_search_deterministic_time = Float64(0.001) use_objective_lb_search = false use_objective_shaving_search = false @@ -801,7 +801,7 @@ function PB.decode(d::PB.AbstractProtoDecoder, ::Type{<:SatParameters}) elseif field_number == 176 use_probing_search = PB.decode(d, Bool) elseif field_number == 204 - use_shaving_in_probing_search = PB.decode(d, Bool) + shaving_deterministic_time_in_probing_search = PB.decode(d, Float64) elseif field_number == 205 shaving_search_deterministic_time = PB.decode(d, Float64) elseif field_number == 228 @@ -930,7 +930,7 @@ function PB.decode(d::PB.AbstractProtoDecoder, ::Type{<:SatParameters}) PB.skip(d, wire_type) end end - return SatParameters(name, preferred_variable_order, initial_polarity, use_phase_saving, polarity_rephase_increment, random_polarity_ratio, random_branches_ratio, use_erwa_heuristic, initial_variables_activity, also_bump_variables_in_conflict_reasons, minimization_algorithm, binary_minimization_algorithm, subsumption_during_conflict_analysis, clause_cleanup_period, clause_cleanup_target, clause_cleanup_ratio, clause_cleanup_protection, clause_cleanup_lbd_bound, clause_cleanup_ordering, pb_cleanup_increment, pb_cleanup_ratio, minimize_with_propagation_restart_period, minimize_with_propagation_num_decisions, variable_activity_decay, max_variable_activity_value, glucose_max_decay, glucose_decay_increment, glucose_decay_increment_period, clause_activity_decay, max_clause_activity_value, restart_algorithms[], default_restart_algorithms, restart_period, restart_running_window_size, restart_dl_average_ratio, restart_lbd_average_ratio, use_blocking_restart, blocking_restart_window_size, blocking_restart_multiplier, num_conflicts_before_strategy_changes, strategy_change_increase_ratio, max_time_in_seconds, max_deterministic_time, max_number_of_conflicts, max_memory_in_mb, absolute_gap_limit, relative_gap_limit, random_seed, permute_variable_randomly, permute_presolve_constraint_order, use_absl_random, log_search_progress, log_frequency_in_seconds, model_reduction_log_frequency_in_seconds, log_subsolver_statistics, log_prefix, log_to_stdout, log_to_response, use_pb_resolution, minimize_reduction_during_pb_resolution, count_assumption_levels_in_lbd, presolve_bve_threshold, presolve_bve_clause_weight, probing_deterministic_time_limit, presolve_probing_deterministic_time_limit, presolve_blocked_clause, presolve_use_bva, presolve_bva_threshold, max_presolve_iterations, cp_model_presolve, cp_model_probing_level, cp_model_use_sat_presolve, use_sat_inprocessing, detect_table_with_cost, table_compression_level, expand_alldiff_constraints, expand_reservoir_constraints, disable_constraint_expansion, encode_complex_linear_constraint_with_integer, merge_no_overlap_work_limit, merge_at_most_one_work_limit, presolve_substitution_level, presolve_extract_integer_enforcement, presolve_inclusion_work_limit, ignore_names, infer_all_diffs, find_big_linear_overlap, num_workers, num_search_workers, min_num_lns_workers, subsolvers[], extra_subsolvers[], ignore_subsolvers[], subsolver_params[], interleave_search, interleave_batch_size, share_objective_bounds, share_level_zero_bounds, share_binary_clauses, debug_postsolve_with_full_solver, debug_max_num_presolve_operations, debug_crash_on_bad_hint, use_optimization_hints, minimize_core, find_multiple_cores, cover_optimization, max_sat_assumption_order, max_sat_reverse_assumption_order, max_sat_stratification, propagation_loop_detection_factor, use_precedences_in_disjunctive_constraint, max_size_to_create_precedence_literals_in_disjunctive, use_strong_propagation_in_disjunctive, use_overload_checker_in_cumulative, use_timetable_edge_finding_in_cumulative, use_hard_precedences_in_cumulative, exploit_all_precedences, use_disjunctive_constraint_in_cumulative, use_timetabling_in_no_overlap_2d, use_energetic_reasoning_in_no_overlap_2d, use_pairwise_reasoning_in_no_overlap_2d, use_dual_scheduling_heuristics, linearization_level, boolean_encoding_level, max_domain_size_when_encoding_eq_neq_constraints, max_num_cuts, cut_level, only_add_cuts_at_level_zero, add_objective_cut, add_cg_cuts, add_mir_cuts, add_zero_half_cuts, add_clique_cuts, max_all_diff_cut_size, add_lin_max_cuts, max_integer_rounding_scaling, add_lp_constraints_lazily, root_lp_iterations, min_orthogonality_for_lp_constraints, max_cut_rounds_at_level_zero, max_consecutive_inactive_count, cut_max_active_count_value, cut_active_count_decay, cut_cleanup_target, new_constraints_batch_size, search_branching, hint_conflict_limit, repair_hint, fix_variables_to_their_hinted_value, exploit_integer_lp_solution, exploit_all_lp_solution, exploit_best_solution, exploit_relaxation_solution, exploit_objective, probing_period_at_root, use_probing_search, use_shaving_in_probing_search, shaving_search_deterministic_time, use_objective_lb_search, use_objective_shaving_search, pseudo_cost_reliability_threshold, optimize_with_core, optimize_with_lb_tree_search, binary_search_num_conflicts, optimize_with_max_hs, test_feasibility_jump, feasibility_jump_max_num_values_scanned, feasibility_jump_protect_linear_feasibility, feasibility_jump_decay, feasibility_jump_var_randomization_probability, feasibility_jump_var_perburbation_range_ratio, feasibility_jump_enable_restarts, num_violation_ls, violation_ls_perturbation_period, shared_tree_num_workers, use_shared_tree_search, shared_tree_worker_objective_split_probability, shared_tree_max_nodes_per_worker, shared_tree_split_strategy, enumerate_all_solutions, keep_all_feasible_solutions_in_presolve, fill_tightened_domains_in_response, fill_additional_solutions_in_response, instantiate_all_variables, auto_detect_greater_than_at_least_one_of, stop_after_first_solution, stop_after_presolve, stop_after_root_propagation, use_lns_only, solution_pool_size, use_rins_lns, use_feasibility_pump, use_lb_relax_lns, fp_rounding, diversify_lns_params, randomize_search, search_randomization_tolerance, use_optional_variables, use_exact_lp_reason, use_branching_in_lp, use_combined_no_overlap, catch_sigint_signal, use_implied_bounds, polish_lp_solution, convert_intervals, symmetry_level, new_linear_propagation, linear_split_size, mip_max_bound, mip_var_scaling, mip_scale_large_domain, mip_automatically_scale_variables, only_solve_ip, mip_wanted_precision, mip_max_activity_exponent, mip_check_precision, mip_compute_true_objective_bound, mip_max_valid_magnitude, mip_drop_tolerance) + return SatParameters(name, preferred_variable_order, initial_polarity, use_phase_saving, polarity_rephase_increment, random_polarity_ratio, random_branches_ratio, use_erwa_heuristic, initial_variables_activity, also_bump_variables_in_conflict_reasons, minimization_algorithm, binary_minimization_algorithm, subsumption_during_conflict_analysis, clause_cleanup_period, clause_cleanup_target, clause_cleanup_ratio, clause_cleanup_protection, clause_cleanup_lbd_bound, clause_cleanup_ordering, pb_cleanup_increment, pb_cleanup_ratio, minimize_with_propagation_restart_period, minimize_with_propagation_num_decisions, variable_activity_decay, max_variable_activity_value, glucose_max_decay, glucose_decay_increment, glucose_decay_increment_period, clause_activity_decay, max_clause_activity_value, restart_algorithms[], default_restart_algorithms, restart_period, restart_running_window_size, restart_dl_average_ratio, restart_lbd_average_ratio, use_blocking_restart, blocking_restart_window_size, blocking_restart_multiplier, num_conflicts_before_strategy_changes, strategy_change_increase_ratio, max_time_in_seconds, max_deterministic_time, max_number_of_conflicts, max_memory_in_mb, absolute_gap_limit, relative_gap_limit, random_seed, permute_variable_randomly, permute_presolve_constraint_order, use_absl_random, log_search_progress, log_frequency_in_seconds, model_reduction_log_frequency_in_seconds, log_subsolver_statistics, log_prefix, log_to_stdout, log_to_response, use_pb_resolution, minimize_reduction_during_pb_resolution, count_assumption_levels_in_lbd, presolve_bve_threshold, presolve_bve_clause_weight, probing_deterministic_time_limit, presolve_probing_deterministic_time_limit, presolve_blocked_clause, presolve_use_bva, presolve_bva_threshold, max_presolve_iterations, cp_model_presolve, cp_model_probing_level, cp_model_use_sat_presolve, use_sat_inprocessing, detect_table_with_cost, table_compression_level, expand_alldiff_constraints, expand_reservoir_constraints, disable_constraint_expansion, encode_complex_linear_constraint_with_integer, merge_no_overlap_work_limit, merge_at_most_one_work_limit, presolve_substitution_level, presolve_extract_integer_enforcement, presolve_inclusion_work_limit, ignore_names, infer_all_diffs, find_big_linear_overlap, num_workers, num_search_workers, min_num_lns_workers, subsolvers[], extra_subsolvers[], ignore_subsolvers[], subsolver_params[], interleave_search, interleave_batch_size, share_objective_bounds, share_level_zero_bounds, share_binary_clauses, debug_postsolve_with_full_solver, debug_max_num_presolve_operations, debug_crash_on_bad_hint, use_optimization_hints, minimize_core, find_multiple_cores, cover_optimization, max_sat_assumption_order, max_sat_reverse_assumption_order, max_sat_stratification, propagation_loop_detection_factor, use_precedences_in_disjunctive_constraint, max_size_to_create_precedence_literals_in_disjunctive, use_strong_propagation_in_disjunctive, use_overload_checker_in_cumulative, use_timetable_edge_finding_in_cumulative, use_hard_precedences_in_cumulative, exploit_all_precedences, use_disjunctive_constraint_in_cumulative, use_timetabling_in_no_overlap_2d, use_energetic_reasoning_in_no_overlap_2d, use_pairwise_reasoning_in_no_overlap_2d, use_dual_scheduling_heuristics, linearization_level, boolean_encoding_level, max_domain_size_when_encoding_eq_neq_constraints, max_num_cuts, cut_level, only_add_cuts_at_level_zero, add_objective_cut, add_cg_cuts, add_mir_cuts, add_zero_half_cuts, add_clique_cuts, max_all_diff_cut_size, add_lin_max_cuts, max_integer_rounding_scaling, add_lp_constraints_lazily, root_lp_iterations, min_orthogonality_for_lp_constraints, max_cut_rounds_at_level_zero, max_consecutive_inactive_count, cut_max_active_count_value, cut_active_count_decay, cut_cleanup_target, new_constraints_batch_size, search_branching, hint_conflict_limit, repair_hint, fix_variables_to_their_hinted_value, exploit_integer_lp_solution, exploit_all_lp_solution, exploit_best_solution, exploit_relaxation_solution, exploit_objective, probing_period_at_root, use_probing_search, shaving_deterministic_time_in_probing_search, shaving_search_deterministic_time, use_objective_lb_search, use_objective_shaving_search, pseudo_cost_reliability_threshold, optimize_with_core, optimize_with_lb_tree_search, binary_search_num_conflicts, optimize_with_max_hs, test_feasibility_jump, feasibility_jump_max_num_values_scanned, feasibility_jump_protect_linear_feasibility, feasibility_jump_decay, feasibility_jump_var_randomization_probability, feasibility_jump_var_perburbation_range_ratio, feasibility_jump_enable_restarts, num_violation_ls, violation_ls_perturbation_period, shared_tree_num_workers, use_shared_tree_search, shared_tree_worker_objective_split_probability, shared_tree_max_nodes_per_worker, shared_tree_split_strategy, enumerate_all_solutions, keep_all_feasible_solutions_in_presolve, fill_tightened_domains_in_response, fill_additional_solutions_in_response, instantiate_all_variables, auto_detect_greater_than_at_least_one_of, stop_after_first_solution, stop_after_presolve, stop_after_root_propagation, use_lns_only, solution_pool_size, use_rins_lns, use_feasibility_pump, use_lb_relax_lns, fp_rounding, diversify_lns_params, randomize_search, search_randomization_tolerance, use_optional_variables, use_exact_lp_reason, use_branching_in_lp, use_combined_no_overlap, catch_sigint_signal, use_implied_bounds, polish_lp_solution, convert_intervals, symmetry_level, new_linear_propagation, linear_split_size, mip_max_bound, mip_var_scaling, mip_scale_large_domain, mip_automatically_scale_variables, only_solve_ip, mip_wanted_precision, mip_max_activity_exponent, mip_check_precision, mip_compute_true_objective_bound, mip_max_valid_magnitude, mip_drop_tolerance) end function PB.encode(e::PB.AbstractProtoEncoder, x::SatParameters) @@ -1091,8 +1091,8 @@ function PB.encode(e::PB.AbstractProtoEncoder, x::SatParameters) x.exploit_objective != true && PB.encode(e, 131, x.exploit_objective) x.probing_period_at_root != Int64(0) && PB.encode(e, 142, x.probing_period_at_root) x.use_probing_search != false && PB.encode(e, 176, x.use_probing_search) - x.use_shaving_in_probing_search != true && PB.encode(e, 204, x.use_shaving_in_probing_search) - x.shaving_search_deterministic_time != Float64(0.001) && PB.encode(e, 205, x.shaving_search_deterministic_time) + x.shaving_deterministic_time_in_probing_search != Float64(0.001) && PB.encode(e, 204, x.shaving_deterministic_time_in_probing_search) + x.shaving_search_deterministic_time != Float64(0.1) && PB.encode(e, 205, x.shaving_search_deterministic_time) x.use_objective_lb_search != false && PB.encode(e, 228, x.use_objective_lb_search) x.use_objective_shaving_search != false && PB.encode(e, 253, x.use_objective_shaving_search) x.pseudo_cost_reliability_threshold != Int64(100) && PB.encode(e, 123, x.pseudo_cost_reliability_threshold) @@ -1314,7 +1314,7 @@ function PB._encoded_size(x::SatParameters) x.exploit_objective != true && (encoded_size += PB._encoded_size(x.exploit_objective, 131)) x.probing_period_at_root != Int64(0) && (encoded_size += PB._encoded_size(x.probing_period_at_root, 142)) x.use_probing_search != false && (encoded_size += PB._encoded_size(x.use_probing_search, 176)) - x.use_shaving_in_probing_search != true && (encoded_size += PB._encoded_size(x.use_shaving_in_probing_search, 204)) + x.shaving_deterministic_time_in_probing_search != Float64(0.001) && (encoded_size += PB._encoded_size(x.shaving_deterministic_time_in_probing_search, 204)) x.shaving_search_deterministic_time != Float64(0.001) && (encoded_size += PB._encoded_size(x.shaving_search_deterministic_time, 205)) x.use_objective_lb_search != false && (encoded_size += PB._encoded_size(x.use_objective_lb_search, 228)) x.use_objective_shaving_search != false && (encoded_size += PB._encoded_size(x.use_objective_shaving_search, 253))