"""
@generated by mypy-protobuf.  Do not edit manually!
isort:skip_file
Copyright 2010-2025 Google LLC
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

LINT: LEGACY_NAMES
"""

import builtins
import collections.abc
import google.protobuf.descriptor
import google.protobuf.internal.containers
import google.protobuf.internal.enum_type_wrapper
import google.protobuf.message
import sys
import typing

if sys.version_info >= (3, 10):
    import typing as typing_extensions
else:
    import typing_extensions

DESCRIPTOR: google.protobuf.descriptor.FileDescriptor

@typing.final
class SatParameters(google.protobuf.message.Message):
    """Contains the definitions for all the sat algorithm parameters and their
    default values.

    NEXT TAG: 356
    """

    DESCRIPTOR: google.protobuf.descriptor.Descriptor

    class _VariableOrder:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _VariableOrderEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._VariableOrder.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        IN_ORDER: SatParameters._VariableOrder.ValueType  # 0
        """As specified by the problem."""
        IN_REVERSE_ORDER: SatParameters._VariableOrder.ValueType  # 1
        IN_RANDOM_ORDER: SatParameters._VariableOrder.ValueType  # 2

    class VariableOrder(_VariableOrder, metaclass=_VariableOrderEnumTypeWrapper):
        """==========================================================================
        Branching and polarity
        ==========================================================================

        Variables without activity (i.e. at the beginning of the search) will be
        tried in this preferred order.
        """

    IN_ORDER: SatParameters.VariableOrder.ValueType  # 0
    """As specified by the problem."""
    IN_REVERSE_ORDER: SatParameters.VariableOrder.ValueType  # 1
    IN_RANDOM_ORDER: SatParameters.VariableOrder.ValueType  # 2

    class _Polarity:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _PolarityEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._Polarity.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        POLARITY_TRUE: SatParameters._Polarity.ValueType  # 0
        POLARITY_FALSE: SatParameters._Polarity.ValueType  # 1
        POLARITY_RANDOM: SatParameters._Polarity.ValueType  # 2

    class Polarity(_Polarity, metaclass=_PolarityEnumTypeWrapper):
        """Specifies the initial polarity (true/false) when the solver branches on a
        variable. This can be modified later by the user, or the phase saving
        heuristic.

        Note(user): POLARITY_FALSE is usually a good choice because of the
        "natural" way to express a linear boolean problem.
        """

    POLARITY_TRUE: SatParameters.Polarity.ValueType  # 0
    POLARITY_FALSE: SatParameters.Polarity.ValueType  # 1
    POLARITY_RANDOM: SatParameters.Polarity.ValueType  # 2

    class _ConflictMinimizationAlgorithm:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _ConflictMinimizationAlgorithmEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._ConflictMinimizationAlgorithm.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        NONE: SatParameters._ConflictMinimizationAlgorithm.ValueType  # 0
        SIMPLE: SatParameters._ConflictMinimizationAlgorithm.ValueType  # 1
        RECURSIVE: SatParameters._ConflictMinimizationAlgorithm.ValueType  # 2

    class ConflictMinimizationAlgorithm(_ConflictMinimizationAlgorithm, metaclass=_ConflictMinimizationAlgorithmEnumTypeWrapper):
        """==========================================================================
        Conflict analysis
        ==========================================================================

        Do we try to minimize conflicts (greedily) when creating them.
        """

    NONE: SatParameters.ConflictMinimizationAlgorithm.ValueType  # 0
    SIMPLE: SatParameters.ConflictMinimizationAlgorithm.ValueType  # 1
    RECURSIVE: SatParameters.ConflictMinimizationAlgorithm.ValueType  # 2

    class _BinaryMinizationAlgorithm:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _BinaryMinizationAlgorithmEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._BinaryMinizationAlgorithm.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        NO_BINARY_MINIMIZATION: SatParameters._BinaryMinizationAlgorithm.ValueType  # 0
        BINARY_MINIMIZATION_FROM_UIP: SatParameters._BinaryMinizationAlgorithm.ValueType  # 1
        BINARY_MINIMIZATION_FROM_UIP_AND_DECISIONS: SatParameters._BinaryMinizationAlgorithm.ValueType  # 5

    class BinaryMinizationAlgorithm(_BinaryMinizationAlgorithm, metaclass=_BinaryMinizationAlgorithmEnumTypeWrapper):
        """Whether to expoit the binary clause to minimize learned clauses further."""

    NO_BINARY_MINIMIZATION: SatParameters.BinaryMinizationAlgorithm.ValueType  # 0
    BINARY_MINIMIZATION_FROM_UIP: SatParameters.BinaryMinizationAlgorithm.ValueType  # 1
    BINARY_MINIMIZATION_FROM_UIP_AND_DECISIONS: SatParameters.BinaryMinizationAlgorithm.ValueType  # 5

    class _ClauseOrdering:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _ClauseOrderingEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._ClauseOrdering.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        CLAUSE_ACTIVITY: SatParameters._ClauseOrdering.ValueType  # 0
        """Order clause by decreasing activity, then by increasing LBD."""
        CLAUSE_LBD: SatParameters._ClauseOrdering.ValueType  # 1
        """Order clause by increasing LBD, then by decreasing activity."""

    class ClauseOrdering(_ClauseOrdering, metaclass=_ClauseOrderingEnumTypeWrapper):
        """The clauses that will be kept during a cleanup are the ones that come
        first under this order. We always keep or exclude ties together.
        """

    CLAUSE_ACTIVITY: SatParameters.ClauseOrdering.ValueType  # 0
    """Order clause by decreasing activity, then by increasing LBD."""
    CLAUSE_LBD: SatParameters.ClauseOrdering.ValueType  # 1
    """Order clause by increasing LBD, then by decreasing activity."""

    class _RestartAlgorithm:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _RestartAlgorithmEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._RestartAlgorithm.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        NO_RESTART: SatParameters._RestartAlgorithm.ValueType  # 0
        LUBY_RESTART: SatParameters._RestartAlgorithm.ValueType  # 1
        """Just follow a Luby sequence times restart_period."""
        DL_MOVING_AVERAGE_RESTART: SatParameters._RestartAlgorithm.ValueType  # 2
        """Moving average restart based on the decision level of conflicts."""
        LBD_MOVING_AVERAGE_RESTART: SatParameters._RestartAlgorithm.ValueType  # 3
        """Moving average restart based on the LBD of conflicts."""
        FIXED_RESTART: SatParameters._RestartAlgorithm.ValueType  # 4
        """Fixed period restart every restart period."""

    class RestartAlgorithm(_RestartAlgorithm, metaclass=_RestartAlgorithmEnumTypeWrapper):
        """==========================================================================
        Restart
        ==========================================================================

        Restart algorithms.

        A reference for the more advanced ones is:
        Gilles Audemard, Laurent Simon, "Refining Restarts Strategies for SAT
        and UNSAT", Principles and Practice of Constraint Programming Lecture
        Notes in Computer Science 2012, pp 118-126
        """

    NO_RESTART: SatParameters.RestartAlgorithm.ValueType  # 0
    LUBY_RESTART: SatParameters.RestartAlgorithm.ValueType  # 1
    """Just follow a Luby sequence times restart_period."""
    DL_MOVING_AVERAGE_RESTART: SatParameters.RestartAlgorithm.ValueType  # 2
    """Moving average restart based on the decision level of conflicts."""
    LBD_MOVING_AVERAGE_RESTART: SatParameters.RestartAlgorithm.ValueType  # 3
    """Moving average restart based on the LBD of conflicts."""
    FIXED_RESTART: SatParameters.RestartAlgorithm.ValueType  # 4
    """Fixed period restart every restart period."""

    class _MaxSatAssumptionOrder:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _MaxSatAssumptionOrderEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._MaxSatAssumptionOrder.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        DEFAULT_ASSUMPTION_ORDER: SatParameters._MaxSatAssumptionOrder.ValueType  # 0
        ORDER_ASSUMPTION_BY_DEPTH: SatParameters._MaxSatAssumptionOrder.ValueType  # 1
        ORDER_ASSUMPTION_BY_WEIGHT: SatParameters._MaxSatAssumptionOrder.ValueType  # 2

    class MaxSatAssumptionOrder(_MaxSatAssumptionOrder, metaclass=_MaxSatAssumptionOrderEnumTypeWrapper):
        """In what order do we add the assumptions in a core-based max-sat algorithm"""

    DEFAULT_ASSUMPTION_ORDER: SatParameters.MaxSatAssumptionOrder.ValueType  # 0
    ORDER_ASSUMPTION_BY_DEPTH: SatParameters.MaxSatAssumptionOrder.ValueType  # 1
    ORDER_ASSUMPTION_BY_WEIGHT: SatParameters.MaxSatAssumptionOrder.ValueType  # 2

    class _MaxSatStratificationAlgorithm:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _MaxSatStratificationAlgorithmEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._MaxSatStratificationAlgorithm.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        STRATIFICATION_NONE: SatParameters._MaxSatStratificationAlgorithm.ValueType  # 0
        """No stratification of the problem."""
        STRATIFICATION_DESCENT: SatParameters._MaxSatStratificationAlgorithm.ValueType  # 1
        """Start with literals with the highest weight, and when SAT, add the
        literals with the next highest weight and so on.
        """
        STRATIFICATION_ASCENT: SatParameters._MaxSatStratificationAlgorithm.ValueType  # 2
        """Start with all literals. Each time a core is found with a given minimum
        weight, do not consider literals with a lower weight for the next core
        computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT
        and just add the literals with the next highest weight.
        """

    class MaxSatStratificationAlgorithm(_MaxSatStratificationAlgorithm, metaclass=_MaxSatStratificationAlgorithmEnumTypeWrapper):
        """What stratification algorithm we use in the presence of weight."""

    STRATIFICATION_NONE: SatParameters.MaxSatStratificationAlgorithm.ValueType  # 0
    """No stratification of the problem."""
    STRATIFICATION_DESCENT: SatParameters.MaxSatStratificationAlgorithm.ValueType  # 1
    """Start with literals with the highest weight, and when SAT, add the
    literals with the next highest weight and so on.
    """
    STRATIFICATION_ASCENT: SatParameters.MaxSatStratificationAlgorithm.ValueType  # 2
    """Start with all literals. Each time a core is found with a given minimum
    weight, do not consider literals with a lower weight for the next core
    computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT
    and just add the literals with the next highest weight.
    """

    class _SearchBranching:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _SearchBranchingEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._SearchBranching.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        AUTOMATIC_SEARCH: SatParameters._SearchBranching.ValueType  # 0
        """Try to fix all literals using the underlying SAT solver's heuristics,
        then generate and fix literals until integer variables are fixed. New
        literals on integer variables are generated using the fixed search
        specified by the user or our default one.
        """
        FIXED_SEARCH: SatParameters._SearchBranching.ValueType  # 1
        """If used then all decisions taken by the solver are made using a fixed
        order as specified in the API or in the CpModelProto search_strategy
        field.
        """
        PORTFOLIO_SEARCH: SatParameters._SearchBranching.ValueType  # 2
        """Simple portfolio search used by LNS workers."""
        LP_SEARCH: SatParameters._SearchBranching.ValueType  # 3
        """If used, the solver will use heuristics from the LP relaxation. This
        exploit the reduced costs of the variables in the relaxation.
        """
        PSEUDO_COST_SEARCH: SatParameters._SearchBranching.ValueType  # 4
        """If used, the solver uses the pseudo costs for branching. Pseudo costs
        are computed using the historical change in objective bounds when some
        decision are taken. Note that this works whether we use an LP or not.
        """
        PORTFOLIO_WITH_QUICK_RESTART_SEARCH: SatParameters._SearchBranching.ValueType  # 5
        """Mainly exposed here for testing. This quickly tries a lot of randomized
        heuristics with a low conflict limit. It usually provides a good first
        solution.
        """
        HINT_SEARCH: SatParameters._SearchBranching.ValueType  # 6
        """Mainly used internally. This is like FIXED_SEARCH, except we follow the
        solution_hint field of the CpModelProto rather than using the information
        provided in the search_strategy.
        """
        PARTIAL_FIXED_SEARCH: SatParameters._SearchBranching.ValueType  # 7
        """Similar to FIXED_SEARCH, but differ in how the variable not listed into
        the fixed search heuristics are branched on. This will always start the
        search tree according to the specified fixed search strategy, but will
        complete it using the default automatic search.
        """
        RANDOMIZED_SEARCH: SatParameters._SearchBranching.ValueType  # 8
        """Randomized search. Used to increase entropy in the search."""

    class SearchBranching(_SearchBranching, metaclass=_SearchBranchingEnumTypeWrapper):
        """The search branching will be used to decide how to branch on unfixed nodes."""

    AUTOMATIC_SEARCH: SatParameters.SearchBranching.ValueType  # 0
    """Try to fix all literals using the underlying SAT solver's heuristics,
    then generate and fix literals until integer variables are fixed. New
    literals on integer variables are generated using the fixed search
    specified by the user or our default one.
    """
    FIXED_SEARCH: SatParameters.SearchBranching.ValueType  # 1
    """If used then all decisions taken by the solver are made using a fixed
    order as specified in the API or in the CpModelProto search_strategy
    field.
    """
    PORTFOLIO_SEARCH: SatParameters.SearchBranching.ValueType  # 2
    """Simple portfolio search used by LNS workers."""
    LP_SEARCH: SatParameters.SearchBranching.ValueType  # 3
    """If used, the solver will use heuristics from the LP relaxation. This
    exploit the reduced costs of the variables in the relaxation.
    """
    PSEUDO_COST_SEARCH: SatParameters.SearchBranching.ValueType  # 4
    """If used, the solver uses the pseudo costs for branching. Pseudo costs
    are computed using the historical change in objective bounds when some
    decision are taken. Note that this works whether we use an LP or not.
    """
    PORTFOLIO_WITH_QUICK_RESTART_SEARCH: SatParameters.SearchBranching.ValueType  # 5
    """Mainly exposed here for testing. This quickly tries a lot of randomized
    heuristics with a low conflict limit. It usually provides a good first
    solution.
    """
    HINT_SEARCH: SatParameters.SearchBranching.ValueType  # 6
    """Mainly used internally. This is like FIXED_SEARCH, except we follow the
    solution_hint field of the CpModelProto rather than using the information
    provided in the search_strategy.
    """
    PARTIAL_FIXED_SEARCH: SatParameters.SearchBranching.ValueType  # 7
    """Similar to FIXED_SEARCH, but differ in how the variable not listed into
    the fixed search heuristics are branched on. This will always start the
    search tree according to the specified fixed search strategy, but will
    complete it using the default automatic search.
    """
    RANDOMIZED_SEARCH: SatParameters.SearchBranching.ValueType  # 8
    """Randomized search. Used to increase entropy in the search."""

    class _SharedTreeSplitStrategy:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _SharedTreeSplitStrategyEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._SharedTreeSplitStrategy.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        SPLIT_STRATEGY_AUTO: SatParameters._SharedTreeSplitStrategy.ValueType  # 0
        """Uses the default strategy, currently equivalent to
        SPLIT_STRATEGY_DISCREPANCY.
        """
        SPLIT_STRATEGY_DISCREPANCY: SatParameters._SharedTreeSplitStrategy.ValueType  # 1
        """Only accept splits if the node to be split's depth+discrepancy is minimal
        for the desired number of leaves.
        The preferred child for discrepancy calculation is the one with the
        lowest objective lower bound or the original branch direction if the
        bounds are equal. This rule allows twice as many workers to work in the
        preferred subtree as non-preferred.
        """
        SPLIT_STRATEGY_OBJECTIVE_LB: SatParameters._SharedTreeSplitStrategy.ValueType  # 2
        """Only split nodes with an objective lb equal to the global lb. If there is
        no objective, this is equivalent to SPLIT_STRATEGY_FIRST_PROPOSAL.
        """
        SPLIT_STRATEGY_BALANCED_TREE: SatParameters._SharedTreeSplitStrategy.ValueType  # 3
        """Attempt to keep the shared tree balanced."""
        SPLIT_STRATEGY_FIRST_PROPOSAL: SatParameters._SharedTreeSplitStrategy.ValueType  # 4
        """Workers race to split their subtree, the winner's proposal is accepted."""

    class SharedTreeSplitStrategy(_SharedTreeSplitStrategy, metaclass=_SharedTreeSplitStrategyEnumTypeWrapper): ...
    SPLIT_STRATEGY_AUTO: SatParameters.SharedTreeSplitStrategy.ValueType  # 0
    """Uses the default strategy, currently equivalent to
    SPLIT_STRATEGY_DISCREPANCY.
    """
    SPLIT_STRATEGY_DISCREPANCY: SatParameters.SharedTreeSplitStrategy.ValueType  # 1
    """Only accept splits if the node to be split's depth+discrepancy is minimal
    for the desired number of leaves.
    The preferred child for discrepancy calculation is the one with the
    lowest objective lower bound or the original branch direction if the
    bounds are equal. This rule allows twice as many workers to work in the
    preferred subtree as non-preferred.
    """
    SPLIT_STRATEGY_OBJECTIVE_LB: SatParameters.SharedTreeSplitStrategy.ValueType  # 2
    """Only split nodes with an objective lb equal to the global lb. If there is
    no objective, this is equivalent to SPLIT_STRATEGY_FIRST_PROPOSAL.
    """
    SPLIT_STRATEGY_BALANCED_TREE: SatParameters.SharedTreeSplitStrategy.ValueType  # 3
    """Attempt to keep the shared tree balanced."""
    SPLIT_STRATEGY_FIRST_PROPOSAL: SatParameters.SharedTreeSplitStrategy.ValueType  # 4
    """Workers race to split their subtree, the winner's proposal is accepted."""

    class _FPRoundingMethod:
        ValueType = typing.NewType("ValueType", builtins.int)
        V: typing_extensions.TypeAlias = ValueType

    class _FPRoundingMethodEnumTypeWrapper(google.protobuf.internal.enum_type_wrapper._EnumTypeWrapper[SatParameters._FPRoundingMethod.ValueType], builtins.type):
        DESCRIPTOR: google.protobuf.descriptor.EnumDescriptor
        NEAREST_INTEGER: SatParameters._FPRoundingMethod.ValueType  # 0
        """Rounds to the nearest integer value."""
        LOCK_BASED: SatParameters._FPRoundingMethod.ValueType  # 1
        """Counts the number of linear constraints restricting the variable in the
        increasing values (up locks) and decreasing values (down locks). Rounds
        the variable in the direction of lesser locks.
        """
        ACTIVE_LOCK_BASED: SatParameters._FPRoundingMethod.ValueType  # 3
        """Similar to lock based rounding except this only considers locks of active
        constraints from the last lp solve.
        """
        PROPAGATION_ASSISTED: SatParameters._FPRoundingMethod.ValueType  # 2
        """This is expensive rounding algorithm. We round variables one by one and
        propagate the bounds in between. If none of the rounded values fall in
        the continuous domain specified by lower and upper bound, we use the
        current lower/upper bound (whichever one is closest) instead of rounding
        the fractional lp solution value. If both the rounded values are in the
        domain, we round to nearest integer.
        """

    class FPRoundingMethod(_FPRoundingMethod, metaclass=_FPRoundingMethodEnumTypeWrapper):
        """Rounding method to use for feasibility pump."""

    NEAREST_INTEGER: SatParameters.FPRoundingMethod.ValueType  # 0
    """Rounds to the nearest integer value."""
    LOCK_BASED: SatParameters.FPRoundingMethod.ValueType  # 1
    """Counts the number of linear constraints restricting the variable in the
    increasing values (up locks) and decreasing values (down locks). Rounds
    the variable in the direction of lesser locks.
    """
    ACTIVE_LOCK_BASED: SatParameters.FPRoundingMethod.ValueType  # 3
    """Similar to lock based rounding except this only considers locks of active
    constraints from the last lp solve.
    """
    PROPAGATION_ASSISTED: SatParameters.FPRoundingMethod.ValueType  # 2
    """This is expensive rounding algorithm. We round variables one by one and
    propagate the bounds in between. If none of the rounded values fall in
    the continuous domain specified by lower and upper bound, we use the
    current lower/upper bound (whichever one is closest) instead of rounding
    the fractional lp solution value. If both the rounded values are in the
    domain, we round to nearest integer.
    """

    NAME_FIELD_NUMBER: builtins.int
    PREFERRED_VARIABLE_ORDER_FIELD_NUMBER: builtins.int
    INITIAL_POLARITY_FIELD_NUMBER: builtins.int
    USE_PHASE_SAVING_FIELD_NUMBER: builtins.int
    POLARITY_REPHASE_INCREMENT_FIELD_NUMBER: builtins.int
    POLARITY_EXPLOIT_LS_HINTS_FIELD_NUMBER: builtins.int
    RANDOM_POLARITY_RATIO_FIELD_NUMBER: builtins.int
    RANDOM_BRANCHES_RATIO_FIELD_NUMBER: builtins.int
    USE_ERWA_HEURISTIC_FIELD_NUMBER: builtins.int
    INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER: builtins.int
    ALSO_BUMP_VARIABLES_IN_CONFLICT_REASONS_FIELD_NUMBER: builtins.int
    MINIMIZATION_ALGORITHM_FIELD_NUMBER: builtins.int
    BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER: builtins.int
    SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER: builtins.int
    EXTRA_SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER: builtins.int
    DECISION_SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER: builtins.int
    EAGERLY_SUBSUME_LAST_N_CONFLICTS_FIELD_NUMBER: builtins.int
    SUBSUME_DURING_VIVIFICATION_FIELD_NUMBER: builtins.int
    USE_CHRONOLOGICAL_BACKTRACKING_FIELD_NUMBER: builtins.int
    MAX_BACKJUMP_LEVELS_FIELD_NUMBER: builtins.int
    CHRONOLOGICAL_BACKTRACK_MIN_CONFLICTS_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_PERIOD_INCREMENT_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_TARGET_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_RATIO_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_LBD_TIER1_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_LBD_TIER2_FIELD_NUMBER: builtins.int
    CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER: builtins.int
    PB_CLEANUP_INCREMENT_FIELD_NUMBER: builtins.int
    PB_CLEANUP_RATIO_FIELD_NUMBER: builtins.int
    VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER: builtins.int
    MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER: builtins.int
    GLUCOSE_MAX_DECAY_FIELD_NUMBER: builtins.int
    GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER: builtins.int
    GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER: builtins.int
    CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER: builtins.int
    MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER: builtins.int
    RESTART_ALGORITHMS_FIELD_NUMBER: builtins.int
    DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER: builtins.int
    RESTART_PERIOD_FIELD_NUMBER: builtins.int
    RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER: builtins.int
    RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER: builtins.int
    RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER: builtins.int
    USE_BLOCKING_RESTART_FIELD_NUMBER: builtins.int
    BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER: builtins.int
    BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER: builtins.int
    NUM_CONFLICTS_BEFORE_STRATEGY_CHANGES_FIELD_NUMBER: builtins.int
    STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER: builtins.int
    MAX_TIME_IN_SECONDS_FIELD_NUMBER: builtins.int
    MAX_DETERMINISTIC_TIME_FIELD_NUMBER: builtins.int
    MAX_NUM_DETERMINISTIC_BATCHES_FIELD_NUMBER: builtins.int
    MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER: builtins.int
    MAX_MEMORY_IN_MB_FIELD_NUMBER: builtins.int
    ABSOLUTE_GAP_LIMIT_FIELD_NUMBER: builtins.int
    RELATIVE_GAP_LIMIT_FIELD_NUMBER: builtins.int
    RANDOM_SEED_FIELD_NUMBER: builtins.int
    PERMUTE_VARIABLE_RANDOMLY_FIELD_NUMBER: builtins.int
    PERMUTE_PRESOLVE_CONSTRAINT_ORDER_FIELD_NUMBER: builtins.int
    USE_ABSL_RANDOM_FIELD_NUMBER: builtins.int
    LOG_SEARCH_PROGRESS_FIELD_NUMBER: builtins.int
    LOG_SUBSOLVER_STATISTICS_FIELD_NUMBER: builtins.int
    LOG_PREFIX_FIELD_NUMBER: builtins.int
    LOG_TO_STDOUT_FIELD_NUMBER: builtins.int
    LOG_TO_RESPONSE_FIELD_NUMBER: builtins.int
    USE_PB_RESOLUTION_FIELD_NUMBER: builtins.int
    MINIMIZE_REDUCTION_DURING_PB_RESOLUTION_FIELD_NUMBER: builtins.int
    COUNT_ASSUMPTION_LEVELS_IN_LBD_FIELD_NUMBER: builtins.int
    PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER: builtins.int
    FILTER_SAT_POSTSOLVE_CLAUSES_FIELD_NUMBER: builtins.int
    PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER: builtins.int
    PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER: builtins.int
    PRESOLVE_PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER: builtins.int
    PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER: builtins.int
    PRESOLVE_USE_BVA_FIELD_NUMBER: builtins.int
    PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER: builtins.int
    MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER: builtins.int
    CP_MODEL_PRESOLVE_FIELD_NUMBER: builtins.int
    CP_MODEL_PROBING_LEVEL_FIELD_NUMBER: builtins.int
    CP_MODEL_USE_SAT_PRESOLVE_FIELD_NUMBER: builtins.int
    LOAD_AT_MOST_ONES_IN_SAT_PRESOLVE_FIELD_NUMBER: builtins.int
    REMOVE_FIXED_VARIABLES_EARLY_FIELD_NUMBER: builtins.int
    DETECT_TABLE_WITH_COST_FIELD_NUMBER: builtins.int
    TABLE_COMPRESSION_LEVEL_FIELD_NUMBER: builtins.int
    EXPAND_ALLDIFF_CONSTRAINTS_FIELD_NUMBER: builtins.int
    MAX_ALLDIFF_DOMAIN_SIZE_FIELD_NUMBER: builtins.int
    EXPAND_RESERVOIR_CONSTRAINTS_FIELD_NUMBER: builtins.int
    MAX_DOMAIN_SIZE_FOR_LINEAR2_EXPANSION_FIELD_NUMBER: builtins.int
    EXPAND_RESERVOIR_USING_CIRCUIT_FIELD_NUMBER: builtins.int
    ENCODE_CUMULATIVE_AS_RESERVOIR_FIELD_NUMBER: builtins.int
    MAX_LIN_MAX_SIZE_FOR_EXPANSION_FIELD_NUMBER: builtins.int
    DISABLE_CONSTRAINT_EXPANSION_FIELD_NUMBER: builtins.int
    ENCODE_COMPLEX_LINEAR_CONSTRAINT_WITH_INTEGER_FIELD_NUMBER: builtins.int
    MERGE_NO_OVERLAP_WORK_LIMIT_FIELD_NUMBER: builtins.int
    MERGE_AT_MOST_ONE_WORK_LIMIT_FIELD_NUMBER: builtins.int
    PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER: builtins.int
    PRESOLVE_EXTRACT_INTEGER_ENFORCEMENT_FIELD_NUMBER: builtins.int
    PRESOLVE_INCLUSION_WORK_LIMIT_FIELD_NUMBER: builtins.int
    IGNORE_NAMES_FIELD_NUMBER: builtins.int
    INFER_ALL_DIFFS_FIELD_NUMBER: builtins.int
    FIND_BIG_LINEAR_OVERLAP_FIELD_NUMBER: builtins.int
    FIND_CLAUSES_THAT_ARE_EXACTLY_ONE_FIELD_NUMBER: builtins.int
    USE_SAT_INPROCESSING_FIELD_NUMBER: builtins.int
    INPROCESSING_DTIME_RATIO_FIELD_NUMBER: builtins.int
    INPROCESSING_PROBING_DTIME_FIELD_NUMBER: builtins.int
    INPROCESSING_MINIMIZATION_DTIME_FIELD_NUMBER: builtins.int
    INPROCESSING_MINIMIZATION_USE_CONFLICT_ANALYSIS_FIELD_NUMBER: builtins.int
    INPROCESSING_MINIMIZATION_USE_ALL_ORDERINGS_FIELD_NUMBER: builtins.int
    INPROCESSING_USE_CONGRUENCE_CLOSURE_FIELD_NUMBER: builtins.int
    INPROCESSING_USE_SAT_SWEEPING_FIELD_NUMBER: builtins.int
    NUM_WORKERS_FIELD_NUMBER: builtins.int
    NUM_SEARCH_WORKERS_FIELD_NUMBER: builtins.int
    NUM_FULL_SUBSOLVERS_FIELD_NUMBER: builtins.int
    SUBSOLVERS_FIELD_NUMBER: builtins.int
    EXTRA_SUBSOLVERS_FIELD_NUMBER: builtins.int
    IGNORE_SUBSOLVERS_FIELD_NUMBER: builtins.int
    FILTER_SUBSOLVERS_FIELD_NUMBER: builtins.int
    SUBSOLVER_PARAMS_FIELD_NUMBER: builtins.int
    INTERLEAVE_SEARCH_FIELD_NUMBER: builtins.int
    INTERLEAVE_BATCH_SIZE_FIELD_NUMBER: builtins.int
    SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER: builtins.int
    SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER: builtins.int
    SHARE_LINEAR2_BOUNDS_FIELD_NUMBER: builtins.int
    SHARE_BINARY_CLAUSES_FIELD_NUMBER: builtins.int
    SHARE_GLUE_CLAUSES_FIELD_NUMBER: builtins.int
    MINIMIZE_SHARED_CLAUSES_FIELD_NUMBER: builtins.int
    SHARE_GLUE_CLAUSES_DTIME_FIELD_NUMBER: builtins.int
    CHECK_LRAT_PROOF_FIELD_NUMBER: builtins.int
    CHECK_MERGED_LRAT_PROOF_FIELD_NUMBER: builtins.int
    OUTPUT_LRAT_PROOF_FIELD_NUMBER: builtins.int
    CHECK_DRAT_PROOF_FIELD_NUMBER: builtins.int
    OUTPUT_DRAT_PROOF_FIELD_NUMBER: builtins.int
    MAX_DRAT_TIME_IN_SECONDS_FIELD_NUMBER: builtins.int
    DEBUG_POSTSOLVE_WITH_FULL_SOLVER_FIELD_NUMBER: builtins.int
    DEBUG_MAX_NUM_PRESOLVE_OPERATIONS_FIELD_NUMBER: builtins.int
    DEBUG_CRASH_ON_BAD_HINT_FIELD_NUMBER: builtins.int
    DEBUG_CRASH_IF_PRESOLVE_BREAKS_HINT_FIELD_NUMBER: builtins.int
    DEBUG_CRASH_IF_LRAT_CHECK_FAILS_FIELD_NUMBER: builtins.int
    USE_OPTIMIZATION_HINTS_FIELD_NUMBER: builtins.int
    CORE_MINIMIZATION_LEVEL_FIELD_NUMBER: builtins.int
    FIND_MULTIPLE_CORES_FIELD_NUMBER: builtins.int
    COVER_OPTIMIZATION_FIELD_NUMBER: builtins.int
    MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER: builtins.int
    MAX_SAT_REVERSE_ASSUMPTION_ORDER_FIELD_NUMBER: builtins.int
    MAX_SAT_STRATIFICATION_FIELD_NUMBER: builtins.int
    PROPAGATION_LOOP_DETECTION_FACTOR_FIELD_NUMBER: builtins.int
    USE_PRECEDENCES_IN_DISJUNCTIVE_CONSTRAINT_FIELD_NUMBER: builtins.int
    TRANSITIVE_PRECEDENCES_WORK_LIMIT_FIELD_NUMBER: builtins.int
    MAX_SIZE_TO_CREATE_PRECEDENCE_LITERALS_IN_DISJUNCTIVE_FIELD_NUMBER: builtins.int
    USE_STRONG_PROPAGATION_IN_DISJUNCTIVE_FIELD_NUMBER: builtins.int
    USE_DYNAMIC_PRECEDENCE_IN_DISJUNCTIVE_FIELD_NUMBER: builtins.int
    USE_DYNAMIC_PRECEDENCE_IN_CUMULATIVE_FIELD_NUMBER: builtins.int
    USE_OVERLOAD_CHECKER_IN_CUMULATIVE_FIELD_NUMBER: builtins.int
    USE_CONSERVATIVE_SCALE_OVERLOAD_CHECKER_FIELD_NUMBER: builtins.int
    USE_TIMETABLE_EDGE_FINDING_IN_CUMULATIVE_FIELD_NUMBER: builtins.int
    MAX_NUM_INTERVALS_FOR_TIMETABLE_EDGE_FINDING_FIELD_NUMBER: builtins.int
    USE_HARD_PRECEDENCES_IN_CUMULATIVE_FIELD_NUMBER: builtins.int
    EXPLOIT_ALL_PRECEDENCES_FIELD_NUMBER: builtins.int
    USE_DISJUNCTIVE_CONSTRAINT_IN_CUMULATIVE_FIELD_NUMBER: builtins.int
    NO_OVERLAP_2D_BOOLEAN_RELATIONS_LIMIT_FIELD_NUMBER: builtins.int
    USE_TIMETABLING_IN_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    USE_ENERGETIC_REASONING_IN_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    USE_AREA_ENERGETIC_REASONING_IN_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    USE_TRY_EDGE_REASONING_IN_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    MAX_PAIRS_PAIRWISE_REASONING_IN_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    MAXIMUM_REGIONS_TO_SPLIT_IN_DISCONNECTED_NO_OVERLAP_2D_FIELD_NUMBER: builtins.int
    USE_LINEAR3_FOR_NO_OVERLAP_2D_PRECEDENCES_FIELD_NUMBER: builtins.int
    USE_DUAL_SCHEDULING_HEURISTICS_FIELD_NUMBER: builtins.int
    USE_ALL_DIFFERENT_FOR_CIRCUIT_FIELD_NUMBER: builtins.int
    ROUTING_CUT_SUBSET_SIZE_FOR_BINARY_RELATION_BOUND_FIELD_NUMBER: builtins.int
    ROUTING_CUT_SUBSET_SIZE_FOR_TIGHT_BINARY_RELATION_BOUND_FIELD_NUMBER: builtins.int
    ROUTING_CUT_SUBSET_SIZE_FOR_EXACT_BINARY_RELATION_BOUND_FIELD_NUMBER: builtins.int
    ROUTING_CUT_SUBSET_SIZE_FOR_SHORTEST_PATHS_BOUND_FIELD_NUMBER: builtins.int
    ROUTING_CUT_DP_EFFORT_FIELD_NUMBER: builtins.int
    ROUTING_CUT_MAX_INFEASIBLE_PATH_LENGTH_FIELD_NUMBER: builtins.int
    SEARCH_BRANCHING_FIELD_NUMBER: builtins.int
    HINT_CONFLICT_LIMIT_FIELD_NUMBER: builtins.int
    REPAIR_HINT_FIELD_NUMBER: builtins.int
    FIX_VARIABLES_TO_THEIR_HINTED_VALUE_FIELD_NUMBER: builtins.int
    USE_PROBING_SEARCH_FIELD_NUMBER: builtins.int
    USE_EXTENDED_PROBING_FIELD_NUMBER: builtins.int
    PROBING_NUM_COMBINATIONS_LIMIT_FIELD_NUMBER: builtins.int
    SHAVING_DETERMINISTIC_TIME_IN_PROBING_SEARCH_FIELD_NUMBER: builtins.int
    SHAVING_SEARCH_DETERMINISTIC_TIME_FIELD_NUMBER: builtins.int
    SHAVING_SEARCH_THRESHOLD_FIELD_NUMBER: builtins.int
    USE_OBJECTIVE_LB_SEARCH_FIELD_NUMBER: builtins.int
    USE_OBJECTIVE_SHAVING_SEARCH_FIELD_NUMBER: builtins.int
    VARIABLES_SHAVING_LEVEL_FIELD_NUMBER: builtins.int
    PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER: builtins.int
    OPTIMIZE_WITH_CORE_FIELD_NUMBER: builtins.int
    OPTIMIZE_WITH_LB_TREE_SEARCH_FIELD_NUMBER: builtins.int
    SAVE_LP_BASIS_IN_LB_TREE_SEARCH_FIELD_NUMBER: builtins.int
    BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER: builtins.int
    OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER: builtins.int
    USE_FEASIBILITY_JUMP_FIELD_NUMBER: builtins.int
    USE_LS_ONLY_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_DECAY_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_LINEARIZATION_LEVEL_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_RESTART_FACTOR_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_BATCH_DTIME_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_VAR_RANDOMIZATION_PROBABILITY_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_VAR_PERBURBATION_RANGE_RATIO_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_ENABLE_RESTARTS_FIELD_NUMBER: builtins.int
    FEASIBILITY_JUMP_MAX_EXPANDED_CONSTRAINT_SIZE_FIELD_NUMBER: builtins.int
    NUM_VIOLATION_LS_FIELD_NUMBER: builtins.int
    VIOLATION_LS_PERTURBATION_PERIOD_FIELD_NUMBER: builtins.int
    VIOLATION_LS_COMPOUND_MOVE_PROBABILITY_FIELD_NUMBER: builtins.int
    SHARED_TREE_NUM_WORKERS_FIELD_NUMBER: builtins.int
    USE_SHARED_TREE_SEARCH_FIELD_NUMBER: builtins.int
    SHARED_TREE_WORKER_MIN_RESTARTS_PER_SUBTREE_FIELD_NUMBER: builtins.int
    SHARED_TREE_WORKER_ENABLE_TRAIL_SHARING_FIELD_NUMBER: builtins.int
    SHARED_TREE_WORKER_ENABLE_PHASE_SHARING_FIELD_NUMBER: builtins.int
    SHARED_TREE_OPEN_LEAVES_PER_WORKER_FIELD_NUMBER: builtins.int
    SHARED_TREE_MAX_NODES_PER_WORKER_FIELD_NUMBER: builtins.int
    SHARED_TREE_SPLIT_STRATEGY_FIELD_NUMBER: builtins.int
    SHARED_TREE_BALANCE_TOLERANCE_FIELD_NUMBER: builtins.int
    SHARED_TREE_SPLIT_MIN_DTIME_FIELD_NUMBER: builtins.int
    ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER: builtins.int
    KEEP_ALL_FEASIBLE_SOLUTIONS_IN_PRESOLVE_FIELD_NUMBER: builtins.int
    FILL_TIGHTENED_DOMAINS_IN_RESPONSE_FIELD_NUMBER: builtins.int
    FILL_ADDITIONAL_SOLUTIONS_IN_RESPONSE_FIELD_NUMBER: builtins.int
    INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER: builtins.int
    AUTO_DETECT_GREATER_THAN_AT_LEAST_ONE_OF_FIELD_NUMBER: builtins.int
    STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER: builtins.int
    STOP_AFTER_PRESOLVE_FIELD_NUMBER: builtins.int
    STOP_AFTER_ROOT_PROPAGATION_FIELD_NUMBER: builtins.int
    LNS_INITIAL_DIFFICULTY_FIELD_NUMBER: builtins.int
    LNS_INITIAL_DETERMINISTIC_LIMIT_FIELD_NUMBER: builtins.int
    USE_LNS_FIELD_NUMBER: builtins.int
    USE_LNS_ONLY_FIELD_NUMBER: builtins.int
    SOLUTION_POOL_SIZE_FIELD_NUMBER: builtins.int
    SOLUTION_POOL_DIVERSITY_LIMIT_FIELD_NUMBER: builtins.int
    ALTERNATIVE_POOL_SIZE_FIELD_NUMBER: builtins.int
    USE_RINS_LNS_FIELD_NUMBER: builtins.int
    USE_FEASIBILITY_PUMP_FIELD_NUMBER: builtins.int
    USE_LB_RELAX_LNS_FIELD_NUMBER: builtins.int
    LB_RELAX_NUM_WORKERS_THRESHOLD_FIELD_NUMBER: builtins.int
    FP_ROUNDING_FIELD_NUMBER: builtins.int
    DIVERSIFY_LNS_PARAMS_FIELD_NUMBER: builtins.int
    RANDOMIZE_SEARCH_FIELD_NUMBER: builtins.int
    SEARCH_RANDOM_VARIABLE_POOL_SIZE_FIELD_NUMBER: builtins.int
    PUSH_ALL_TASKS_TOWARD_START_FIELD_NUMBER: builtins.int
    USE_OPTIONAL_VARIABLES_FIELD_NUMBER: builtins.int
    USE_EXACT_LP_REASON_FIELD_NUMBER: builtins.int
    USE_COMBINED_NO_OVERLAP_FIELD_NUMBER: builtins.int
    AT_MOST_ONE_MAX_EXPANSION_SIZE_FIELD_NUMBER: builtins.int
    CATCH_SIGINT_SIGNAL_FIELD_NUMBER: builtins.int
    USE_IMPLIED_BOUNDS_FIELD_NUMBER: builtins.int
    POLISH_LP_SOLUTION_FIELD_NUMBER: builtins.int
    LP_PRIMAL_TOLERANCE_FIELD_NUMBER: builtins.int
    LP_DUAL_TOLERANCE_FIELD_NUMBER: builtins.int
    CONVERT_INTERVALS_FIELD_NUMBER: builtins.int
    SYMMETRY_LEVEL_FIELD_NUMBER: builtins.int
    USE_SYMMETRY_IN_LP_FIELD_NUMBER: builtins.int
    KEEP_SYMMETRY_IN_PRESOLVE_FIELD_NUMBER: builtins.int
    SYMMETRY_DETECTION_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER: builtins.int
    NEW_LINEAR_PROPAGATION_FIELD_NUMBER: builtins.int
    LINEAR_SPLIT_SIZE_FIELD_NUMBER: builtins.int
    LINEARIZATION_LEVEL_FIELD_NUMBER: builtins.int
    BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER: builtins.int
    MAX_DOMAIN_SIZE_WHEN_ENCODING_EQ_NEQ_CONSTRAINTS_FIELD_NUMBER: builtins.int
    MAX_NUM_CUTS_FIELD_NUMBER: builtins.int
    CUT_LEVEL_FIELD_NUMBER: builtins.int
    ONLY_ADD_CUTS_AT_LEVEL_ZERO_FIELD_NUMBER: builtins.int
    ADD_OBJECTIVE_CUT_FIELD_NUMBER: builtins.int
    ADD_CG_CUTS_FIELD_NUMBER: builtins.int
    ADD_MIR_CUTS_FIELD_NUMBER: builtins.int
    ADD_ZERO_HALF_CUTS_FIELD_NUMBER: builtins.int
    ADD_CLIQUE_CUTS_FIELD_NUMBER: builtins.int
    ADD_RLT_CUTS_FIELD_NUMBER: builtins.int
    MAX_ALL_DIFF_CUT_SIZE_FIELD_NUMBER: builtins.int
    ADD_LIN_MAX_CUTS_FIELD_NUMBER: builtins.int
    MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER: builtins.int
    ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER: builtins.int
    ROOT_LP_ITERATIONS_FIELD_NUMBER: builtins.int
    MIN_ORTHOGONALITY_FOR_LP_CONSTRAINTS_FIELD_NUMBER: builtins.int
    MAX_CUT_ROUNDS_AT_LEVEL_ZERO_FIELD_NUMBER: builtins.int
    MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER: builtins.int
    CUT_MAX_ACTIVE_COUNT_VALUE_FIELD_NUMBER: builtins.int
    CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER: builtins.int
    CUT_CLEANUP_TARGET_FIELD_NUMBER: builtins.int
    NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER: builtins.int
    EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER: builtins.int
    EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER: builtins.int
    EXPLOIT_BEST_SOLUTION_FIELD_NUMBER: builtins.int
    EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER: builtins.int
    EXPLOIT_OBJECTIVE_FIELD_NUMBER: builtins.int
    DETECT_LINEARIZED_PRODUCT_FIELD_NUMBER: builtins.int
    USE_NEW_INTEGER_CONFLICT_RESOLUTION_FIELD_NUMBER: builtins.int
    CREATE_1UIP_BOOLEAN_DURING_ICR_FIELD_NUMBER: builtins.int
    MIP_MAX_BOUND_FIELD_NUMBER: builtins.int
    MIP_VAR_SCALING_FIELD_NUMBER: builtins.int
    MIP_SCALE_LARGE_DOMAIN_FIELD_NUMBER: builtins.int
    MIP_AUTOMATICALLY_SCALE_VARIABLES_FIELD_NUMBER: builtins.int
    ONLY_SOLVE_IP_FIELD_NUMBER: builtins.int
    MIP_WANTED_PRECISION_FIELD_NUMBER: builtins.int
    MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER: builtins.int
    MIP_CHECK_PRECISION_FIELD_NUMBER: builtins.int
    MIP_COMPUTE_TRUE_OBJECTIVE_BOUND_FIELD_NUMBER: builtins.int
    MIP_MAX_VALID_MAGNITUDE_FIELD_NUMBER: builtins.int
    MIP_TREAT_HIGH_MAGNITUDE_BOUNDS_AS_INFINITY_FIELD_NUMBER: builtins.int
    MIP_DROP_TOLERANCE_FIELD_NUMBER: builtins.int
    MIP_PRESOLVE_LEVEL_FIELD_NUMBER: builtins.int
    name: builtins.str
    """In some context, like in a portfolio of search, it makes sense to name a
    given parameters set for logging purpose.
    """
    preferred_variable_order: Global___SatParameters.VariableOrder.ValueType
    initial_polarity: Global___SatParameters.Polarity.ValueType
    use_phase_saving: builtins.bool
    """If this is true, then the polarity of a variable will be the last value it
    was assigned to, or its default polarity if it was never assigned since the
    call to ResetDecisionHeuristic().

    Actually, we use a newer version where we follow the last value in the
    longest non-conflicting partial assignment in the current phase.

    This is called 'literal phase saving'. For details see 'A Lightweight
    Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and
    A.Darwiche, In 10th International Conference on Theory and Applications of
    Satisfiability Testing, 2007.
    """
    polarity_rephase_increment: builtins.int
    """If non-zero, then we change the polarity heuristic after that many number
    of conflicts in an arithmetically increasing fashion. So x the first time,
    2 * x the second time, etc...
    """
    polarity_exploit_ls_hints: builtins.bool
    """If true and we have first solution LS workers, tries in some phase to
    follow a LS solutions that violates has litle constraints as possible.
    """
    random_polarity_ratio: builtins.float
    """The proportion of polarity chosen at random. Note that this take
    precedence over the phase saving heuristic. This is different from
    initial_polarity:POLARITY_RANDOM because it will select a new random
    polarity each time the variable is branched upon instead of selecting one
    initially and then always taking this choice.
    """
    random_branches_ratio: builtins.float
    """A number between 0 and 1 that indicates the proportion of branching
    variables that are selected randomly instead of choosing the first variable
    from the given variable_ordering strategy.
    """
    use_erwa_heuristic: builtins.bool
    """Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
    described in "Learning Rate Based Branching Heuristic for SAT solvers",
    J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
    """
    initial_variables_activity: builtins.float
    """The initial value of the variables activity. A non-zero value only make
    sense when use_erwa_heuristic is true. Experiments with a value of 1e-2
    together with the ERWA heuristic showed slighthly better result than simply
    using zero. The idea is that when the "learning rate" of a variable becomes
    lower than this value, then we prefer to branch on never explored before
    variables. This is not in the ERWA paper.
    """
    also_bump_variables_in_conflict_reasons: builtins.bool
    """When this is true, then the variables that appear in any of the reason of
    the variables in a conflict have their activity bumped. This is addition to
    the variables in the conflict, and the one that were used during conflict
    resolution.
    """
    minimization_algorithm: Global___SatParameters.ConflictMinimizationAlgorithm.ValueType
    binary_minimization_algorithm: Global___SatParameters.BinaryMinizationAlgorithm.ValueType
    subsumption_during_conflict_analysis: builtins.bool
    """At a really low cost, during the 1-UIP conflict computation, it is easy to
    detect if some of the involved reasons are subsumed by the current
    conflict. When this is true, such clauses are detached and later removed
    from the problem.
    """
    extra_subsumption_during_conflict_analysis: builtins.bool
    """It is possible that "intermediate" clauses during conflict resolution
    subsumes some of the clauses that propagated. This is quite cheap to detect
    and result in more subsumption/strengthening of clauses.
    """
    decision_subsumption_during_conflict_analysis: builtins.bool
    """Try even more subsumption options during conflict analysis."""
    eagerly_subsume_last_n_conflicts: builtins.int
    """If >=0, each time we have a conflict, we try to subsume the last n learned
    clause with it.
    """
    subsume_during_vivification: builtins.bool
    """If we remove clause that we now are "implied" by others. Note that this
    might not always be good as we might loose some propagation power.
    """
    use_chronological_backtracking: builtins.bool
    """If true, try to backtrack as little as possible on conflict and re-imply
    the clauses later.
    This means we discard less propagation than traditional backjumping, but
    requites additional bookkeeping to handle reimplication.
    See: https://doi.org/10.1007/978-3-319-94144-8_7
    """
    max_backjump_levels: builtins.int
    """If chronological backtracking is enabled, this is the maximum number of
    levels we will backjump over, otherwise we will backtrack.
    """
    chronological_backtrack_min_conflicts: builtins.int
    """If chronological backtracking is enabled, this is the minimum number of
    conflicts before we will consider backjumping.
    """
    clause_cleanup_period: builtins.int
    """==========================================================================
    Clause database management
    ==========================================================================

    Trigger a cleanup when this number of "deletable" clauses is learned.
    """
    clause_cleanup_period_increment: builtins.int
    """Increase clause_cleanup_period by this amount after each cleanup."""
    clause_cleanup_target: builtins.int
    """During a cleanup, we will always keep that number of "deletable" clauses.
    Note that this doesn't include the "protected" clauses.
    """
    clause_cleanup_ratio: builtins.float
    """During a cleanup, if clause_cleanup_target is 0, we will delete the
    clause_cleanup_ratio of "deletable" clauses instead of aiming for a fixed
    target of clauses to keep.
    """
    clause_cleanup_lbd_bound: builtins.int
    """All the clauses with a LBD (literal blocks distance) lower or equal to this
    parameters will always be kept.

    Note that the LBD of a clause that just propagated is 1 + number of
    different decision levels of its literals. So that the "classic" LBD of a
    learned conflict is the same as its LBD when we backjump and then propagate
    it.
    """
    clause_cleanup_lbd_tier1: builtins.int
    """All the clause with a LBD lower or equal to this will be kept except if
    its activity hasn't been bumped in the last 32 cleanup phase. Note that
    this has no effect if it is <= clause_cleanup_lbd_bound.
    """
    clause_cleanup_lbd_tier2: builtins.int
    """All the clause with a LBD lower or equal to this will be kept except if its
    activity hasn't been bumped since the previous cleanup phase. Note that
    this has no effect if it is <= clause_cleanup_lbd_bound or <=
    clause_cleanup_lbd_tier1.
    """
    clause_cleanup_ordering: Global___SatParameters.ClauseOrdering.ValueType
    pb_cleanup_increment: builtins.int
    """Same as for the clauses, but for the learned pseudo-Boolean constraints."""
    pb_cleanup_ratio: builtins.float
    variable_activity_decay: builtins.float
    """==========================================================================
    Variable and clause activities
    ==========================================================================

    Each time a conflict is found, the activities of some variables are
    increased by one. Then, the activity of all variables are multiplied by
    variable_activity_decay.

    To implement this efficiently, the activity of all the variables is not
    decayed at each conflict. Instead, the activity increment is multiplied by
    1 / decay. When an activity reach max_variable_activity_value, all the
    activity are multiplied by 1 / max_variable_activity_value.
    """
    max_variable_activity_value: builtins.float
    glucose_max_decay: builtins.float
    """The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
    0.95. This "hack" seems to work well and comes from:

    Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013
    http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
    """
    glucose_decay_increment: builtins.float
    glucose_decay_increment_period: builtins.int
    clause_activity_decay: builtins.float
    """Clause activity parameters (same effect as the one on the variables)."""
    max_clause_activity_value: builtins.float
    default_restart_algorithms: builtins.str
    restart_period: builtins.int
    """Restart period for the FIXED_RESTART strategy. This is also the multiplier
    used by the LUBY_RESTART strategy.
    """
    restart_running_window_size: builtins.int
    """Size of the window for the moving average restarts."""
    restart_dl_average_ratio: builtins.float
    """In the moving average restart algorithms, a restart is triggered if the
    window average times this ratio is greater that the global average.
    """
    restart_lbd_average_ratio: builtins.float
    use_blocking_restart: builtins.bool
    """Block a moving restart algorithm if the trail size of the current conflict
    is greater than the multiplier times the moving average of the trail size
    at the previous conflicts.
    """
    blocking_restart_window_size: builtins.int
    blocking_restart_multiplier: builtins.float
    num_conflicts_before_strategy_changes: builtins.int
    """After each restart, if the number of conflict since the last strategy
    change is greater that this, then we increment a "strategy_counter" that
    can be use to change the search strategy used by the following restarts.
    """
    strategy_change_increase_ratio: builtins.float
    """The parameter num_conflicts_before_strategy_changes is increased by that
    much after each strategy change.
    """
    max_time_in_seconds: builtins.float
    """==========================================================================
    Limits
    ==========================================================================

    Maximum time allowed in seconds to solve a problem.
    The counter will starts at the beginning of the Solve() call.
    """
    max_deterministic_time: builtins.float
    """Maximum time allowed in deterministic time to solve a problem.
    The deterministic time should be correlated with the real time used by the
    solver, the time unit being as close as possible to a second.
    """
    max_num_deterministic_batches: builtins.int
    """Stops after that number of batches has been scheduled. This only make sense
    when interleave_search is true.
    """
    max_number_of_conflicts: builtins.int
    """Maximum number of conflicts allowed to solve a problem.

    TODO(user): Maybe change the way the conflict limit is enforced?
    currently it is enforced on each independent internal SAT solve, rather
    than on the overall number of conflicts across all solves. So in the
    context of an optimization problem, this is not really usable directly by a
    client.
    kint64max
    """
    max_memory_in_mb: builtins.int
    """Maximum memory allowed for the whole thread containing the solver. The
    solver will abort as soon as it detects that this limit is crossed. As a
    result, this limit is approximative, but usually the solver will not go too
    much over.

    TODO(user): This is only used by the pure SAT solver, generalize to CP-SAT.
    """
    absolute_gap_limit: builtins.float
    """Stop the search when the gap between the best feasible objective (O) and
    our best objective bound (B) is smaller than a limit.
    The exact definition is:
    - Absolute: abs(O - B)
    - Relative: abs(O - B) / max(1, abs(O)).

    Important: The relative gap depends on the objective offset! If you
    artificially shift the objective, you will get widely different value of
    the relative gap.

    Note that if the gap is reached, the search status will be OPTIMAL. But
    one can check the best objective bound to see the actual gap.

    If the objective is integer, then any absolute gap < 1 will lead to a true
    optimal. If the objective is floating point, a gap of zero make little
    sense so is is why we use a non-zero default value. At the end of the
    search, we will display a warning if OPTIMAL is reported yet the gap is
    greater than this absolute gap.
    """
    relative_gap_limit: builtins.float
    random_seed: builtins.int
    """==========================================================================
    Other parameters
    ==========================================================================

    At the beginning of each solve, the random number generator used in some
    part of the solver is reinitialized to this seed. If you change the random
    seed, the solver may make different choices during the solving process.

    For some problems, the running time may vary a lot depending on small
    change in the solving algorithm. Running the solver with different seeds
    enables to have more robust benchmarks when evaluating new features.
    """
    permute_variable_randomly: builtins.bool
    """This is mainly here to test the solver variability. Note that in tests, if
    not explicitly set to false, all 3 options will be set to true so that
    clients do not rely on the solver returning a specific solution if they are
    many equivalent optimal solutions.
    """
    permute_presolve_constraint_order: builtins.bool
    use_absl_random: builtins.bool
    log_search_progress: builtins.bool
    """Whether the solver should log the search progress. This is the maing
    logging parameter and if this is false, none of the logging (callbacks,
    log_to_stdout, log_to_response, ...) will do anything.
    """
    log_subsolver_statistics: builtins.bool
    """Whether the solver should display per sub-solver search statistics.
    This is only useful is log_search_progress is set to true, and if the
    number of search workers is > 1. Note that in all case we display a bit
    of stats with one line per subsolver.
    """
    log_prefix: builtins.str
    """Add a prefix to all logs."""
    log_to_stdout: builtins.bool
    """Log to stdout."""
    log_to_response: builtins.bool
    """Log to response proto."""
    use_pb_resolution: builtins.bool
    """Experimental.

    This is an old experiment, it might cause crashes in multi-thread and you
    should double check the solver result. It can still be used if you only
    care about feasible solutions (these are checked) and it gives good result
    on your problem. We might revive it at some point.

    Whether to use pseudo-Boolean resolution to analyze a conflict. Note that
    this option only make sense if your problem is modelized using
    pseudo-Boolean constraints. If you only have clauses, this shouldn't change
    anything (except slow the solver down).
    """
    minimize_reduction_during_pb_resolution: builtins.bool
    """A different algorithm during PB resolution. It minimizes the number of
    calls to ReduceCoefficients() which can be time consuming. However, the
    search space will be different and if the coefficients are large, this may
    lead to integer overflows that could otherwise be prevented.
    """
    count_assumption_levels_in_lbd: builtins.bool
    """Whether or not the assumption levels are taken into account during the LBD
    computation. According to the reference below, not counting them improves
    the solver in some situation. Note that this only impact solves under
    assumptions.

    Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for
    Incremental SAT Solving with Assumptions: Application to MUS Extraction"
    Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes
    in Computer Science Volume 7962, 2013, pp 309-317.
    """
    presolve_bve_threshold: builtins.int
    """==========================================================================
    Presolve
    ==========================================================================

    During presolve, only try to perform the bounded variable elimination (BVE)
    of a variable x if the number of occurrences of x times the number of
    occurrences of not(x) is not greater than this parameter.
    """
    filter_sat_postsolve_clauses: builtins.bool
    """Internal parameter. During BVE, if we eliminate a variable x, by default we
    will push all clauses containing x and all clauses containing not(x) to the
    postsolve. However, it is possible to write the postsolve code so that only
    one such set is needed. The idea is that, if we push the set containing a
    literal l, is to set l to false except if it is needed to satisfy one of
    the clause in the set. This is always beneficial, but for historical
    reason, not all our postsolve algorithm support this.
    """
    presolve_bve_clause_weight: builtins.int
    """During presolve, we apply BVE only if this weight times the number of
    clauses plus the number of clause literals is not increased.
    """
    probing_deterministic_time_limit: builtins.float
    """The maximum "deterministic" time limit to spend in probing. A value of
    zero will disable the probing.

    TODO(user): Clean up. The first one is used in CP-SAT, the other in pure
    SAT presolve.
    """
    presolve_probing_deterministic_time_limit: builtins.float
    presolve_blocked_clause: builtins.bool
    """Whether we use an heuristic to detect some basic case of blocked clause
    in the SAT presolve.
    """
    presolve_use_bva: builtins.bool
    """Whether or not we use Bounded Variable Addition (BVA) in the presolve."""
    presolve_bva_threshold: builtins.int
    """Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
    by stricly more than this threshold. The algorithm described in the paper
    uses 0, but quick experiments showed that 1 is a good value. It may not be
    worth it to add a new variable just to remove one clause.
    """
    max_presolve_iterations: builtins.int
    """In case of large reduction in a presolve iteration, we perform multiple
    presolve iterations. This parameter controls the maximum number of such
    presolve iterations.
    """
    cp_model_presolve: builtins.bool
    """Whether we presolve the cp_model before solving it."""
    cp_model_probing_level: builtins.int
    """How much effort do we spend on probing. 0 disables it completely."""
    cp_model_use_sat_presolve: builtins.bool
    """Whether we also use the sat presolve when cp_model_presolve is true."""
    load_at_most_ones_in_sat_presolve: builtins.bool
    """If we try to load at most ones and exactly ones constraints when running
    the pure SAT presolve. Or if we just ignore them.

    If one detects at_most_one via merge_at_most_one_work_limit or exactly one
    with find_clauses_that_are_exactly_one, it might be good to also set this
    to true.
    """
    remove_fixed_variables_early: builtins.bool
    """If cp_model_presolve is true and there is a large proportion of fixed
    variable after the first model copy, remap all the model to a dense set of
    variable before the full presolve even starts. This should help for LNS on
    large models.
    """
    detect_table_with_cost: builtins.bool
    """If true, we detect variable that are unique to a table constraint and only
    there to encode a cost on each tuple. This is usually the case when a WCSP
    (weighted constraint program) is encoded into CP-SAT format.

    This can lead to a dramatic speed-up for such problems but is still
    experimental at this point.
    """
    table_compression_level: builtins.int
    """How much we try to "compress" a table constraint. Compressing more leads to
    less Booleans and faster propagation but can reduced the quality of the lp
    relaxation. Values goes from 0 to 3 where we always try to fully compress a
    table. At 2, we try to automatically decide if it is worth it.
    """
    expand_alldiff_constraints: builtins.bool
    """If true, expand all_different constraints that are not permutations.
    Permutations (#Variables = #Values) are always expanded.
    """
    max_alldiff_domain_size: builtins.int
    """Max domain size for all_different constraints to be expanded."""
    expand_reservoir_constraints: builtins.bool
    """If true, expand the reservoir constraints by creating booleans for all
    possible precedences between event and encoding the constraint.
    """
    max_domain_size_for_linear2_expansion: builtins.int
    """Max domain size for expanding linear2 constraints (ax + by ==/!= c)."""
    expand_reservoir_using_circuit: builtins.bool
    """Mainly useful for testing.

    If this and expand_reservoir_constraints is true, we use a different
    encoding of the reservoir constraint using circuit instead of precedences.
    Note that this is usually slower, but can exercise different part of the
    solver. Note that contrary to the precedence encoding, this easily support
    variable demands.

    WARNING: with this encoding, the constraint takes a slightly different
    meaning. There must exist a permutation of the events occurring at the same
    time such that the level is within the reservoir after each of these events
    (in this permuted order). So we cannot have +100 and -100 at the same time
    if the level must be between 0 and 10 (as authorized by the reservoir
    constraint).
    """
    encode_cumulative_as_reservoir: builtins.bool
    """Encore cumulative with fixed demands and capacity as a reservoir
    constraint. The only reason you might want to do that is to test the
    reservoir propagation code!
    """
    max_lin_max_size_for_expansion: builtins.int
    """If the number of expressions in the lin_max is less that the max size
    parameter, model expansion replaces target = max(xi) by linear constraint
    with the introduction of new booleans bi such that bi => target == xi.

    This is mainly for experimenting compared to a custom lin_max propagator.
    """
    disable_constraint_expansion: builtins.bool
    """If true, it disable all constraint expansion.
    This should only be used to test the presolve of expanded constraints.
    """
    encode_complex_linear_constraint_with_integer: builtins.bool
    """Linear constraint with a complex right hand side (more than a single
    interval) need to be expanded, there is a couple of way to do that.
    """
    merge_no_overlap_work_limit: builtins.float
    """During presolve, we use a maximum clique heuristic to merge together
    no-overlap constraints or at most one constraints. This code can be slow,
    so we have a limit in place on the number of explored nodes in the
    underlying graph. The internal limit is an int64, but we use double here to
    simplify manual input.
    """
    merge_at_most_one_work_limit: builtins.float
    presolve_substitution_level: builtins.int
    """How much substitution (also called free variable aggregation in MIP
    litterature) should we perform at presolve. This currently only concerns
    variable appearing only in linear constraints. For now the value 0 turns it
    off and any positive value performs substitution.
    """
    presolve_extract_integer_enforcement: builtins.bool
    """If true, we will extract from linear constraints, enforcement literals of
    the form "integer variable at bound => simplified constraint". This should
    always be beneficial except that we don't always handle them as efficiently
    as we could for now. This causes problem on manna81.mps (LP relaxation not
    as tight it seems) and on neos-3354841-apure.mps.gz (too many literals
    created this way).
    """
    presolve_inclusion_work_limit: builtins.int
    """A few presolve operations involve detecting constraints included in other
    constraint. Since there can be a quadratic number of such pairs, and
    processing them usually involve scanning them, the complexity of these
    operations can be big. This enforce a local deterministic limit on the
    number of entries scanned. Default is 1e8.

    A value of zero will disable these presolve rules completely.
    """
    ignore_names: builtins.bool
    """If true, we don't keep names in our internal copy of the user given model."""
    infer_all_diffs: builtins.bool
    """Run a max-clique code amongst all the x != y we can find and try to infer
    set of variables that are all different. This allows to close neos16.mps
    for instance. Note that we only run this code if there is no all_diff
    already in the model so that if a user want to add some all_diff, we assume
    it is well done and do not try to add more.

    This will also detect and add no_overlap constraints, if all the relations
    x != y have "offsets" between them. I.e. x > y + offset.
    """
    find_big_linear_overlap: builtins.bool
    """Try to find large "rectangle" in the linear constraint matrix with
    identical lines. If such rectangle is big enough, we can introduce a new
    integer variable corresponding to the common expression and greatly reduce
    the number of non-zero.
    """
    find_clauses_that_are_exactly_one: builtins.bool
    """By propagating (or just using binary clauses), one can detect that all
    literal of a clause are actually in at most one relationship. Thus this
    constraint can be promoted to an exactly one constraints. This should help
    as it convey more structure. Note that this is expensive, so we have a
    deterministic limit in place.
    """
    use_sat_inprocessing: builtins.bool
    """==========================================================================
    Inprocessing
    ==========================================================================

    Enable or disable "inprocessing" which is some SAT presolving done at
    each restart to the root level.
    """
    inprocessing_dtime_ratio: builtins.float
    """Proportion of deterministic time we should spend on inprocessing.
    At each "restart", if the proportion is below this ratio, we will do some
    inprocessing, otherwise, we skip it for this restart.
    """
    inprocessing_probing_dtime: builtins.float
    """The amount of dtime we should spend on probing for each inprocessing round."""
    inprocessing_minimization_dtime: builtins.float
    """Parameters for an heuristic similar to the one described in "An effective
    learnt clause minimization approach for CDCL Sat Solvers",
    https://www.ijcai.org/proceedings/2017/0098.pdf

    This is the amount of dtime we should spend on this technique during each
    inprocessing phase.

    The minimization technique is the same as the one used to minimize core in
    max-sat. We also minimize problem clauses and not just the learned clause
    that we keep forever like in the paper.
    """
    inprocessing_minimization_use_conflict_analysis: builtins.bool
    inprocessing_minimization_use_all_orderings: builtins.bool
    inprocessing_use_congruence_closure: builtins.bool
    """Whether we use the algorithm described in "Clausal Congruence closure",
    Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, 2024.

    Note that we only have a basic version currently.
    """
    inprocessing_use_sat_sweeping: builtins.bool
    """Whether we use the SAT sweeping algorithm described in "Clausal Equivalence
    Sweeping", Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks,
    2025.
    """
    num_workers: builtins.int
    """==========================================================================
    Multithread
    ==========================================================================

    Specify the number of parallel workers (i.e. threads) to use during search.
    This should usually be lower than your number of available cpus +
    hyperthread in your machine.

    A value of 0 means the solver will try to use all cores on the machine.
    A number of 1 means no parallelism.

    Note that 'num_workers' is the preferred name, but if it is set to zero,
    we will still read the deprecated 'num_search_workers'.

    As of 2020-04-10, if you're using SAT via MPSolver (to solve integer
    programs) this field is overridden with a value of 8, if the field is not
    set *explicitly*. Thus, always set this field explicitly or via
    MPSolver::SetNumThreads().
    """
    num_search_workers: builtins.int
    num_full_subsolvers: builtins.int
    """We distinguish subsolvers that consume a full thread, and the ones that are
    always interleaved. If left at zero, we will fix this with a default
    formula that depends on num_workers. But if you start modifying what runs,
    you might want to fix that to a given value depending on the num_workers
    you use.
    """
    interleave_search: builtins.bool
    """Experimental. If this is true, then we interleave all our major search
    strategy and distribute the work amongst num_workers.

    The search is deterministic (independently of num_workers!), and we
    schedule and wait for interleave_batch_size task to be completed before
    synchronizing and scheduling the next batch of tasks.
    """
    interleave_batch_size: builtins.int
    share_objective_bounds: builtins.bool
    """Allows objective sharing between workers."""
    share_level_zero_bounds: builtins.bool
    """Allows sharing of the bounds of modified variables at level 0."""
    share_linear2_bounds: builtins.bool
    """Allows sharing of the bounds on linear2 discovered at level 0. This is
    mainly interesting on scheduling type of problems when we branch on
    precedences.

    Warning: This currently non-deterministic.
    """
    share_binary_clauses: builtins.bool
    """Allows sharing of new learned binary clause between workers."""
    share_glue_clauses: builtins.bool
    """Allows sharing of short glue clauses between workers.
    Implicitly disabled if share_binary_clauses is false.
    """
    minimize_shared_clauses: builtins.bool
    """Minimize and detect subsumption of shared clauses immediately after they
    are imported.
    """
    share_glue_clauses_dtime: builtins.float
    """The amount of dtime between each export of shared glue clauses."""
    check_lrat_proof: builtins.bool
    """==========================================================================
    Proofs
    ==========================================================================

    If true, inferred clauses are checked with an LRAT checker as they are
    learned, in presolve (reduced to trivial simplifications if
    cp_model_presolve is false), and in each worker. As of December 2025, this
    only works with pure SAT problems, with
     - cp_model_presolve = false,
     - linearization_level <= 1,
     - symmetry_level <= 1.
    """
    check_merged_lrat_proof: builtins.bool
    """If true, and if output_lrat_proof is true and the problem is UNSAT, check
    that the merged proof file is valid, i.e., that clause sharing between
    workers is correct. This checks each inferred clause, so you might want to
    disable check_lrat_proof to avoid redundant work. As of November 2025, this
    only works for pure SAT problems, with num_workers = 1.
    """
    output_lrat_proof: builtins.bool
    """If true, an LRAT proof that all the clauses inferred by the solver are
    valid is output to several files (one for presolve -- reduced to trivial
    simplifications if cp_model_presolve is false, one per worker, and one for
    the merged proof). As of December 2025, this only works for pure SAT
    problems, with
     - cp_model_presolve = false,
     - linearization_level <= 1,
     - symmetry_level <= 1.
    """
    check_drat_proof: builtins.bool
    """If true, and if the problem is UNSAT, a DRAT proof of this UNSAT property
    is checked after the solver has finished. As of November 2025, this only
    works for pure SAT problems, with
     - num_workers = 1,
     - cp_model_presolve = false,
     - linearization_level <= 1,
     - symmetry_level <= 1.
    """
    output_drat_proof: builtins.bool
    """If true, a DRAT proof that all the clauses inferred by the solver are valid
    is output to a file. As of December 2025, this only works for pure SAT
    problems, with
     - num_workers = 1,
     - cp_model_presolve = false,
     - linearization_level <= 1,
     - symmetry_level <= 1.
    """
    max_drat_time_in_seconds: builtins.float
    """The maximum time allowed to check the DRAT proof (this can take more time
    than the solve itself). Only used if check_drat_proof is true.
    """
    debug_postsolve_with_full_solver: builtins.bool
    """==========================================================================
    Debugging parameters
    ==========================================================================

    We have two different postsolve code. The default one should be better and
    it allows for a more powerful presolve, but it can be useful to postsolve
    using the full solver instead.
    """
    debug_max_num_presolve_operations: builtins.int
    """If positive, try to stop just after that many presolve rules have been
    applied. This is mainly useful for debugging presolve.
    """
    debug_crash_on_bad_hint: builtins.bool
    """Crash if we do not manage to complete the hint into a full solution."""
    debug_crash_if_presolve_breaks_hint: builtins.bool
    """Crash if presolve breaks a feasible hint."""
    debug_crash_if_lrat_check_fails: builtins.bool
    """Crash if the LRAT UNSAT proof is invalid."""
    use_optimization_hints: builtins.bool
    """==========================================================================
    Max-sat parameters
    ==========================================================================

    For an optimization problem, whether we follow some hints in order to find
    a better first solution. For a variable with hint, the solver will always
    try to follow the hint. It will revert to the variable_branching default
    otherwise.
    """
    core_minimization_level: builtins.int
    """If positive, we spend some effort on each core:
    - At level 1, we use a simple heuristic to try to minimize an UNSAT core.
    - At level 2, we use propagation to minimize the core but also identify
      literal in at most one relationship in this core.
    """
    find_multiple_cores: builtins.bool
    """Whether we try to find more independent cores for a given set of
    assumptions in the core based max-SAT algorithms.
    """
    cover_optimization: builtins.bool
    """If true, when the max-sat algo find a core, we compute the minimal number
    of literals in the core that needs to be true to have a feasible solution.
    This is also called core exhaustion in more recent max-SAT papers.
    """
    max_sat_assumption_order: Global___SatParameters.MaxSatAssumptionOrder.ValueType
    max_sat_reverse_assumption_order: builtins.bool
    """If true, adds the assumption in the reverse order of the one defined by
    max_sat_assumption_order.
    """
    max_sat_stratification: Global___SatParameters.MaxSatStratificationAlgorithm.ValueType
    propagation_loop_detection_factor: builtins.float
    """==========================================================================
    Constraint programming parameters
    ==========================================================================

    Some search decisions might cause a really large number of propagations to
    happen when integer variables with large domains are only reduced by 1 at
    each step. If we propagate more than the number of variable times this
    parameters we try to take counter-measure. Setting this to 0.0 disable this
    feature.

    TODO(user): Setting this to something like 10 helps in most cases, but the
    code is currently buggy and can cause the solve to enter a bad state where
    no progress is made.
    """
    use_precedences_in_disjunctive_constraint: builtins.bool
    """When this is true, then a disjunctive constraint will try to use the
    precedence relations between time intervals to propagate their bounds
    further. For instance if task A and B are both before C and task A and B
    are in disjunction, then we can deduce that task C must start after
    duration(A) + duration(B) instead of simply max(duration(A), duration(B)),
    provided that the start time for all task was currently zero.

    This always result in better propagation, but it is usually slow, so
    depending on the problem, turning this off may lead to a faster solution.
    """
    transitive_precedences_work_limit: builtins.int
    """At root level, we might compute the transitive closure of "precedences"
    relations so that we can exploit that in scheduling problems. Setting this
    to zero disable the feature.
    """
    max_size_to_create_precedence_literals_in_disjunctive: builtins.int
    """Create one literal for each disjunction of two pairs of tasks. This slows
    down the solve time, but improves the lower bound of the objective in the
    makespan case. This will be triggered if the number of intervals is less or
    equal than the parameter and if use_strong_propagation_in_disjunctive is
    true.
    """
    use_strong_propagation_in_disjunctive: builtins.bool
    """Enable stronger and more expensive propagation on no_overlap constraint."""
    use_dynamic_precedence_in_disjunctive: builtins.bool
    """Whether we try to branch on decision "interval A before interval B" rather
    than on intervals bounds. This usually works better, but slow down a bit
    the time to find the first solution.

    These parameters are still EXPERIMENTAL, the result should be correct, but
    it some corner cases, they can cause some failing CHECK in the solver.
    """
    use_dynamic_precedence_in_cumulative: builtins.bool
    use_overload_checker_in_cumulative: builtins.bool
    """When this is true, the cumulative constraint is reinforced with overload
    checking, i.e., an additional level of reasoning based on energy. This
    additional level supplements the default level of reasoning as well as
    timetable edge finding.

    This always result in better propagation, but it is usually slow, so
    depending on the problem, turning this off may lead to a faster solution.
    """
    use_conservative_scale_overload_checker: builtins.bool
    """Enable a heuristic to solve cumulative constraints using a modified energy
    constraint. We modify the usual energy definition by applying a
    super-additive function (also called "conservative scale" or "dual-feasible
    function") to the demand and the durations of the tasks.

    This heuristic is fast but for most problems it does not help much to find
    a solution.
    """
    use_timetable_edge_finding_in_cumulative: builtins.bool
    """When this is true, the cumulative constraint is reinforced with timetable
    edge finding, i.e., an additional level of reasoning based on the
    conjunction of energy and mandatory parts. This additional level
    supplements the default level of reasoning as well as overload_checker.

    This always result in better propagation, but it is usually slow, so
    depending on the problem, turning this off may lead to a faster solution.
    """
    max_num_intervals_for_timetable_edge_finding: builtins.int
    """Max number of intervals for the timetable_edge_finding algorithm to
    propagate. A value of 0 disables the constraint.
    """
    use_hard_precedences_in_cumulative: builtins.bool
    """If true, detect and create constraint for integer variable that are "after"
    a set of intervals in the same cumulative constraint.

    Experimental: by default we just use "direct" precedences. If
    exploit_all_precedences is true, we explore the full precedence graph. This
    assumes we have a DAG otherwise it fails.
    """
    exploit_all_precedences: builtins.bool
    use_disjunctive_constraint_in_cumulative: builtins.bool
    """When this is true, the cumulative constraint is reinforced with propagators
    from the disjunctive constraint to improve the inference on a set of tasks
    that are disjunctive at the root of the problem. This additional level
    supplements the default level of reasoning.

    Propagators of the cumulative constraint will not be used at all if all the
    tasks are disjunctive at root node.

    This always result in better propagation, but it is usually slow, so
    depending on the problem, turning this off may lead to a faster solution.
    """
    no_overlap_2d_boolean_relations_limit: builtins.int
    """If less than this number of boxes are present in a no-overlap 2d, we
    create 4 Booleans per pair of boxes:
    - Box 2 is after Box 1 on x.
    - Box 1 is after Box 2 on x.
    - Box 2 is after Box 1 on y.
    - Box 1 is after Box 2 on y.

    Note that at least one of them must be true, and at most one on x and one
    on y can be true.

    This can significantly help in closing small problem. The SAT reasoning
    can be a lot more powerful when we take decision on such positional
    relations.
    """
    use_timetabling_in_no_overlap_2d: builtins.bool
    """When this is true, the no_overlap_2d constraint is reinforced with
    propagators from the cumulative constraints. It consists of ignoring the
    position of rectangles in one position and projecting the no_overlap_2d on
    the other dimension to create a cumulative constraint. This is done on both
    axis. This additional level supplements the default level of reasoning.
    """
    use_energetic_reasoning_in_no_overlap_2d: builtins.bool
    """When this is true, the no_overlap_2d constraint is reinforced with
    energetic reasoning. This additional level supplements the default level of
    reasoning.
    """
    use_area_energetic_reasoning_in_no_overlap_2d: builtins.bool
    """When this is true, the no_overlap_2d constraint is reinforced with
    an energetic reasoning that uses an area-based energy. This can be combined
    with the two other overlap heuristics above.
    """
    use_try_edge_reasoning_in_no_overlap_2d: builtins.bool
    max_pairs_pairwise_reasoning_in_no_overlap_2d: builtins.int
    """If the number of pairs to look is below this threshold, do an extra step of
    propagation in the no_overlap_2d constraint by looking at all pairs of
    intervals.
    """
    maximum_regions_to_split_in_disconnected_no_overlap_2d: builtins.int
    """Detects when the space where items of a no_overlap_2d constraint can placed
    is disjoint (ie., fixed boxes split the domain). When it is the case, we
    can introduce a boolean for each pair <item, component> encoding whether
    the item is in the component or not. Then we replace the original
    no_overlap_2d constraint by one no_overlap_2d constraint for each
    component, with the new booleans as the enforcement_literal of the
    intervals. This is equivalent to expanding the original no_overlap_2d
    constraint into a bin packing problem with each connected component being a
    bin. This heuristic is only done when the number of regions to split
    is less than this parameter and <= 1 disables it.
    """
    use_linear3_for_no_overlap_2d_precedences: builtins.bool
    """When set, this activates a propagator for the no_overlap_2d constraint that
    uses any eventual linear constraints of the model in the form
    `{start interval 1} - {end interval 2} + c*w <= ub` to detect that two
    intervals must overlap in one dimension for some values of `w`. This is
    particularly useful for problems where the distance between two boxes is
    part of the model.
    """
    use_dual_scheduling_heuristics: builtins.bool
    """When set, it activates a few scheduling parameters to improve the lower
    bound of scheduling problems. This is only effective with multiple workers
    as it modifies the reduced_cost, lb_tree_search, and probing workers.
    """
    use_all_different_for_circuit: builtins.bool
    """Turn on extra propagation for the circuit constraint.
    This can be quite slow.
    """
    routing_cut_subset_size_for_binary_relation_bound: builtins.int
    """If the size of a subset of nodes of a RoutesConstraint is less than this
    value, use linear constraints of size 1 and 2 (such as capacity and time
    window constraints) enforced by the arc literals to compute cuts for this
    subset (unless the subset size is less than
    routing_cut_subset_size_for_tight_binary_relation_bound, in which case the
    corresponding algorithm is used instead). The algorithm for these cuts has
    a O(n^3) complexity, where n is the subset size. Hence the value of this
    parameter should not be too large (e.g. 10 or 20).
    """
    routing_cut_subset_size_for_tight_binary_relation_bound: builtins.int
    """Similar to above, but with a different algorithm producing better cuts, at
    the price of a higher O(2^n) complexity, where n is the subset size. Hence
    the value of this parameter should be small (e.g. less than 10).
    """
    routing_cut_subset_size_for_exact_binary_relation_bound: builtins.int
    """Similar to above, but with an even stronger algorithm in O(n!). We try to
    be defensive and abort early or not run that often. Still the value of
    that parameter shouldn't really be much more than 10.
    """
    routing_cut_subset_size_for_shortest_paths_bound: builtins.int
    """Similar to routing_cut_subset_size_for_exact_binary_relation_bound but
    use a bound based on shortest path distances (which respect triangular
    inequality). This allows to derive bounds that are valid for any superset
    of a given subset. This is slow, so it shouldn't really be larger than 10.
    """
    routing_cut_dp_effort: builtins.float
    """The amount of "effort" to spend in dynamic programming for computing
    routing cuts. This is in term of basic operations needed by the algorithm
    in the worst case, so a value like 1e8 should take less than a second to
    compute.
    """
    routing_cut_max_infeasible_path_length: builtins.int
    """If the length of an infeasible path is less than this value, a cut will be
    added to exclude it.
    """
    search_branching: Global___SatParameters.SearchBranching.ValueType
    hint_conflict_limit: builtins.int
    """Conflict limit used in the phase that exploit the solution hint."""
    repair_hint: builtins.bool
    """If true, the solver tries to repair the solution given in the hint. This
    search terminates after the 'hint_conflict_limit' is reached and the solver
    switches to regular search. If false, then  we do a FIXED_SEARCH using the
    hint until the hint_conflict_limit is reached.
    """
    fix_variables_to_their_hinted_value: builtins.bool
    """If true, variables appearing in the solution hints will be fixed to their
    hinted value.
    """
    use_probing_search: builtins.bool
    """If true, search will continuously probe Boolean variables, and integer
    variable bounds. This parameter is set to true in parallel on the probing
    worker.
    """
    use_extended_probing: builtins.bool
    """Use extended probing (probe bool_or, at_most_one, exactly_one)."""
    probing_num_combinations_limit: builtins.int
    """How many combinations of pairs or triplets of variables we want to scan."""
    shaving_deterministic_time_in_probing_search: builtins.float
    """Add a shaving phase (where the solver tries to prove that the lower or
    upper bound of a variable are infeasible) to the probing search. (<= 0
    disables it).
    """
    shaving_search_deterministic_time: builtins.float
    """Specifies the amount of deterministic time spent of each try at shaving a
    bound in the shaving search.
    """
    shaving_search_threshold: builtins.int
    """Specifies the threshold between two modes in the shaving procedure.
    If the range of the variable/objective is less than this threshold, then
    the shaving procedure will try to remove values one by one. Otherwise, it
    will try to remove one range at a time.
    """
    use_objective_lb_search: builtins.bool
    """If true, search will search in ascending max objective value (when
    minimizing) starting from the lower bound of the objective.
    """
    use_objective_shaving_search: builtins.bool
    """This search differs from the previous search as it will not use assumptions
    to bound the objective, and it will recreate a full model with the
    hardcoded objective value.
    """
    variables_shaving_level: builtins.int
    """This search takes all Boolean or integer variables, and maximize or
    minimize them in order to reduce their domain. -1 is automatic, otherwise
    value 0 disables it, and 1, 2, or 3 changes something.
    """
    pseudo_cost_reliability_threshold: builtins.int
    """The solver ignores the pseudo costs of variables with number of recordings
    less than this threshold.
    """
    optimize_with_core: builtins.bool
    """The default optimization method is a simple "linear scan", each time trying
    to find a better solution than the previous one. If this is true, then we
    use a core-based approach (like in max-SAT) when we try to increase the
    lower bound instead.
    """
    optimize_with_lb_tree_search: builtins.bool
    """Do a more conventional tree search (by opposition to SAT based one) where
    we keep all the explored node in a tree. This is meant to be used in a
    portfolio and focus on improving the objective lower bound. Keeping the
    whole tree allow us to report a better objective lower bound coming from
    the worst open node in the tree.
    """
    save_lp_basis_in_lb_tree_search: builtins.bool
    """Experimental. Save the current LP basis at each node of the search tree so
    that when we jump around, we can load it and reduce the number of LP
    iterations needed.

    It currently works okay if we do not change the lp with cuts or
    simplification... More work is needed to make it robust in all cases.
    """
    binary_search_num_conflicts: builtins.int
    """If non-negative, perform a binary search on the objective variable in order
    to find an [min, max] interval outside of which the solver proved unsat/sat
    under this amount of conflict. This can quickly reduce the objective domain
    on some problems.
    """
    optimize_with_max_hs: builtins.bool
    """This has no effect if optimize_with_core is false. If true, use a different
    core-based algorithm similar to the max-HS algo for max-SAT. This is a
    hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT
    one. This is also related to the PhD work of tobyodavies@
    "Automatic Logic-Based Benders Decomposition with MiniZinc"
    http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
    """
    use_feasibility_jump: builtins.bool
    """Parameters for an heuristic similar to the one described in the paper:
    "Feasibility Jump: an LP-free Lagrangian MIP heuristic", Bjørnar
    Luteberget, Giorgio Sartor, 2023, Mathematical Programming Computation.
    """
    use_ls_only: builtins.bool
    """Disable every other type of subsolver, setting this turns CP-SAT into a
    pure local-search solver.
    """
    feasibility_jump_decay: builtins.float
    """On each restart, we randomly choose if we use decay (with this parameter)
    or no decay.
    """
    feasibility_jump_linearization_level: builtins.int
    """How much do we linearize the problem in the local search code."""
    feasibility_jump_restart_factor: builtins.int
    """This is a factor that directly influence the work before each restart.
    Increasing it leads to longer restart.
    """
    feasibility_jump_batch_dtime: builtins.float
    """How much dtime for each LS batch."""
    feasibility_jump_var_randomization_probability: builtins.float
    """Probability for a variable to have a non default value upon restarts or
    perturbations.
    """
    feasibility_jump_var_perburbation_range_ratio: builtins.float
    """Max distance between the default value and the pertubated value relative to
    the range of the domain of the variable.
    """
    feasibility_jump_enable_restarts: builtins.bool
    """When stagnating, feasibility jump will either restart from a default
    solution (with some possible randomization), or randomly pertubate the
    current solution. This parameter selects the first option.
    """
    feasibility_jump_max_expanded_constraint_size: builtins.int
    """Maximum size of no_overlap or no_overlap_2d constraint for a quadratic
    expansion. This might look a lot, but by expanding such constraint, we get
    a linear time evaluation per single variable moves instead of a slow O(n
    log n) one.
    """
    num_violation_ls: builtins.int
    """This will create incomplete subsolvers (that are not LNS subsolvers)
    that use the feasibility jump code to find improving solution, treating
    the objective improvement as a hard constraint.
    """
    violation_ls_perturbation_period: builtins.int
    """How long violation_ls should wait before perturbating a solution."""
    violation_ls_compound_move_probability: builtins.float
    """Probability of using compound move search each restart.
    TODO(user): Add reference to paper when published.
    """
    shared_tree_num_workers: builtins.int
    """Enables shared tree search.
    If positive, start this many complete worker threads to explore a shared
    search tree. These workers communicate objective bounds and simple decision
    nogoods relating to the shared prefix of the tree, and will avoid exploring
    the same subtrees as one another.
    Specifying a negative number uses a heuristic to select an appropriate
    number of shared tree workeres based on the total number of workers.
    """
    use_shared_tree_search: builtins.bool
    """Set on shared subtree workers. Users should not set this directly."""
    shared_tree_worker_min_restarts_per_subtree: builtins.int
    """Minimum restarts before a worker will replace a subtree
    that looks "bad" based on the average LBD of learned clauses.
    """
    shared_tree_worker_enable_trail_sharing: builtins.bool
    """If true, workers share more of the information from their local trail.
    Specifically, literals implied by the shared tree decisions.
    """
    shared_tree_worker_enable_phase_sharing: builtins.bool
    """If true, shared tree workers share their target phase when returning an
    assigned subtree for the next worker to use.
    """
    shared_tree_open_leaves_per_worker: builtins.float
    """How many open leaf nodes should the shared tree maintain per worker."""
    shared_tree_max_nodes_per_worker: builtins.int
    """In order to limit total shared memory and communication overhead, limit the
    total number of nodes that may be generated in the shared tree. If the
    shared tree runs out of unassigned leaves, workers act as portfolio
    workers. Note: this limit includes interior nodes, not just leaves.
    """
    shared_tree_split_strategy: Global___SatParameters.SharedTreeSplitStrategy.ValueType
    shared_tree_balance_tolerance: builtins.int
    """How much deeper compared to the ideal max depth of the tree is considered
    "balanced" enough to still accept a split. Without such a tolerance,
    sometimes the tree can only be split by a single worker, and they may not
    generate a split for some time. In contrast, with a tolerance of 1, at
    least half of all workers should be able to split the tree as soon as a
    split becomes required. This only has an effect on
    SPLIT_STRATEGY_BALANCED_TREE and SPLIT_STRATEGY_DISCREPANCY.
    """
    shared_tree_split_min_dtime: builtins.float
    """How much dtime a worker will wait between proposing splits.
    This limits the contention in splitting the shared tree, and also reduces
    the number of too-easy subtrees that are generates.
    """
    enumerate_all_solutions: builtins.bool
    """Whether we enumerate all solutions of a problem without objective.

    WARNING:
    - This can be used with num_workers > 1 but then each solutions can be
      found more than once, so it is up to the client to deduplicate them.
    - If keep_all_feasible_solutions_in_presolve is unset, we will set it to
      true as otherwise, many feasible solution can just be removed by the
      presolve. It is still possible to manually set this to false if one only
      wants to enumerate all solutions of the presolved model.
    """
    keep_all_feasible_solutions_in_presolve: builtins.bool
    """If true, we disable the presolve reductions that remove feasible solutions
    from the search space. Such solution are usually dominated by a "better"
    solution that is kept, but depending on the situation, we might want to
    keep all solutions.

    A trivial example is when a variable is unused. If this is true, then the
    presolve will not fix it to an arbitrary value and it will stay in the
    search space.
    """
    fill_tightened_domains_in_response: builtins.bool
    """If true, add information about the derived variable domains to the
    CpSolverResponse. It is an option because it makes the response slighly
    bigger and there is a bit more work involved during the postsolve to
    construct it, but it should still have a low overhead. See the
    tightened_variables field in CpSolverResponse for more details.
    """
    fill_additional_solutions_in_response: builtins.bool
    """If true, the final response addition_solutions field will be filled with
    all solutions from our solutions pool.

    Note that if both this field and enumerate_all_solutions is true, we will
    copy to the pool all of the solution found. So if solution_pool_size is big
    enough, you can get all solutions this way instead of using the solution
    callback.

    Note that this only affect the "final" solution, not the one passed to the
    solution callbacks.
    """
    instantiate_all_variables: builtins.bool
    """If true, the solver will add a default integer branching strategy to the
    already defined search strategy. If not, some variable might still not be
    fixed at the end of the search. For now we assume these variable can just
    be set to their lower bound.
    """
    auto_detect_greater_than_at_least_one_of: builtins.bool
    """If true, then the precedences propagator try to detect for each variable if
    it has a set of "optional incoming arc" for which at least one of them is
    present. This is usually useful to have but can be slow on model with a lot
    of precedence.
    """
    stop_after_first_solution: builtins.bool
    """For an optimization problem, stop the solver as soon as we have a solution."""
    stop_after_presolve: builtins.bool
    """Mainly used when improving the presolver. When true, stops the solver after
    the presolve is complete (or after loading and root level propagation).
    """
    stop_after_root_propagation: builtins.bool
    lns_initial_difficulty: builtins.float
    """LNS parameters.

    Initial parameters for neighborhood generation.
    """
    lns_initial_deterministic_limit: builtins.float
    use_lns: builtins.bool
    """Testing parameters used to disable all lns workers."""
    use_lns_only: builtins.bool
    """Experimental parameters to disable everything but lns."""
    solution_pool_size: builtins.int
    """Size of the top-n different solutions kept by the solver.
    This parameter must be > 0. Currently, having this larger than one mainly
    impact the "base" solution chosen for a LNS/LS fragment.
    """
    solution_pool_diversity_limit: builtins.int
    """If solution_pool_size is <= this, we will use DP to keep a "diverse" set
    of solutions (the one further apart via hamming distance) in the pool.
    Setting this to large value might be slow, especially if your solution are
    large.
    """
    alternative_pool_size: builtins.int
    """In order to not get stuck in local optima, when this is non-zero, we try to
    also work on "older" solutions with a worse objective value so we get a
    chance to follow a different LS/LNS trajectory.
    """
    use_rins_lns: builtins.bool
    """Turns on relaxation induced neighborhood generator."""
    use_feasibility_pump: builtins.bool
    """Adds a feasibility pump subsolver along with lns subsolvers."""
    use_lb_relax_lns: builtins.bool
    """Turns on neighborhood generator based on local branching LP. Based on Huang
    et al., "Local Branching Relaxation Heuristics for Integer Linear
    Programs", 2023.
    """
    lb_relax_num_workers_threshold: builtins.int
    """Only use lb-relax if we have at least that many workers."""
    fp_rounding: Global___SatParameters.FPRoundingMethod.ValueType
    diversify_lns_params: builtins.bool
    """If true, registers more lns subsolvers with different parameters."""
    randomize_search: builtins.bool
    """Randomize fixed search."""
    search_random_variable_pool_size: builtins.int
    """Search randomization will collect the top
    'search_random_variable_pool_size' valued variables, and pick one randomly.
    The value of the variable is specific to each strategy.
    """
    push_all_tasks_toward_start: builtins.bool
    """Experimental code: specify if the objective pushes all tasks toward the
    start of the schedule.
    """
    use_optional_variables: builtins.bool
    """If true, we automatically detect variables whose constraint are always
    enforced by the same literal and we mark them as optional. This allows
    to propagate them as if they were present in some situation.

    TODO(user): This is experimental and seems to lead to wrong optimal in
    some situation. It should however gives correct solutions. Fix.
    """
    use_exact_lp_reason: builtins.bool
    """The solver usually exploit the LP relaxation of a model. If this option is
    true, then whatever is infered by the LP will be used like an heuristic to
    compute EXACT propagation on the IP. So with this option, there is no
    numerical imprecision issues.
    """
    use_combined_no_overlap: builtins.bool
    """This can be beneficial if there is a lot of no-overlap constraints but a
    relatively low number of different intervals in the problem. Like 1000
    intervals, but 1M intervals in the no-overlap constraints covering them.
    """
    at_most_one_max_expansion_size: builtins.int
    """All at_most_one constraints with a size <= param will be replaced by a
    quadratic number of binary implications.
    """
    catch_sigint_signal: builtins.bool
    """Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
    when calling solve. If set, catching the SIGINT signal will terminate the
    search gracefully, as if a time limit was reached.
    """
    use_implied_bounds: builtins.bool
    """Stores and exploits "implied-bounds" in the solver. That is, relations of
    the form literal => (var >= bound). This is currently used to derive
    stronger cuts.
    """
    polish_lp_solution: builtins.bool
    """Whether we try to do a few degenerate iteration at the end of an LP solve
    to minimize the fractionality of the integer variable in the basis. This
    helps on some problems, but not so much on others. It also cost of bit of
    time to do such polish step.
    """
    lp_primal_tolerance: builtins.float
    """The internal LP tolerances used by CP-SAT. These applies to the internal
    and scaled problem. If the domains of your variables are large it might be
    good to use lower tolerances. If your problem is binary with low
    coefficients, it might be good to use higher ones to speed-up the lp
    solves.
    """
    lp_dual_tolerance: builtins.float
    convert_intervals: builtins.bool
    """Temporary flag util the feature is more mature. This convert intervals to
    the newer proto format that support affine start/var/end instead of just
    variables.
    """
    symmetry_level: builtins.int
    """Whether we try to automatically detect the symmetries in a model and
    exploit them. Currently, at level 1 we detect them in presolve and try
    to fix Booleans. At level 2, we also do some form of dynamic symmetry
    breaking during search. At level 3, we also detect symmetries for very
    large models, which can be slow. At level 4, we try to break as much
    symmetry as possible in presolve.
    """
    use_symmetry_in_lp: builtins.bool
    """When we have symmetry, it is possible to "fold" all variables from the same
    orbit into a single variable, while having the same power of LP relaxation.
    This can help significantly on symmetric problem. However there is
    currently a bit of overhead as the rest of the solver need to do some
    translation between the folded LP and the rest of the problem.
    """
    keep_symmetry_in_presolve: builtins.bool
    """Experimental. This will compute the symmetry of the problem once and for
    all. All presolve operations we do should keep the symmetry group intact
    or modify it properly. For now we have really little support for this. We
    will disable a bunch of presolve operations that could be supported.
    """
    symmetry_detection_deterministic_time_limit: builtins.float
    """Deterministic time limit for symmetry detection."""
    new_linear_propagation: builtins.bool
    """The new linear propagation code treat all constraints at once and use
    an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter
    order and potentially detect propagation cycle earlier.
    """
    linear_split_size: builtins.int
    """Linear constraints that are not pseudo-Boolean and that are longer than
    this size will be split into sqrt(size) intermediate sums in order to have
    faster propation in the CP engine.
    """
    linearization_level: builtins.int
    """==========================================================================
    Linear programming relaxation
    ==========================================================================

    A non-negative level indicating the type of constraints we consider in the
    LP relaxation. At level zero, no LP relaxation is used. At level 1, only
    the linear constraint and full encoding are added. At level 2, we also add
    all the Boolean constraints.
    """
    boolean_encoding_level: builtins.int
    """A non-negative level indicating how much we should try to fully encode
    Integer variables as Boolean.
    """
    max_domain_size_when_encoding_eq_neq_constraints: builtins.int
    """When loading a*x + b*y ==/!= c when x and y are both fully encoded.
    The solver may decide to replace the linear equation by a set of clauses.
    This is triggered if the sizes of the domains of x and y are below the
    threshold.
    """
    max_num_cuts: builtins.int
    """The limit on the number of cuts in our cut pool. When this is reached we do
    not generate cuts anymore.

    TODO(user): We should probably remove this parameters, and just always
    generate cuts but only keep the best n or something.
    """
    cut_level: builtins.int
    """Control the global cut effort. Zero will turn off all cut. For now we just
    have one level. Note also that most cuts are only used at linearization
    level >= 2.
    """
    only_add_cuts_at_level_zero: builtins.bool
    """For the cut that can be generated at any level, this control if we only
    try to generate them at the root node.
    """
    add_objective_cut: builtins.bool
    """When the LP objective is fractional, do we add the cut that forces the
    linear objective expression to be greater or equal to this fractional value
    rounded up? We can always do that since our objective is integer, and
    combined with MIR heuristic to reduce the coefficient of such cut, it can
    help.
    """
    add_cg_cuts: builtins.bool
    """Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
    Note that for now, this is not heavily tuned.
    """
    add_mir_cuts: builtins.bool
    """Whether we generate MIR cuts at root node.
    Note that for now, this is not heavily tuned.
    """
    add_zero_half_cuts: builtins.bool
    """Whether we generate Zero-Half cuts at root node.
    Note that for now, this is not heavily tuned.
    """
    add_clique_cuts: builtins.bool
    """Whether we generate clique cuts from the binary implication graph. Note
    that as the search goes on, this graph will contains new binary clauses
    learned by the SAT engine.
    """
    add_rlt_cuts: builtins.bool
    """Whether we generate RLT cuts. This is still experimental but can help on
    binary problem with a lot of clauses of size 3.
    """
    max_all_diff_cut_size: builtins.int
    """Cut generator for all diffs can add too many cuts for large all_diff
    constraints. This parameter restricts the large all_diff constraints to
    have a cut generator.
    """
    add_lin_max_cuts: builtins.bool
    """For the lin max constraints, generates the cuts described in "Strong
    mixed-integer programming formulations for trained neural networks" by Ross
    Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
    """
    max_integer_rounding_scaling: builtins.int
    """In the integer rounding procedure used for MIR and Gomory cut, the maximum
    "scaling" we use (must be positive). The lower this is, the lower the
    integer coefficients of the cut will be. Note that cut generated by lower
    values are not necessarily worse than cut generated by larger value. There
    is no strict dominance relationship.

    Setting this to 2 result in the "strong fractional rouding" of Letchford
    and Lodi.
    """
    add_lp_constraints_lazily: builtins.bool
    """If true, we start by an empty LP, and only add constraints not satisfied
    by the current LP solution batch by batch. A constraint that is only added
    like this is known as a "lazy" constraint in the literature, except that we
    currently consider all constraints as lazy here.
    """
    root_lp_iterations: builtins.int
    """Even at the root node, we do not want to spend too much time on the LP if
    it is "difficult". So we solve it in "chunks" of that many iterations. The
    solve will be continued down in the tree or the next time we go back to the
    root node.
    """
    min_orthogonality_for_lp_constraints: builtins.float
    """While adding constraints, skip the constraints which have orthogonality
    less than 'min_orthogonality_for_lp_constraints' with already added
    constraints during current call. Orthogonality is defined as 1 -
    cosine(vector angle between constraints). A value of zero disable this
    feature.
    """
    max_cut_rounds_at_level_zero: builtins.int
    """Max number of time we perform cut generation and resolve the LP at level 0."""
    max_consecutive_inactive_count: builtins.int
    """If a constraint/cut in LP is not active for that many consecutive OPTIMAL
    solves, remove it from the LP. Note that it might be added again later if
    it become violated by the current LP solution.
    """
    cut_max_active_count_value: builtins.float
    """These parameters are similar to sat clause management activity parameters.
    They are effective only if the number of generated cuts exceed the storage
    limit. Default values are based on a few experiments on miplib instances.
    """
    cut_active_count_decay: builtins.float
    cut_cleanup_target: builtins.int
    """Target number of constraints to remove during cleanup."""
    new_constraints_batch_size: builtins.int
    """Add that many lazy constraints (or cuts) at once in the LP. Note that at
    the beginning of the solve, we do add more than this.
    """
    exploit_integer_lp_solution: builtins.bool
    """All the "exploit_*" parameters below work in the same way: when branching
    on an IntegerVariable, these parameters affect the value the variable is
    branched on. Currently the first heuristic that triggers win in the order
    in which they appear below.

    TODO(user): Maybe do like for the restart algorithm, introduce an enum
    and a repeated field that control the order on which these are applied?

    If true and the Lp relaxation of the problem has an integer optimal
    solution, try to exploit it. Note that since the LP relaxation may not
    contain all the constraints, such a solution is not necessarily a solution
    of the full problem.
    """
    exploit_all_lp_solution: builtins.bool
    """If true and the Lp relaxation of the problem has a solution, try to exploit
    it. This is same as above except in this case the lp solution might not be
    an integer solution.
    """
    exploit_best_solution: builtins.bool
    """When branching on a variable, follow the last best solution value."""
    exploit_relaxation_solution: builtins.bool
    """When branching on a variable, follow the last best relaxation solution
    value. We use the relaxation with the tightest bound on the objective as
    the best relaxation solution.
    """
    exploit_objective: builtins.bool
    """When branching an a variable that directly affect the objective,
    branch on the value that lead to the best objective first.
    """
    detect_linearized_product: builtins.bool
    """Infer products of Boolean or of Boolean time IntegerVariable from the
    linear constrainst in the problem. This can be used in some cuts, altough
    for now we don't really exploit it.
    """
    use_new_integer_conflict_resolution: builtins.bool
    """This should be better on integer problems.
    But it is still work in progress.
    """
    create_1uip_boolean_during_icr: builtins.bool
    """If true, and during integer conflict resolution (icr) the 1-UIP is an
    integer literal for which we do not have an associated Boolean. Create one.
    """
    mip_max_bound: builtins.float
    """==========================================================================
    MIP -> CP-SAT (i.e. IP with integer coeff) conversion parameters that are
    used by our automatic "scaling" algorithm.

    Note that it is hard to do a meaningful conversion automatically and if
    you have a model with continuous variables, it is best if you scale the
    domain of the variable yourself so that you have a relevant precision for
    the application at hand. Same for the coefficients and constraint bounds.
    ==========================================================================

    We need to bound the maximum magnitude of the variables for CP-SAT, and
    that is the bound we use. If the MIP model expect larger variable value in
    the solution, then the converted model will likely not be relevant.
    """
    mip_var_scaling: builtins.float
    """All continuous variable of the problem will be multiplied by this factor.
    By default, we don't do any variable scaling and rely on the MIP model to
    specify continuous variable domain with the wanted precision.
    """
    mip_scale_large_domain: builtins.bool
    """If this is false, then mip_var_scaling is only applied to variables with
    "small" domain. If it is true, we scale all floating point variable
    independenlty of their domain.
    """
    mip_automatically_scale_variables: builtins.bool
    """If true, some continuous variable might be automatically scaled. For now,
    this is only the case where we detect that a variable is actually an
    integer multiple of a constant. For instance, variables of the form k * 0.5
    are quite frequent, and if we detect this, we will scale such variable
    domain by 2 to make it implied integer.
    """
    only_solve_ip: builtins.bool
    """If one try to solve a MIP model with CP-SAT, because we assume all variable
    to be integer after scaling, we will not necessarily have the correct
    optimal. Note however that all feasible solutions are valid since we will
    just solve a more restricted version of the original problem.

    This parameters is here to prevent user to think the solution is optimal
    when it might not be. One will need to manually set this to false to solve
    a MIP model where the optimal might be different.

    Note that this is tested after some MIP presolve steps, so even if not
    all original variable are integer, we might end up with a pure IP after
    presolve and after implied integer detection.
    """
    mip_wanted_precision: builtins.float
    """When scaling constraint with double coefficients to integer coefficients,
    we will multiply by a power of 2 and round the coefficients. We will choose
    the lowest power such that we have no potential overflow (see
    mip_max_activity_exponent) and the worst case constraint activity error
    does not exceed this threshold.

    Note that we also detect constraint with rational coefficients and scale
    them accordingly when it seems better instead of using a power of 2.

    We also relax all constraint bounds by this absolute value. For pure
    integer constraint, if this value if lower than one, this will not change
    anything. However it is needed when scaling MIP problems.

    If we manage to scale a constraint correctly, the maximum error we can make
    will be twice this value (once for the scaling error and once for the
    relaxed bounds). If we are not able to scale that well, we will display
    that fact but still scale as best as we can.
    """
    mip_max_activity_exponent: builtins.int
    """To avoid integer overflow, we always force the maximum possible constraint
    activity (and objective value) according to the initial variable domain to
    be smaller than 2 to this given power. Because of this, we cannot always
    reach the "mip_wanted_precision" parameter above.

    This can go as high as 62, but some internal algo currently abort early if
    they might run into integer overflow, so it is better to keep it a bit
    lower than this.
    """
    mip_check_precision: builtins.float
    """As explained in mip_precision and mip_max_activity_exponent, we cannot
    always reach the wanted precision during scaling. We use this threshold to
    enphasize in the logs when the precision seems bad.
    """
    mip_compute_true_objective_bound: builtins.bool
    """Even if we make big error when scaling the objective, we can always derive
    a correct lower bound on the original objective by using the exact lower
    bound on the scaled integer version of the objective. This should be fast,
    but if you don't care about having a precise lower bound, you can turn it
    off.
    """
    mip_max_valid_magnitude: builtins.float
    """Any finite values in the input MIP must be below this threshold, otherwise
    the model will be reported invalid. This is needed to avoid floating point
    overflow when evaluating bounds * coeff for instance. We are a bit more
    defensive, but in practice, users shouldn't use super large values in a
    MIP.
    """
    mip_treat_high_magnitude_bounds_as_infinity: builtins.bool
    """By default, any variable/constraint bound with a finite value and a
    magnitude greater than the mip_max_valid_magnitude will result with a
    invalid model. This flags change the behavior such that such bounds are
    silently transformed to +∞ or -∞.

    It is recommended to keep it at false, and create valid bounds.
    """
    mip_drop_tolerance: builtins.float
    """Any value in the input mip with a magnitude lower than this will be set to
    zero. This is to avoid some issue in LP presolving.
    """
    mip_presolve_level: builtins.int
    """When solving a MIP, we do some basic floating point presolving before
    scaling the problem to integer to be handled by CP-SAT. This control how
    much of that presolve we do. It can help to better scale floating point
    model, but it is not always behaving nicely.
    """
    @property
    def restart_algorithms(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[Global___SatParameters.RestartAlgorithm.ValueType]:
        """The restart strategies will change each time the strategy_counter is
        increased. The current strategy will simply be the one at index
        strategy_counter modulo the number of strategy. Note that if this list
        includes a NO_RESTART, nothing will change when it is reached because the
        strategy_counter will only increment after a restart.

        The idea of switching of search strategy tailored for SAT/UNSAT comes from
        Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/.
        But more generally, it seems REALLY beneficial to try different strategy.
        """

    @property
    def subsolvers(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.str]:
        """In multi-thread, the solver can be mainly seen as a portfolio of solvers
        with different parameters. This field indicates the names of the parameters
        that are used in multithread. This only applies to "full" subsolvers.

        See cp_model_search.cc to see a list of the names and the default value (if
        left empty) that looks like:
        - default_lp           (linearization_level:1)
        - fixed                (only if fixed search specified or scheduling)
        - no_lp                (linearization_level:0)
        - max_lp               (linearization_level:2)
        - pseudo_costs         (only if objective, change search heuristic)
        - reduced_costs        (only if objective, change search heuristic)
        - quick_restart        (kind of probing)
        - quick_restart_no_lp  (kind of probing with linearization_level:0)
        - lb_tree_search       (to improve lower bound, MIP like tree search)
        - probing              (continuous probing and shaving)

        Also, note that some set of parameters will be ignored if they do not make
        sense. For instance if there is no objective, pseudo_cost or reduced_cost
        search will be ignored. Core based search will only work if the objective
        has many terms. If there is no fixed strategy fixed will be ignored. And so
        on.

        The order is important, as only the first num_full_subsolvers will be
        scheduled. You can see in the log which one are selected for a given run.
        """

    @property
    def extra_subsolvers(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.str]:
        """A convenient way to add more workers types.
        These will be added at the beginning of the list.
        """

    @property
    def ignore_subsolvers(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.str]:
        """Rather than fully specifying subsolvers, it is often convenient to just
        remove the ones that are not useful on a given problem or only keep
        specific ones for testing. Each string is interpreted as a "glob", so we
        support '*' and '?'.

        The way this work is that we will only accept a name that match a filter
        pattern (if non-empty) and do not match an ignore pattern. Note also that
        these fields work on LNS or LS names even if these are currently not
        specified via the subsolvers field.
        """

    @property
    def filter_subsolvers(self) -> google.protobuf.internal.containers.RepeatedScalarFieldContainer[builtins.str]: ...
    @property
    def subsolver_params(self) -> google.protobuf.internal.containers.RepeatedCompositeFieldContainer[Global___SatParameters]:
        """It is possible to specify additional subsolver configuration. These can be
        referred by their params.name() in the fields above. Note that only the
        specified field will "overwrite" the ones of the base parameter. If a
        subsolver_params has the name of an existing subsolver configuration, the
        named parameters will be merged into the subsolver configuration.
        """

    def __init__(
        self,
        *,
        name: builtins.str | None = ...,
        preferred_variable_order: Global___SatParameters.VariableOrder.ValueType | None = ...,
        initial_polarity: Global___SatParameters.Polarity.ValueType | None = ...,
        use_phase_saving: builtins.bool | None = ...,
        polarity_rephase_increment: builtins.int | None = ...,
        polarity_exploit_ls_hints: builtins.bool | None = ...,
        random_polarity_ratio: builtins.float | None = ...,
        random_branches_ratio: builtins.float | None = ...,
        use_erwa_heuristic: builtins.bool | None = ...,
        initial_variables_activity: builtins.float | None = ...,
        also_bump_variables_in_conflict_reasons: builtins.bool | None = ...,
        minimization_algorithm: Global___SatParameters.ConflictMinimizationAlgorithm.ValueType | None = ...,
        binary_minimization_algorithm: Global___SatParameters.BinaryMinizationAlgorithm.ValueType | None = ...,
        subsumption_during_conflict_analysis: builtins.bool | None = ...,
        extra_subsumption_during_conflict_analysis: builtins.bool | None = ...,
        decision_subsumption_during_conflict_analysis: builtins.bool | None = ...,
        eagerly_subsume_last_n_conflicts: builtins.int | None = ...,
        subsume_during_vivification: builtins.bool | None = ...,
        use_chronological_backtracking: builtins.bool | None = ...,
        max_backjump_levels: builtins.int | None = ...,
        chronological_backtrack_min_conflicts: builtins.int | None = ...,
        clause_cleanup_period: builtins.int | None = ...,
        clause_cleanup_period_increment: builtins.int | None = ...,
        clause_cleanup_target: builtins.int | None = ...,
        clause_cleanup_ratio: builtins.float | None = ...,
        clause_cleanup_lbd_bound: builtins.int | None = ...,
        clause_cleanup_lbd_tier1: builtins.int | None = ...,
        clause_cleanup_lbd_tier2: builtins.int | None = ...,
        clause_cleanup_ordering: Global___SatParameters.ClauseOrdering.ValueType | None = ...,
        pb_cleanup_increment: builtins.int | None = ...,
        pb_cleanup_ratio: builtins.float | None = ...,
        variable_activity_decay: builtins.float | None = ...,
        max_variable_activity_value: builtins.float | None = ...,
        glucose_max_decay: builtins.float | None = ...,
        glucose_decay_increment: builtins.float | None = ...,
        glucose_decay_increment_period: builtins.int | None = ...,
        clause_activity_decay: builtins.float | None = ...,
        max_clause_activity_value: builtins.float | None = ...,
        restart_algorithms: collections.abc.Iterable[Global___SatParameters.RestartAlgorithm.ValueType] | None = ...,
        default_restart_algorithms: builtins.str | None = ...,
        restart_period: builtins.int | None = ...,
        restart_running_window_size: builtins.int | None = ...,
        restart_dl_average_ratio: builtins.float | None = ...,
        restart_lbd_average_ratio: builtins.float | None = ...,
        use_blocking_restart: builtins.bool | None = ...,
        blocking_restart_window_size: builtins.int | None = ...,
        blocking_restart_multiplier: builtins.float | None = ...,
        num_conflicts_before_strategy_changes: builtins.int | None = ...,
        strategy_change_increase_ratio: builtins.float | None = ...,
        max_time_in_seconds: builtins.float | None = ...,
        max_deterministic_time: builtins.float | None = ...,
        max_num_deterministic_batches: builtins.int | None = ...,
        max_number_of_conflicts: builtins.int | None = ...,
        max_memory_in_mb: builtins.int | None = ...,
        absolute_gap_limit: builtins.float | None = ...,
        relative_gap_limit: builtins.float | None = ...,
        random_seed: builtins.int | None = ...,
        permute_variable_randomly: builtins.bool | None = ...,
        permute_presolve_constraint_order: builtins.bool | None = ...,
        use_absl_random: builtins.bool | None = ...,
        log_search_progress: builtins.bool | None = ...,
        log_subsolver_statistics: builtins.bool | None = ...,
        log_prefix: builtins.str | None = ...,
        log_to_stdout: builtins.bool | None = ...,
        log_to_response: builtins.bool | None = ...,
        use_pb_resolution: builtins.bool | None = ...,
        minimize_reduction_during_pb_resolution: builtins.bool | None = ...,
        count_assumption_levels_in_lbd: builtins.bool | None = ...,
        presolve_bve_threshold: builtins.int | None = ...,
        filter_sat_postsolve_clauses: builtins.bool | None = ...,
        presolve_bve_clause_weight: builtins.int | None = ...,
        probing_deterministic_time_limit: builtins.float | None = ...,
        presolve_probing_deterministic_time_limit: builtins.float | None = ...,
        presolve_blocked_clause: builtins.bool | None = ...,
        presolve_use_bva: builtins.bool | None = ...,
        presolve_bva_threshold: builtins.int | None = ...,
        max_presolve_iterations: builtins.int | None = ...,
        cp_model_presolve: builtins.bool | None = ...,
        cp_model_probing_level: builtins.int | None = ...,
        cp_model_use_sat_presolve: builtins.bool | None = ...,
        load_at_most_ones_in_sat_presolve: builtins.bool | None = ...,
        remove_fixed_variables_early: builtins.bool | None = ...,
        detect_table_with_cost: builtins.bool | None = ...,
        table_compression_level: builtins.int | None = ...,
        expand_alldiff_constraints: builtins.bool | None = ...,
        max_alldiff_domain_size: builtins.int | None = ...,
        expand_reservoir_constraints: builtins.bool | None = ...,
        max_domain_size_for_linear2_expansion: builtins.int | None = ...,
        expand_reservoir_using_circuit: builtins.bool | None = ...,
        encode_cumulative_as_reservoir: builtins.bool | None = ...,
        max_lin_max_size_for_expansion: builtins.int | None = ...,
        disable_constraint_expansion: builtins.bool | None = ...,
        encode_complex_linear_constraint_with_integer: builtins.bool | None = ...,
        merge_no_overlap_work_limit: builtins.float | None = ...,
        merge_at_most_one_work_limit: builtins.float | None = ...,
        presolve_substitution_level: builtins.int | None = ...,
        presolve_extract_integer_enforcement: builtins.bool | None = ...,
        presolve_inclusion_work_limit: builtins.int | None = ...,
        ignore_names: builtins.bool | None = ...,
        infer_all_diffs: builtins.bool | None = ...,
        find_big_linear_overlap: builtins.bool | None = ...,
        find_clauses_that_are_exactly_one: builtins.bool | None = ...,
        use_sat_inprocessing: builtins.bool | None = ...,
        inprocessing_dtime_ratio: builtins.float | None = ...,
        inprocessing_probing_dtime: builtins.float | None = ...,
        inprocessing_minimization_dtime: builtins.float | None = ...,
        inprocessing_minimization_use_conflict_analysis: builtins.bool | None = ...,
        inprocessing_minimization_use_all_orderings: builtins.bool | None = ...,
        inprocessing_use_congruence_closure: builtins.bool | None = ...,
        inprocessing_use_sat_sweeping: builtins.bool | None = ...,
        num_workers: builtins.int | None = ...,
        num_search_workers: builtins.int | None = ...,
        num_full_subsolvers: builtins.int | None = ...,
        subsolvers: collections.abc.Iterable[builtins.str] | None = ...,
        extra_subsolvers: collections.abc.Iterable[builtins.str] | None = ...,
        ignore_subsolvers: collections.abc.Iterable[builtins.str] | None = ...,
        filter_subsolvers: collections.abc.Iterable[builtins.str] | None = ...,
        subsolver_params: collections.abc.Iterable[Global___SatParameters] | None = ...,
        interleave_search: builtins.bool | None = ...,
        interleave_batch_size: builtins.int | None = ...,
        share_objective_bounds: builtins.bool | None = ...,
        share_level_zero_bounds: builtins.bool | None = ...,
        share_linear2_bounds: builtins.bool | None = ...,
        share_binary_clauses: builtins.bool | None = ...,
        share_glue_clauses: builtins.bool | None = ...,
        minimize_shared_clauses: builtins.bool | None = ...,
        share_glue_clauses_dtime: builtins.float | None = ...,
        check_lrat_proof: builtins.bool | None = ...,
        check_merged_lrat_proof: builtins.bool | None = ...,
        output_lrat_proof: builtins.bool | None = ...,
        check_drat_proof: builtins.bool | None = ...,
        output_drat_proof: builtins.bool | None = ...,
        max_drat_time_in_seconds: builtins.float | None = ...,
        debug_postsolve_with_full_solver: builtins.bool | None = ...,
        debug_max_num_presolve_operations: builtins.int | None = ...,
        debug_crash_on_bad_hint: builtins.bool | None = ...,
        debug_crash_if_presolve_breaks_hint: builtins.bool | None = ...,
        debug_crash_if_lrat_check_fails: builtins.bool | None = ...,
        use_optimization_hints: builtins.bool | None = ...,
        core_minimization_level: builtins.int | None = ...,
        find_multiple_cores: builtins.bool | None = ...,
        cover_optimization: builtins.bool | None = ...,
        max_sat_assumption_order: Global___SatParameters.MaxSatAssumptionOrder.ValueType | None = ...,
        max_sat_reverse_assumption_order: builtins.bool | None = ...,
        max_sat_stratification: Global___SatParameters.MaxSatStratificationAlgorithm.ValueType | None = ...,
        propagation_loop_detection_factor: builtins.float | None = ...,
        use_precedences_in_disjunctive_constraint: builtins.bool | None = ...,
        transitive_precedences_work_limit: builtins.int | None = ...,
        max_size_to_create_precedence_literals_in_disjunctive: builtins.int | None = ...,
        use_strong_propagation_in_disjunctive: builtins.bool | None = ...,
        use_dynamic_precedence_in_disjunctive: builtins.bool | None = ...,
        use_dynamic_precedence_in_cumulative: builtins.bool | None = ...,
        use_overload_checker_in_cumulative: builtins.bool | None = ...,
        use_conservative_scale_overload_checker: builtins.bool | None = ...,
        use_timetable_edge_finding_in_cumulative: builtins.bool | None = ...,
        max_num_intervals_for_timetable_edge_finding: builtins.int | None = ...,
        use_hard_precedences_in_cumulative: builtins.bool | None = ...,
        exploit_all_precedences: builtins.bool | None = ...,
        use_disjunctive_constraint_in_cumulative: builtins.bool | None = ...,
        no_overlap_2d_boolean_relations_limit: builtins.int | None = ...,
        use_timetabling_in_no_overlap_2d: builtins.bool | None = ...,
        use_energetic_reasoning_in_no_overlap_2d: builtins.bool | None = ...,
        use_area_energetic_reasoning_in_no_overlap_2d: builtins.bool | None = ...,
        use_try_edge_reasoning_in_no_overlap_2d: builtins.bool | None = ...,
        max_pairs_pairwise_reasoning_in_no_overlap_2d: builtins.int | None = ...,
        maximum_regions_to_split_in_disconnected_no_overlap_2d: builtins.int | None = ...,
        use_linear3_for_no_overlap_2d_precedences: builtins.bool | None = ...,
        use_dual_scheduling_heuristics: builtins.bool | None = ...,
        use_all_different_for_circuit: builtins.bool | None = ...,
        routing_cut_subset_size_for_binary_relation_bound: builtins.int | None = ...,
        routing_cut_subset_size_for_tight_binary_relation_bound: builtins.int | None = ...,
        routing_cut_subset_size_for_exact_binary_relation_bound: builtins.int | None = ...,
        routing_cut_subset_size_for_shortest_paths_bound: builtins.int | None = ...,
        routing_cut_dp_effort: builtins.float | None = ...,
        routing_cut_max_infeasible_path_length: builtins.int | None = ...,
        search_branching: Global___SatParameters.SearchBranching.ValueType | None = ...,
        hint_conflict_limit: builtins.int | None = ...,
        repair_hint: builtins.bool | None = ...,
        fix_variables_to_their_hinted_value: builtins.bool | None = ...,
        use_probing_search: builtins.bool | None = ...,
        use_extended_probing: builtins.bool | None = ...,
        probing_num_combinations_limit: builtins.int | None = ...,
        shaving_deterministic_time_in_probing_search: builtins.float | None = ...,
        shaving_search_deterministic_time: builtins.float | None = ...,
        shaving_search_threshold: builtins.int | None = ...,
        use_objective_lb_search: builtins.bool | None = ...,
        use_objective_shaving_search: builtins.bool | None = ...,
        variables_shaving_level: builtins.int | None = ...,
        pseudo_cost_reliability_threshold: builtins.int | None = ...,
        optimize_with_core: builtins.bool | None = ...,
        optimize_with_lb_tree_search: builtins.bool | None = ...,
        save_lp_basis_in_lb_tree_search: builtins.bool | None = ...,
        binary_search_num_conflicts: builtins.int | None = ...,
        optimize_with_max_hs: builtins.bool | None = ...,
        use_feasibility_jump: builtins.bool | None = ...,
        use_ls_only: builtins.bool | None = ...,
        feasibility_jump_decay: builtins.float | None = ...,
        feasibility_jump_linearization_level: builtins.int | None = ...,
        feasibility_jump_restart_factor: builtins.int | None = ...,
        feasibility_jump_batch_dtime: builtins.float | None = ...,
        feasibility_jump_var_randomization_probability: builtins.float | None = ...,
        feasibility_jump_var_perburbation_range_ratio: builtins.float | None = ...,
        feasibility_jump_enable_restarts: builtins.bool | None = ...,
        feasibility_jump_max_expanded_constraint_size: builtins.int | None = ...,
        num_violation_ls: builtins.int | None = ...,
        violation_ls_perturbation_period: builtins.int | None = ...,
        violation_ls_compound_move_probability: builtins.float | None = ...,
        shared_tree_num_workers: builtins.int | None = ...,
        use_shared_tree_search: builtins.bool | None = ...,
        shared_tree_worker_min_restarts_per_subtree: builtins.int | None = ...,
        shared_tree_worker_enable_trail_sharing: builtins.bool | None = ...,
        shared_tree_worker_enable_phase_sharing: builtins.bool | None = ...,
        shared_tree_open_leaves_per_worker: builtins.float | None = ...,
        shared_tree_max_nodes_per_worker: builtins.int | None = ...,
        shared_tree_split_strategy: Global___SatParameters.SharedTreeSplitStrategy.ValueType | None = ...,
        shared_tree_balance_tolerance: builtins.int | None = ...,
        shared_tree_split_min_dtime: builtins.float | None = ...,
        enumerate_all_solutions: builtins.bool | None = ...,
        keep_all_feasible_solutions_in_presolve: builtins.bool | None = ...,
        fill_tightened_domains_in_response: builtins.bool | None = ...,
        fill_additional_solutions_in_response: builtins.bool | None = ...,
        instantiate_all_variables: builtins.bool | None = ...,
        auto_detect_greater_than_at_least_one_of: builtins.bool | None = ...,
        stop_after_first_solution: builtins.bool | None = ...,
        stop_after_presolve: builtins.bool | None = ...,
        stop_after_root_propagation: builtins.bool | None = ...,
        lns_initial_difficulty: builtins.float | None = ...,
        lns_initial_deterministic_limit: builtins.float | None = ...,
        use_lns: builtins.bool | None = ...,
        use_lns_only: builtins.bool | None = ...,
        solution_pool_size: builtins.int | None = ...,
        solution_pool_diversity_limit: builtins.int | None = ...,
        alternative_pool_size: builtins.int | None = ...,
        use_rins_lns: builtins.bool | None = ...,
        use_feasibility_pump: builtins.bool | None = ...,
        use_lb_relax_lns: builtins.bool | None = ...,
        lb_relax_num_workers_threshold: builtins.int | None = ...,
        fp_rounding: Global___SatParameters.FPRoundingMethod.ValueType | None = ...,
        diversify_lns_params: builtins.bool | None = ...,
        randomize_search: builtins.bool | None = ...,
        search_random_variable_pool_size: builtins.int | None = ...,
        push_all_tasks_toward_start: builtins.bool | None = ...,
        use_optional_variables: builtins.bool | None = ...,
        use_exact_lp_reason: builtins.bool | None = ...,
        use_combined_no_overlap: builtins.bool | None = ...,
        at_most_one_max_expansion_size: builtins.int | None = ...,
        catch_sigint_signal: builtins.bool | None = ...,
        use_implied_bounds: builtins.bool | None = ...,
        polish_lp_solution: builtins.bool | None = ...,
        lp_primal_tolerance: builtins.float | None = ...,
        lp_dual_tolerance: builtins.float | None = ...,
        convert_intervals: builtins.bool | None = ...,
        symmetry_level: builtins.int | None = ...,
        use_symmetry_in_lp: builtins.bool | None = ...,
        keep_symmetry_in_presolve: builtins.bool | None = ...,
        symmetry_detection_deterministic_time_limit: builtins.float | None = ...,
        new_linear_propagation: builtins.bool | None = ...,
        linear_split_size: builtins.int | None = ...,
        linearization_level: builtins.int | None = ...,
        boolean_encoding_level: builtins.int | None = ...,
        max_domain_size_when_encoding_eq_neq_constraints: builtins.int | None = ...,
        max_num_cuts: builtins.int | None = ...,
        cut_level: builtins.int | None = ...,
        only_add_cuts_at_level_zero: builtins.bool | None = ...,
        add_objective_cut: builtins.bool | None = ...,
        add_cg_cuts: builtins.bool | None = ...,
        add_mir_cuts: builtins.bool | None = ...,
        add_zero_half_cuts: builtins.bool | None = ...,
        add_clique_cuts: builtins.bool | None = ...,
        add_rlt_cuts: builtins.bool | None = ...,
        max_all_diff_cut_size: builtins.int | None = ...,
        add_lin_max_cuts: builtins.bool | None = ...,
        max_integer_rounding_scaling: builtins.int | None = ...,
        add_lp_constraints_lazily: builtins.bool | None = ...,
        root_lp_iterations: builtins.int | None = ...,
        min_orthogonality_for_lp_constraints: builtins.float | None = ...,
        max_cut_rounds_at_level_zero: builtins.int | None = ...,
        max_consecutive_inactive_count: builtins.int | None = ...,
        cut_max_active_count_value: builtins.float | None = ...,
        cut_active_count_decay: builtins.float | None = ...,
        cut_cleanup_target: builtins.int | None = ...,
        new_constraints_batch_size: builtins.int | None = ...,
        exploit_integer_lp_solution: builtins.bool | None = ...,
        exploit_all_lp_solution: builtins.bool | None = ...,
        exploit_best_solution: builtins.bool | None = ...,
        exploit_relaxation_solution: builtins.bool | None = ...,
        exploit_objective: builtins.bool | None = ...,
        detect_linearized_product: builtins.bool | None = ...,
        use_new_integer_conflict_resolution: builtins.bool | None = ...,
        create_1uip_boolean_during_icr: builtins.bool | None = ...,
        mip_max_bound: builtins.float | None = ...,
        mip_var_scaling: builtins.float | None = ...,
        mip_scale_large_domain: builtins.bool | None = ...,
        mip_automatically_scale_variables: builtins.bool | None = ...,
        only_solve_ip: builtins.bool | None = ...,
        mip_wanted_precision: builtins.float | None = ...,
        mip_max_activity_exponent: builtins.int | None = ...,
        mip_check_precision: builtins.float | None = ...,
        mip_compute_true_objective_bound: builtins.bool | None = ...,
        mip_max_valid_magnitude: builtins.float | None = ...,
        mip_treat_high_magnitude_bounds_as_infinity: builtins.bool | None = ...,
        mip_drop_tolerance: builtins.float | None = ...,
        mip_presolve_level: builtins.int | None = ...,
    ) -> None: ...
    _HasFieldArgType: typing_extensions.TypeAlias = typing.Literal["absolute_gap_limit", b"absolute_gap_limit", "add_cg_cuts", b"add_cg_cuts", "add_clique_cuts", b"add_clique_cuts", "add_lin_max_cuts", b"add_lin_max_cuts", "add_lp_constraints_lazily", b"add_lp_constraints_lazily", "add_mir_cuts", b"add_mir_cuts", "add_objective_cut", b"add_objective_cut", "add_rlt_cuts", b"add_rlt_cuts", "add_zero_half_cuts", b"add_zero_half_cuts", "also_bump_variables_in_conflict_reasons", b"also_bump_variables_in_conflict_reasons", "alternative_pool_size", b"alternative_pool_size", "at_most_one_max_expansion_size", b"at_most_one_max_expansion_size", "auto_detect_greater_than_at_least_one_of", b"auto_detect_greater_than_at_least_one_of", "binary_minimization_algorithm", b"binary_minimization_algorithm", "binary_search_num_conflicts", b"binary_search_num_conflicts", "blocking_restart_multiplier", b"blocking_restart_multiplier", "blocking_restart_window_size", b"blocking_restart_window_size", "boolean_encoding_level", b"boolean_encoding_level", "catch_sigint_signal", b"catch_sigint_signal", "check_drat_proof", b"check_drat_proof", "check_lrat_proof", b"check_lrat_proof", "check_merged_lrat_proof", b"check_merged_lrat_proof", "chronological_backtrack_min_conflicts", b"chronological_backtrack_min_conflicts", "clause_activity_decay", b"clause_activity_decay", "clause_cleanup_lbd_bound", b"clause_cleanup_lbd_bound", "clause_cleanup_lbd_tier1", b"clause_cleanup_lbd_tier1", "clause_cleanup_lbd_tier2", b"clause_cleanup_lbd_tier2", "clause_cleanup_ordering", b"clause_cleanup_ordering", "clause_cleanup_period", b"clause_cleanup_period", "clause_cleanup_period_increment", b"clause_cleanup_period_increment", "clause_cleanup_ratio", b"clause_cleanup_ratio", "clause_cleanup_target", b"clause_cleanup_target", "convert_intervals", b"convert_intervals", "core_minimization_level", b"core_minimization_level", "count_assumption_levels_in_lbd", b"count_assumption_levels_in_lbd", "cover_optimization", b"cover_optimization", "cp_model_presolve", b"cp_model_presolve", "cp_model_probing_level", b"cp_model_probing_level", "cp_model_use_sat_presolve", b"cp_model_use_sat_presolve", "create_1uip_boolean_during_icr", b"create_1uip_boolean_during_icr", "cut_active_count_decay", b"cut_active_count_decay", "cut_cleanup_target", b"cut_cleanup_target", "cut_level", b"cut_level", "cut_max_active_count_value", b"cut_max_active_count_value", "debug_crash_if_lrat_check_fails", b"debug_crash_if_lrat_check_fails", "debug_crash_if_presolve_breaks_hint", b"debug_crash_if_presolve_breaks_hint", "debug_crash_on_bad_hint", b"debug_crash_on_bad_hint", "debug_max_num_presolve_operations", b"debug_max_num_presolve_operations", "debug_postsolve_with_full_solver", b"debug_postsolve_with_full_solver", "decision_subsumption_during_conflict_analysis", b"decision_subsumption_during_conflict_analysis", "default_restart_algorithms", b"default_restart_algorithms", "detect_linearized_product", b"detect_linearized_product", "detect_table_with_cost", b"detect_table_with_cost", "disable_constraint_expansion", b"disable_constraint_expansion", "diversify_lns_params", b"diversify_lns_params", "eagerly_subsume_last_n_conflicts", b"eagerly_subsume_last_n_conflicts", "encode_complex_linear_constraint_with_integer", b"encode_complex_linear_constraint_with_integer", "encode_cumulative_as_reservoir", b"encode_cumulative_as_reservoir", "enumerate_all_solutions", b"enumerate_all_solutions", "expand_alldiff_constraints", b"expand_alldiff_constraints", "expand_reservoir_constraints", b"expand_reservoir_constraints", "expand_reservoir_using_circuit", b"expand_reservoir_using_circuit", "exploit_all_lp_solution", b"exploit_all_lp_solution", "exploit_all_precedences", b"exploit_all_precedences", "exploit_best_solution", b"exploit_best_solution", "exploit_integer_lp_solution", b"exploit_integer_lp_solution", "exploit_objective", b"exploit_objective", "exploit_relaxation_solution", b"exploit_relaxation_solution", "extra_subsumption_during_conflict_analysis", b"extra_subsumption_during_conflict_analysis", "feasibility_jump_batch_dtime", b"feasibility_jump_batch_dtime", "feasibility_jump_decay", b"feasibility_jump_decay", "feasibility_jump_enable_restarts", b"feasibility_jump_enable_restarts", "feasibility_jump_linearization_level", b"feasibility_jump_linearization_level", "feasibility_jump_max_expanded_constraint_size", b"feasibility_jump_max_expanded_constraint_size", "feasibility_jump_restart_factor", b"feasibility_jump_restart_factor", "feasibility_jump_var_perburbation_range_ratio", b"feasibility_jump_var_perburbation_range_ratio", "feasibility_jump_var_randomization_probability", b"feasibility_jump_var_randomization_probability", "fill_additional_solutions_in_response", b"fill_additional_solutions_in_response", "fill_tightened_domains_in_response", b"fill_tightened_domains_in_response", "filter_sat_postsolve_clauses", b"filter_sat_postsolve_clauses", "find_big_linear_overlap", b"find_big_linear_overlap", "find_clauses_that_are_exactly_one", b"find_clauses_that_are_exactly_one", "find_multiple_cores", b"find_multiple_cores", "fix_variables_to_their_hinted_value", b"fix_variables_to_their_hinted_value", "fp_rounding", b"fp_rounding", "glucose_decay_increment", b"glucose_decay_increment", "glucose_decay_increment_period", b"glucose_decay_increment_period", "glucose_max_decay", b"glucose_max_decay", "hint_conflict_limit", b"hint_conflict_limit", "ignore_names", b"ignore_names", "infer_all_diffs", b"infer_all_diffs", "initial_polarity", b"initial_polarity", "initial_variables_activity", b"initial_variables_activity", "inprocessing_dtime_ratio", b"inprocessing_dtime_ratio", "inprocessing_minimization_dtime", b"inprocessing_minimization_dtime", "inprocessing_minimization_use_all_orderings", b"inprocessing_minimization_use_all_orderings", "inprocessing_minimization_use_conflict_analysis", b"inprocessing_minimization_use_conflict_analysis", "inprocessing_probing_dtime", b"inprocessing_probing_dtime", "inprocessing_use_congruence_closure", b"inprocessing_use_congruence_closure", "inprocessing_use_sat_sweeping", b"inprocessing_use_sat_sweeping", "instantiate_all_variables", b"instantiate_all_variables", "interleave_batch_size", b"interleave_batch_size", "interleave_search", b"interleave_search", "keep_all_feasible_solutions_in_presolve", b"keep_all_feasible_solutions_in_presolve", "keep_symmetry_in_presolve", b"keep_symmetry_in_presolve", "lb_relax_num_workers_threshold", b"lb_relax_num_workers_threshold", "linear_split_size", b"linear_split_size", "linearization_level", b"linearization_level", "lns_initial_deterministic_limit", b"lns_initial_deterministic_limit", "lns_initial_difficulty", b"lns_initial_difficulty", "load_at_most_ones_in_sat_presolve", b"load_at_most_ones_in_sat_presolve", "log_prefix", b"log_prefix", "log_search_progress", b"log_search_progress", "log_subsolver_statistics", b"log_subsolver_statistics", "log_to_response", b"log_to_response", "log_to_stdout", b"log_to_stdout", "lp_dual_tolerance", b"lp_dual_tolerance", "lp_primal_tolerance", b"lp_primal_tolerance", "max_all_diff_cut_size", b"max_all_diff_cut_size", "max_alldiff_domain_size", b"max_alldiff_domain_size", "max_backjump_levels", b"max_backjump_levels", "max_clause_activity_value", b"max_clause_activity_value", "max_consecutive_inactive_count", b"max_consecutive_inactive_count", "max_cut_rounds_at_level_zero", b"max_cut_rounds_at_level_zero", "max_deterministic_time", b"max_deterministic_time", "max_domain_size_for_linear2_expansion", b"max_domain_size_for_linear2_expansion", "max_domain_size_when_encoding_eq_neq_constraints", b"max_domain_size_when_encoding_eq_neq_constraints", "max_drat_time_in_seconds", b"max_drat_time_in_seconds", "max_integer_rounding_scaling", b"max_integer_rounding_scaling", "max_lin_max_size_for_expansion", b"max_lin_max_size_for_expansion", "max_memory_in_mb", b"max_memory_in_mb", "max_num_cuts", b"max_num_cuts", "max_num_deterministic_batches", b"max_num_deterministic_batches", "max_num_intervals_for_timetable_edge_finding", b"max_num_intervals_for_timetable_edge_finding", "max_number_of_conflicts", b"max_number_of_conflicts", "max_pairs_pairwise_reasoning_in_no_overlap_2d", b"max_pairs_pairwise_reasoning_in_no_overlap_2d", "max_presolve_iterations", b"max_presolve_iterations", "max_sat_assumption_order", b"max_sat_assumption_order", "max_sat_reverse_assumption_order", b"max_sat_reverse_assumption_order", "max_sat_stratification", b"max_sat_stratification", "max_size_to_create_precedence_literals_in_disjunctive", b"max_size_to_create_precedence_literals_in_disjunctive", "max_time_in_seconds", b"max_time_in_seconds", "max_variable_activity_value", b"max_variable_activity_value", "maximum_regions_to_split_in_disconnected_no_overlap_2d", b"maximum_regions_to_split_in_disconnected_no_overlap_2d", "merge_at_most_one_work_limit", b"merge_at_most_one_work_limit", "merge_no_overlap_work_limit", b"merge_no_overlap_work_limit", "min_orthogonality_for_lp_constraints", b"min_orthogonality_for_lp_constraints", "minimization_algorithm", b"minimization_algorithm", "minimize_reduction_during_pb_resolution", b"minimize_reduction_during_pb_resolution", "minimize_shared_clauses", b"minimize_shared_clauses", "mip_automatically_scale_variables", b"mip_automatically_scale_variables", "mip_check_precision", b"mip_check_precision", "mip_compute_true_objective_bound", b"mip_compute_true_objective_bound", "mip_drop_tolerance", b"mip_drop_tolerance", "mip_max_activity_exponent", b"mip_max_activity_exponent", "mip_max_bound", b"mip_max_bound", "mip_max_valid_magnitude", b"mip_max_valid_magnitude", "mip_presolve_level", b"mip_presolve_level", "mip_scale_large_domain", b"mip_scale_large_domain", "mip_treat_high_magnitude_bounds_as_infinity", b"mip_treat_high_magnitude_bounds_as_infinity", "mip_var_scaling", b"mip_var_scaling", "mip_wanted_precision", b"mip_wanted_precision", "name", b"name", "new_constraints_batch_size", b"new_constraints_batch_size", "new_linear_propagation", b"new_linear_propagation", "no_overlap_2d_boolean_relations_limit", b"no_overlap_2d_boolean_relations_limit", "num_conflicts_before_strategy_changes", b"num_conflicts_before_strategy_changes", "num_full_subsolvers", b"num_full_subsolvers", "num_search_workers", b"num_search_workers", "num_violation_ls", b"num_violation_ls", "num_workers", b"num_workers", "only_add_cuts_at_level_zero", b"only_add_cuts_at_level_zero", "only_solve_ip", b"only_solve_ip", "optimize_with_core", b"optimize_with_core", "optimize_with_lb_tree_search", b"optimize_with_lb_tree_search", "optimize_with_max_hs", b"optimize_with_max_hs", "output_drat_proof", b"output_drat_proof", "output_lrat_proof", b"output_lrat_proof", "pb_cleanup_increment", b"pb_cleanup_increment", "pb_cleanup_ratio", b"pb_cleanup_ratio", "permute_presolve_constraint_order", b"permute_presolve_constraint_order", "permute_variable_randomly", b"permute_variable_randomly", "polarity_exploit_ls_hints", b"polarity_exploit_ls_hints", "polarity_rephase_increment", b"polarity_rephase_increment", "polish_lp_solution", b"polish_lp_solution", "preferred_variable_order", b"preferred_variable_order", "presolve_blocked_clause", b"presolve_blocked_clause", "presolve_bva_threshold", b"presolve_bva_threshold", "presolve_bve_clause_weight", b"presolve_bve_clause_weight", "presolve_bve_threshold", b"presolve_bve_threshold", "presolve_extract_integer_enforcement", b"presolve_extract_integer_enforcement", "presolve_inclusion_work_limit", b"presolve_inclusion_work_limit", "presolve_probing_deterministic_time_limit", b"presolve_probing_deterministic_time_limit", "presolve_substitution_level", b"presolve_substitution_level", "presolve_use_bva", b"presolve_use_bva", "probing_deterministic_time_limit", b"probing_deterministic_time_limit", "probing_num_combinations_limit", b"probing_num_combinations_limit", "propagation_loop_detection_factor", b"propagation_loop_detection_factor", "pseudo_cost_reliability_threshold", b"pseudo_cost_reliability_threshold", "push_all_tasks_toward_start", b"push_all_tasks_toward_start", "random_branches_ratio", b"random_branches_ratio", "random_polarity_ratio", b"random_polarity_ratio", "random_seed", b"random_seed", "randomize_search", b"randomize_search", "relative_gap_limit", b"relative_gap_limit", "remove_fixed_variables_early", b"remove_fixed_variables_early", "repair_hint", b"repair_hint", "restart_dl_average_ratio", b"restart_dl_average_ratio", "restart_lbd_average_ratio", b"restart_lbd_average_ratio", "restart_period", b"restart_period", "restart_running_window_size", b"restart_running_window_size", "root_lp_iterations", b"root_lp_iterations", "routing_cut_dp_effort", b"routing_cut_dp_effort", "routing_cut_max_infeasible_path_length", b"routing_cut_max_infeasible_path_length", "routing_cut_subset_size_for_binary_relation_bound", b"routing_cut_subset_size_for_binary_relation_bound", "routing_cut_subset_size_for_exact_binary_relation_bound", b"routing_cut_subset_size_for_exact_binary_relation_bound", "routing_cut_subset_size_for_shortest_paths_bound", b"routing_cut_subset_size_for_shortest_paths_bound", "routing_cut_subset_size_for_tight_binary_relation_bound", b"routing_cut_subset_size_for_tight_binary_relation_bound", "save_lp_basis_in_lb_tree_search", b"save_lp_basis_in_lb_tree_search", "search_branching", b"search_branching", "search_random_variable_pool_size", b"search_random_variable_pool_size", "share_binary_clauses", b"share_binary_clauses", "share_glue_clauses", b"share_glue_clauses", "share_glue_clauses_dtime", b"share_glue_clauses_dtime", "share_level_zero_bounds", b"share_level_zero_bounds", "share_linear2_bounds", b"share_linear2_bounds", "share_objective_bounds", b"share_objective_bounds", "shared_tree_balance_tolerance", b"shared_tree_balance_tolerance", "shared_tree_max_nodes_per_worker", b"shared_tree_max_nodes_per_worker", "shared_tree_num_workers", b"shared_tree_num_workers", "shared_tree_open_leaves_per_worker", b"shared_tree_open_leaves_per_worker", "shared_tree_split_min_dtime", b"shared_tree_split_min_dtime", "shared_tree_split_strategy", b"shared_tree_split_strategy", "shared_tree_worker_enable_phase_sharing", b"shared_tree_worker_enable_phase_sharing", "shared_tree_worker_enable_trail_sharing", b"shared_tree_worker_enable_trail_sharing", "shared_tree_worker_min_restarts_per_subtree", b"shared_tree_worker_min_restarts_per_subtree", "shaving_deterministic_time_in_probing_search", b"shaving_deterministic_time_in_probing_search", "shaving_search_deterministic_time", b"shaving_search_deterministic_time", "shaving_search_threshold", b"shaving_search_threshold", "solution_pool_diversity_limit", b"solution_pool_diversity_limit", "solution_pool_size", b"solution_pool_size", "stop_after_first_solution", b"stop_after_first_solution", "stop_after_presolve", b"stop_after_presolve", "stop_after_root_propagation", b"stop_after_root_propagation", "strategy_change_increase_ratio", b"strategy_change_increase_ratio", "subsume_during_vivification", b"subsume_during_vivification", "subsumption_during_conflict_analysis", b"subsumption_during_conflict_analysis", "symmetry_detection_deterministic_time_limit", b"symmetry_detection_deterministic_time_limit", "symmetry_level", b"symmetry_level", "table_compression_level", b"table_compression_level", "transitive_precedences_work_limit", b"transitive_precedences_work_limit", "use_absl_random", b"use_absl_random", "use_all_different_for_circuit", b"use_all_different_for_circuit", "use_area_energetic_reasoning_in_no_overlap_2d", b"use_area_energetic_reasoning_in_no_overlap_2d", "use_blocking_restart", b"use_blocking_restart", "use_chronological_backtracking", b"use_chronological_backtracking", "use_combined_no_overlap", b"use_combined_no_overlap", "use_conservative_scale_overload_checker", b"use_conservative_scale_overload_checker", "use_disjunctive_constraint_in_cumulative", b"use_disjunctive_constraint_in_cumulative", "use_dual_scheduling_heuristics", b"use_dual_scheduling_heuristics", "use_dynamic_precedence_in_cumulative", b"use_dynamic_precedence_in_cumulative", "use_dynamic_precedence_in_disjunctive", b"use_dynamic_precedence_in_disjunctive", "use_energetic_reasoning_in_no_overlap_2d", b"use_energetic_reasoning_in_no_overlap_2d", "use_erwa_heuristic", b"use_erwa_heuristic", "use_exact_lp_reason", b"use_exact_lp_reason", "use_extended_probing", b"use_extended_probing", "use_feasibility_jump", b"use_feasibility_jump", "use_feasibility_pump", b"use_feasibility_pump", "use_hard_precedences_in_cumulative", b"use_hard_precedences_in_cumulative", "use_implied_bounds", b"use_implied_bounds", "use_lb_relax_lns", b"use_lb_relax_lns", "use_linear3_for_no_overlap_2d_precedences", b"use_linear3_for_no_overlap_2d_precedences", "use_lns", b"use_lns", "use_lns_only", b"use_lns_only", "use_ls_only", b"use_ls_only", "use_new_integer_conflict_resolution", b"use_new_integer_conflict_resolution", "use_objective_lb_search", b"use_objective_lb_search", "use_objective_shaving_search", b"use_objective_shaving_search", "use_optimization_hints", b"use_optimization_hints", "use_optional_variables", b"use_optional_variables", "use_overload_checker_in_cumulative", b"use_overload_checker_in_cumulative", "use_pb_resolution", b"use_pb_resolution", "use_phase_saving", b"use_phase_saving", "use_precedences_in_disjunctive_constraint", b"use_precedences_in_disjunctive_constraint", "use_probing_search", b"use_probing_search", "use_rins_lns", b"use_rins_lns", "use_sat_inprocessing", b"use_sat_inprocessing", "use_shared_tree_search", b"use_shared_tree_search", "use_strong_propagation_in_disjunctive", b"use_strong_propagation_in_disjunctive", "use_symmetry_in_lp", b"use_symmetry_in_lp", "use_timetable_edge_finding_in_cumulative", b"use_timetable_edge_finding_in_cumulative", "use_timetabling_in_no_overlap_2d", b"use_timetabling_in_no_overlap_2d", "use_try_edge_reasoning_in_no_overlap_2d", b"use_try_edge_reasoning_in_no_overlap_2d", "variable_activity_decay", b"variable_activity_decay", "variables_shaving_level", b"variables_shaving_level", "violation_ls_compound_move_probability", b"violation_ls_compound_move_probability", "violation_ls_perturbation_period", b"violation_ls_perturbation_period"]
    def HasField(self, field_name: _HasFieldArgType) -> builtins.bool: ...
    _ClearFieldArgType: typing_extensions.TypeAlias = typing.Literal["absolute_gap_limit", b"absolute_gap_limit", "add_cg_cuts", b"add_cg_cuts", "add_clique_cuts", b"add_clique_cuts", "add_lin_max_cuts", b"add_lin_max_cuts", "add_lp_constraints_lazily", b"add_lp_constraints_lazily", "add_mir_cuts", b"add_mir_cuts", "add_objective_cut", b"add_objective_cut", "add_rlt_cuts", b"add_rlt_cuts", "add_zero_half_cuts", b"add_zero_half_cuts", "also_bump_variables_in_conflict_reasons", b"also_bump_variables_in_conflict_reasons", "alternative_pool_size", b"alternative_pool_size", "at_most_one_max_expansion_size", b"at_most_one_max_expansion_size", "auto_detect_greater_than_at_least_one_of", b"auto_detect_greater_than_at_least_one_of", "binary_minimization_algorithm", b"binary_minimization_algorithm", "binary_search_num_conflicts", b"binary_search_num_conflicts", "blocking_restart_multiplier", b"blocking_restart_multiplier", "blocking_restart_window_size", b"blocking_restart_window_size", "boolean_encoding_level", b"boolean_encoding_level", "catch_sigint_signal", b"catch_sigint_signal", "check_drat_proof", b"check_drat_proof", "check_lrat_proof", b"check_lrat_proof", "check_merged_lrat_proof", b"check_merged_lrat_proof", "chronological_backtrack_min_conflicts", b"chronological_backtrack_min_conflicts", "clause_activity_decay", b"clause_activity_decay", "clause_cleanup_lbd_bound", b"clause_cleanup_lbd_bound", "clause_cleanup_lbd_tier1", b"clause_cleanup_lbd_tier1", "clause_cleanup_lbd_tier2", b"clause_cleanup_lbd_tier2", "clause_cleanup_ordering", b"clause_cleanup_ordering", "clause_cleanup_period", b"clause_cleanup_period", "clause_cleanup_period_increment", b"clause_cleanup_period_increment", "clause_cleanup_ratio", b"clause_cleanup_ratio", "clause_cleanup_target", b"clause_cleanup_target", "convert_intervals", b"convert_intervals", "core_minimization_level", b"core_minimization_level", "count_assumption_levels_in_lbd", b"count_assumption_levels_in_lbd", "cover_optimization", b"cover_optimization", "cp_model_presolve", b"cp_model_presolve", "cp_model_probing_level", b"cp_model_probing_level", "cp_model_use_sat_presolve", b"cp_model_use_sat_presolve", "create_1uip_boolean_during_icr", b"create_1uip_boolean_during_icr", "cut_active_count_decay", b"cut_active_count_decay", "cut_cleanup_target", b"cut_cleanup_target", "cut_level", b"cut_level", "cut_max_active_count_value", b"cut_max_active_count_value", "debug_crash_if_lrat_check_fails", b"debug_crash_if_lrat_check_fails", "debug_crash_if_presolve_breaks_hint", b"debug_crash_if_presolve_breaks_hint", "debug_crash_on_bad_hint", b"debug_crash_on_bad_hint", "debug_max_num_presolve_operations", b"debug_max_num_presolve_operations", "debug_postsolve_with_full_solver", b"debug_postsolve_with_full_solver", "decision_subsumption_during_conflict_analysis", b"decision_subsumption_during_conflict_analysis", "default_restart_algorithms", b"default_restart_algorithms", "detect_linearized_product", b"detect_linearized_product", "detect_table_with_cost", b"detect_table_with_cost", "disable_constraint_expansion", b"disable_constraint_expansion", "diversify_lns_params", b"diversify_lns_params", "eagerly_subsume_last_n_conflicts", b"eagerly_subsume_last_n_conflicts", "encode_complex_linear_constraint_with_integer", b"encode_complex_linear_constraint_with_integer", "encode_cumulative_as_reservoir", b"encode_cumulative_as_reservoir", "enumerate_all_solutions", b"enumerate_all_solutions", "expand_alldiff_constraints", b"expand_alldiff_constraints", "expand_reservoir_constraints", b"expand_reservoir_constraints", "expand_reservoir_using_circuit", b"expand_reservoir_using_circuit", "exploit_all_lp_solution", b"exploit_all_lp_solution", "exploit_all_precedences", b"exploit_all_precedences", "exploit_best_solution", b"exploit_best_solution", "exploit_integer_lp_solution", b"exploit_integer_lp_solution", "exploit_objective", b"exploit_objective", "exploit_relaxation_solution", b"exploit_relaxation_solution", "extra_subsolvers", b"extra_subsolvers", "extra_subsumption_during_conflict_analysis", b"extra_subsumption_during_conflict_analysis", "feasibility_jump_batch_dtime", b"feasibility_jump_batch_dtime", "feasibility_jump_decay", b"feasibility_jump_decay", "feasibility_jump_enable_restarts", b"feasibility_jump_enable_restarts", "feasibility_jump_linearization_level", b"feasibility_jump_linearization_level", "feasibility_jump_max_expanded_constraint_size", b"feasibility_jump_max_expanded_constraint_size", "feasibility_jump_restart_factor", b"feasibility_jump_restart_factor", "feasibility_jump_var_perburbation_range_ratio", b"feasibility_jump_var_perburbation_range_ratio", "feasibility_jump_var_randomization_probability", b"feasibility_jump_var_randomization_probability", "fill_additional_solutions_in_response", b"fill_additional_solutions_in_response", "fill_tightened_domains_in_response", b"fill_tightened_domains_in_response", "filter_sat_postsolve_clauses", b"filter_sat_postsolve_clauses", "filter_subsolvers", b"filter_subsolvers", "find_big_linear_overlap", b"find_big_linear_overlap", "find_clauses_that_are_exactly_one", b"find_clauses_that_are_exactly_one", "find_multiple_cores", b"find_multiple_cores", "fix_variables_to_their_hinted_value", b"fix_variables_to_their_hinted_value", "fp_rounding", b"fp_rounding", "glucose_decay_increment", b"glucose_decay_increment", "glucose_decay_increment_period", b"glucose_decay_increment_period", "glucose_max_decay", b"glucose_max_decay", "hint_conflict_limit", b"hint_conflict_limit", "ignore_names", b"ignore_names", "ignore_subsolvers", b"ignore_subsolvers", "infer_all_diffs", b"infer_all_diffs", "initial_polarity", b"initial_polarity", "initial_variables_activity", b"initial_variables_activity", "inprocessing_dtime_ratio", b"inprocessing_dtime_ratio", "inprocessing_minimization_dtime", b"inprocessing_minimization_dtime", "inprocessing_minimization_use_all_orderings", b"inprocessing_minimization_use_all_orderings", "inprocessing_minimization_use_conflict_analysis", b"inprocessing_minimization_use_conflict_analysis", "inprocessing_probing_dtime", b"inprocessing_probing_dtime", "inprocessing_use_congruence_closure", b"inprocessing_use_congruence_closure", "inprocessing_use_sat_sweeping", b"inprocessing_use_sat_sweeping", "instantiate_all_variables", b"instantiate_all_variables", "interleave_batch_size", b"interleave_batch_size", "interleave_search", b"interleave_search", "keep_all_feasible_solutions_in_presolve", b"keep_all_feasible_solutions_in_presolve", "keep_symmetry_in_presolve", b"keep_symmetry_in_presolve", "lb_relax_num_workers_threshold", b"lb_relax_num_workers_threshold", "linear_split_size", b"linear_split_size", "linearization_level", b"linearization_level", "lns_initial_deterministic_limit", b"lns_initial_deterministic_limit", "lns_initial_difficulty", b"lns_initial_difficulty", "load_at_most_ones_in_sat_presolve", b"load_at_most_ones_in_sat_presolve", "log_prefix", b"log_prefix", "log_search_progress", b"log_search_progress", "log_subsolver_statistics", b"log_subsolver_statistics", "log_to_response", b"log_to_response", "log_to_stdout", b"log_to_stdout", "lp_dual_tolerance", b"lp_dual_tolerance", "lp_primal_tolerance", b"lp_primal_tolerance", "max_all_diff_cut_size", b"max_all_diff_cut_size", "max_alldiff_domain_size", b"max_alldiff_domain_size", "max_backjump_levels", b"max_backjump_levels", "max_clause_activity_value", b"max_clause_activity_value", "max_consecutive_inactive_count", b"max_consecutive_inactive_count", "max_cut_rounds_at_level_zero", b"max_cut_rounds_at_level_zero", "max_deterministic_time", b"max_deterministic_time", "max_domain_size_for_linear2_expansion", b"max_domain_size_for_linear2_expansion", "max_domain_size_when_encoding_eq_neq_constraints", b"max_domain_size_when_encoding_eq_neq_constraints", "max_drat_time_in_seconds", b"max_drat_time_in_seconds", "max_integer_rounding_scaling", b"max_integer_rounding_scaling", "max_lin_max_size_for_expansion", b"max_lin_max_size_for_expansion", "max_memory_in_mb", b"max_memory_in_mb", "max_num_cuts", b"max_num_cuts", "max_num_deterministic_batches", b"max_num_deterministic_batches", "max_num_intervals_for_timetable_edge_finding", b"max_num_intervals_for_timetable_edge_finding", "max_number_of_conflicts", b"max_number_of_conflicts", "max_pairs_pairwise_reasoning_in_no_overlap_2d", b"max_pairs_pairwise_reasoning_in_no_overlap_2d", "max_presolve_iterations", b"max_presolve_iterations", "max_sat_assumption_order", b"max_sat_assumption_order", "max_sat_reverse_assumption_order", b"max_sat_reverse_assumption_order", "max_sat_stratification", b"max_sat_stratification", "max_size_to_create_precedence_literals_in_disjunctive", b"max_size_to_create_precedence_literals_in_disjunctive", "max_time_in_seconds", b"max_time_in_seconds", "max_variable_activity_value", b"max_variable_activity_value", "maximum_regions_to_split_in_disconnected_no_overlap_2d", b"maximum_regions_to_split_in_disconnected_no_overlap_2d", "merge_at_most_one_work_limit", b"merge_at_most_one_work_limit", "merge_no_overlap_work_limit", b"merge_no_overlap_work_limit", "min_orthogonality_for_lp_constraints", b"min_orthogonality_for_lp_constraints", "minimization_algorithm", b"minimization_algorithm", "minimize_reduction_during_pb_resolution", b"minimize_reduction_during_pb_resolution", "minimize_shared_clauses", b"minimize_shared_clauses", "mip_automatically_scale_variables", b"mip_automatically_scale_variables", "mip_check_precision", b"mip_check_precision", "mip_compute_true_objective_bound", b"mip_compute_true_objective_bound", "mip_drop_tolerance", b"mip_drop_tolerance", "mip_max_activity_exponent", b"mip_max_activity_exponent", "mip_max_bound", b"mip_max_bound", "mip_max_valid_magnitude", b"mip_max_valid_magnitude", "mip_presolve_level", b"mip_presolve_level", "mip_scale_large_domain", b"mip_scale_large_domain", "mip_treat_high_magnitude_bounds_as_infinity", b"mip_treat_high_magnitude_bounds_as_infinity", "mip_var_scaling", b"mip_var_scaling", "mip_wanted_precision", b"mip_wanted_precision", "name", b"name", "new_constraints_batch_size", b"new_constraints_batch_size", "new_linear_propagation", b"new_linear_propagation", "no_overlap_2d_boolean_relations_limit", b"no_overlap_2d_boolean_relations_limit", "num_conflicts_before_strategy_changes", b"num_conflicts_before_strategy_changes", "num_full_subsolvers", b"num_full_subsolvers", "num_search_workers", b"num_search_workers", "num_violation_ls", b"num_violation_ls", "num_workers", b"num_workers", "only_add_cuts_at_level_zero", b"only_add_cuts_at_level_zero", "only_solve_ip", b"only_solve_ip", "optimize_with_core", b"optimize_with_core", "optimize_with_lb_tree_search", b"optimize_with_lb_tree_search", "optimize_with_max_hs", b"optimize_with_max_hs", "output_drat_proof", b"output_drat_proof", "output_lrat_proof", b"output_lrat_proof", "pb_cleanup_increment", b"pb_cleanup_increment", "pb_cleanup_ratio", b"pb_cleanup_ratio", "permute_presolve_constraint_order", b"permute_presolve_constraint_order", "permute_variable_randomly", b"permute_variable_randomly", "polarity_exploit_ls_hints", b"polarity_exploit_ls_hints", "polarity_rephase_increment", b"polarity_rephase_increment", "polish_lp_solution", b"polish_lp_solution", "preferred_variable_order", b"preferred_variable_order", "presolve_blocked_clause", b"presolve_blocked_clause", "presolve_bva_threshold", b"presolve_bva_threshold", "presolve_bve_clause_weight", b"presolve_bve_clause_weight", "presolve_bve_threshold", b"presolve_bve_threshold", "presolve_extract_integer_enforcement", b"presolve_extract_integer_enforcement", "presolve_inclusion_work_limit", b"presolve_inclusion_work_limit", "presolve_probing_deterministic_time_limit", b"presolve_probing_deterministic_time_limit", "presolve_substitution_level", b"presolve_substitution_level", "presolve_use_bva", b"presolve_use_bva", "probing_deterministic_time_limit", b"probing_deterministic_time_limit", "probing_num_combinations_limit", b"probing_num_combinations_limit", "propagation_loop_detection_factor", b"propagation_loop_detection_factor", "pseudo_cost_reliability_threshold", b"pseudo_cost_reliability_threshold", "push_all_tasks_toward_start", b"push_all_tasks_toward_start", "random_branches_ratio", b"random_branches_ratio", "random_polarity_ratio", b"random_polarity_ratio", "random_seed", b"random_seed", "randomize_search", b"randomize_search", "relative_gap_limit", b"relative_gap_limit", "remove_fixed_variables_early", b"remove_fixed_variables_early", "repair_hint", b"repair_hint", "restart_algorithms", b"restart_algorithms", "restart_dl_average_ratio", b"restart_dl_average_ratio", "restart_lbd_average_ratio", b"restart_lbd_average_ratio", "restart_period", b"restart_period", "restart_running_window_size", b"restart_running_window_size", "root_lp_iterations", b"root_lp_iterations", "routing_cut_dp_effort", b"routing_cut_dp_effort", "routing_cut_max_infeasible_path_length", b"routing_cut_max_infeasible_path_length", "routing_cut_subset_size_for_binary_relation_bound", b"routing_cut_subset_size_for_binary_relation_bound", "routing_cut_subset_size_for_exact_binary_relation_bound", b"routing_cut_subset_size_for_exact_binary_relation_bound", "routing_cut_subset_size_for_shortest_paths_bound", b"routing_cut_subset_size_for_shortest_paths_bound", "routing_cut_subset_size_for_tight_binary_relation_bound", b"routing_cut_subset_size_for_tight_binary_relation_bound", "save_lp_basis_in_lb_tree_search", b"save_lp_basis_in_lb_tree_search", "search_branching", b"search_branching", "search_random_variable_pool_size", b"search_random_variable_pool_size", "share_binary_clauses", b"share_binary_clauses", "share_glue_clauses", b"share_glue_clauses", "share_glue_clauses_dtime", b"share_glue_clauses_dtime", "share_level_zero_bounds", b"share_level_zero_bounds", "share_linear2_bounds", b"share_linear2_bounds", "share_objective_bounds", b"share_objective_bounds", "shared_tree_balance_tolerance", b"shared_tree_balance_tolerance", "shared_tree_max_nodes_per_worker", b"shared_tree_max_nodes_per_worker", "shared_tree_num_workers", b"shared_tree_num_workers", "shared_tree_open_leaves_per_worker", b"shared_tree_open_leaves_per_worker", "shared_tree_split_min_dtime", b"shared_tree_split_min_dtime", "shared_tree_split_strategy", b"shared_tree_split_strategy", "shared_tree_worker_enable_phase_sharing", b"shared_tree_worker_enable_phase_sharing", "shared_tree_worker_enable_trail_sharing", b"shared_tree_worker_enable_trail_sharing", "shared_tree_worker_min_restarts_per_subtree", b"shared_tree_worker_min_restarts_per_subtree", "shaving_deterministic_time_in_probing_search", b"shaving_deterministic_time_in_probing_search", "shaving_search_deterministic_time", b"shaving_search_deterministic_time", "shaving_search_threshold", b"shaving_search_threshold", "solution_pool_diversity_limit", b"solution_pool_diversity_limit", "solution_pool_size", b"solution_pool_size", "stop_after_first_solution", b"stop_after_first_solution", "stop_after_presolve", b"stop_after_presolve", "stop_after_root_propagation", b"stop_after_root_propagation", "strategy_change_increase_ratio", b"strategy_change_increase_ratio", "subsolver_params", b"subsolver_params", "subsolvers", b"subsolvers", "subsume_during_vivification", b"subsume_during_vivification", "subsumption_during_conflict_analysis", b"subsumption_during_conflict_analysis", "symmetry_detection_deterministic_time_limit", b"symmetry_detection_deterministic_time_limit", "symmetry_level", b"symmetry_level", "table_compression_level", b"table_compression_level", "transitive_precedences_work_limit", b"transitive_precedences_work_limit", "use_absl_random", b"use_absl_random", "use_all_different_for_circuit", b"use_all_different_for_circuit", "use_area_energetic_reasoning_in_no_overlap_2d", b"use_area_energetic_reasoning_in_no_overlap_2d", "use_blocking_restart", b"use_blocking_restart", "use_chronological_backtracking", b"use_chronological_backtracking", "use_combined_no_overlap", b"use_combined_no_overlap", "use_conservative_scale_overload_checker", b"use_conservative_scale_overload_checker", "use_disjunctive_constraint_in_cumulative", b"use_disjunctive_constraint_in_cumulative", "use_dual_scheduling_heuristics", b"use_dual_scheduling_heuristics", "use_dynamic_precedence_in_cumulative", b"use_dynamic_precedence_in_cumulative", "use_dynamic_precedence_in_disjunctive", b"use_dynamic_precedence_in_disjunctive", "use_energetic_reasoning_in_no_overlap_2d", b"use_energetic_reasoning_in_no_overlap_2d", "use_erwa_heuristic", b"use_erwa_heuristic", "use_exact_lp_reason", b"use_exact_lp_reason", "use_extended_probing", b"use_extended_probing", "use_feasibility_jump", b"use_feasibility_jump", "use_feasibility_pump", b"use_feasibility_pump", "use_hard_precedences_in_cumulative", b"use_hard_precedences_in_cumulative", "use_implied_bounds", b"use_implied_bounds", "use_lb_relax_lns", b"use_lb_relax_lns", "use_linear3_for_no_overlap_2d_precedences", b"use_linear3_for_no_overlap_2d_precedences", "use_lns", b"use_lns", "use_lns_only", b"use_lns_only", "use_ls_only", b"use_ls_only", "use_new_integer_conflict_resolution", b"use_new_integer_conflict_resolution", "use_objective_lb_search", b"use_objective_lb_search", "use_objective_shaving_search", b"use_objective_shaving_search", "use_optimization_hints", b"use_optimization_hints", "use_optional_variables", b"use_optional_variables", "use_overload_checker_in_cumulative", b"use_overload_checker_in_cumulative", "use_pb_resolution", b"use_pb_resolution", "use_phase_saving", b"use_phase_saving", "use_precedences_in_disjunctive_constraint", b"use_precedences_in_disjunctive_constraint", "use_probing_search", b"use_probing_search", "use_rins_lns", b"use_rins_lns", "use_sat_inprocessing", b"use_sat_inprocessing", "use_shared_tree_search", b"use_shared_tree_search", "use_strong_propagation_in_disjunctive", b"use_strong_propagation_in_disjunctive", "use_symmetry_in_lp", b"use_symmetry_in_lp", "use_timetable_edge_finding_in_cumulative", b"use_timetable_edge_finding_in_cumulative", "use_timetabling_in_no_overlap_2d", b"use_timetabling_in_no_overlap_2d", "use_try_edge_reasoning_in_no_overlap_2d", b"use_try_edge_reasoning_in_no_overlap_2d", "variable_activity_decay", b"variable_activity_decay", "variables_shaving_level", b"variables_shaving_level", "violation_ls_compound_move_probability", b"violation_ls_compound_move_probability", "violation_ls_perturbation_period", b"violation_ls_perturbation_period"]
    def ClearField(self, field_name: _ClearFieldArgType) -> None: ...

Global___SatParameters: typing_extensions.TypeAlias = SatParameters
