@@ -194,6 +194,39 @@ The following reformulation methods are currently supported:
     - `final_reform_method`: Reformulation method to apply after cutting plane iterations. Default: `BigM()`.
     - `M_value`: Big-M value to use in the relaxed Big-M reformulation during iterations. Default: `1e9`.
 
+## Basic Steps
+
+A [basic step](https://epubs.siam.org/doi/10.1137/0606047) intersects two or more disjunctions into a single one whose disjuncts are the intersections of the original disjuncts, taken over their cartesian product. The feasible region is unchanged, but the hull relaxation of the result is at least as tight as before. Global constraints can also be intersected into a disjunction (an improper basic step), which is done with the `constraints` keyword argument:
+
+```julia
+using DisjunctiveProgramming, HiGHS
+
+model = GDPModel(HiGHS.Optimizer)
+@variable(model, 0 <= x <= 5)
+@variable(model, Y[1:2], Logical)
+@variable(model, Z[1:2], Logical)
+@objective(model, Max, x)
+@constraint(model, x <= 1, Disjunct(Y[1]))
+@constraint(model, 2 <= x <= 3, Disjunct(Y[2]))
+@constraint(model, x <= 1, Disjunct(Z[1]))
+@constraint(model, 4 <= x <= 5, Disjunct(Z[2]))
+d1 = disjunction(model, Y)
+d2 = disjunction(model, Z)
+
+# replace both disjunctions with their 4 term product disjunction
+apply_basic_step(model, [d1, d2])
+
+optimize!(model, gdp_method = Hull())
+```
+
+`apply_basic_step` deletes the original disjunctions and their disjunct constraints, but keeps the original logical variables and ties them to the new product indicators with `Exactly` constraints, so any reformulation method can be used afterwards. The indicators of the disjuncts that were intersected to form a product disjunct can be queried with `product_parents(w)`, where `w` is one of the indicators of the returned disjunction. It accepts the following optional arguments:
+
+- `constraints`: Global constraints to intersect into every disjunct of the new disjunction. They are deleted from the model afterwards.
+- `name`: Base name for the product disjunction, its indicator variables, and the linking constraints. Anonymous by default.
+- `relax_products`: If `true`, the binary variables of the product indicators are relaxed to `[0, 1]`. This is valid because the original indicators remain binary and force the products integral, and it avoids growing the number of binary variables.
+
+Note that the number of disjuncts of the product disjunction is the product of those of the inputs, so repeated basic steps grow the model multiplicatively. Intersecting disjunctions that share variables (or that are coupled by an intersected global constraint) is what tightens the relaxation; disjunctions over disjoint variables gain nothing and only pay the size cost.
+
 ## Conic Constraints
 
 Disjunct constraints can also be defined with the conic sets `SecondOrderCone`, `RotatedSecondOrderCone`, `MOI.ExponentialCone`, and `MOI.PowerCone`. Big-M reformulates these by relaxing the constraint function along a fixed interior direction of the cone, and Hull produces the exact conic hull of [Bernal Neira & Grossmann [2021]](https://arxiv.org/abs/2109.09657).
 
@@ -26,6 +26,31 @@ end
 ################################################################################
 DP.InfiniteLogical(prefs...) = DP.Logical(InfiniteOpt.Infinite(prefs...))
 
+const _InfExpr = Union{
+    InfiniteOpt.GeneralVariableRef,
+    JuMP.GenericAffExpr{<:Any, InfiniteOpt.GeneralVariableRef},
+    JuMP.GenericQuadExpr{<:Any, InfiniteOpt.GeneralVariableRef},
+    JuMP.GenericNonlinearExpr{InfiniteOpt.GeneralVariableRef}
+}
+
+# The parameters of every expression, in the order encountered
+function _union_parameter_refs(exprs)
+    return unique!([pref for expr in exprs
+                    for pref in InfiniteOpt.parameter_refs(expr)])
+end
+
+# A product indicator varies over the parameters of its parents, so the
+# linking constraints stay pointwise-consistent with the originals
+function DP.product_indicator_variable(
+    model::InfiniteOpt.InfiniteModel,
+    parents
+    )
+    prefs = _union_parameter_refs(DP.binary_variable(p) for p in parents)
+    lvar = DP.LogicalVariable(nothing, nothing, nothing)
+    isempty(prefs) && return lvar
+    return DP._TaggedLogicalVariable(lvar, InfiniteOpt.Infinite(prefs...))
+end
+
 _is_parameter(vref::InfiniteOpt.GeneralVariableRef) =
     _is_parameter(InfiniteOpt.dispatch_variable_ref(vref))
 _is_parameter(::InfiniteOpt.DependentParameterRef) = true
@@ -88,21 +113,8 @@ function DP.VariableProperties(
     return DP.VariableProperties(info, "", nothing, var_type)
 end
 
-function DP.VariableProperties(
-    exprs::Vector{<:Union{
-        InfiniteOpt.GeneralVariableRef,
-        JuMP.GenericAffExpr{<:Any, InfiniteOpt.GeneralVariableRef},
-        JuMP.GenericQuadExpr{<:Any, InfiniteOpt.GeneralVariableRef},
-        JuMP.GenericNonlinearExpr{InfiniteOpt.GeneralVariableRef}
-    }}
-)
-    all_prefs = Set{InfiniteOpt.GeneralVariableRef}()
-    for expr in exprs
-        for pref in InfiniteOpt.parameter_refs(expr)
-            push!(all_prefs, pref)
-        end
-    end
-    prefs = Tuple(all_prefs)
+function DP.VariableProperties(exprs::AbstractVector{<:_InfExpr})
+    prefs = _union_parameter_refs(exprs)
     info = DP._free_variable_info()
     var_type = !isempty(prefs) ? InfiniteOpt.Infinite(prefs...) : nothing
     return DP.VariableProperties(info, "", nothing, var_type)
@@ -159,6 +171,34 @@ function JuMP.add_constraint(
     error("Cannot add, subtract, or multiply with logical variables.")
 end
 
+# Resolve the ambiguity between InfiniteOpt's generic
+# `delete(::InfiniteModel, vref)` and DP's typed deletes (needed when a
+# basic step deletes its inputs). The ref types must be concrete, since
+# a `Union` of them is not specific enough.
+function JuMP.delete(
+    m::InfiniteOpt.InfiniteModel, cref::DP.DisjunctionRef
+    )
+    return DP._delete(m, cref)
+end
+
+function JuMP.delete(
+    m::InfiniteOpt.InfiniteModel, cref::DP.DisjunctConstraintRef
+    )
+    return DP._delete(m, cref)
+end
+
+function JuMP.delete(
+    m::InfiniteOpt.InfiniteModel, cref::DP.LogicalConstraintRef
+    )
+    return DP._delete(m, cref)
+end
+
+function JuMP.delete(
+    m::InfiniteOpt.InfiniteModel, vref::DP.LogicalVariableRef
+    )
+    return DP._delete(m, vref)
+end
+
 ################################################################################
 #                                  METHODS
 ################################################################################
 
@@ -32,6 +32,7 @@ include("print.jl")
 include("extension_api.jl")
 include("utilities.jl")
 include("psplit.jl")
+include("basicsteps.jl")
 
 # Define additional stuff that should not be exported
 const _EXCLUDE_SYMBOLS = [Symbol(@__MODULE__), :eval, :include]