Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

alternating_path_ty

Alternating_path : Graph → Matching → List Nat → Prop — alternating path wrt matching.

app

app2

app3

arrow

assignment_ty

Assignment : Nat → (Nat → Nat) → Prop — a permutation assignment for n×n matrix.

augmenting_path_ty

AugmentingPath : Graph → Matching → List Nat → Prop — augmenting path.

berge_theorem_ty

BergeTheorem : max matching augmenting path characterization

bipartite_graph_ty

BipartiteGraph : Type — bipartite graph with two vertex sets.

bipartite_incidence_tu_ty

BipartiteIncidenceTU : incidence matrix of bipartite graph is TU.

blossom_ty

Blossom : Graph → Matching → List Nat → Prop — odd cycle contracted in Edmonds’ algorithm.

bool_ty

branch_and_bound_ty

BranchAndBound : ILPInstance → List Int — branch-and-bound solver.

build_combinatorial_optimization_env

Register all combinatorial optimization axioms into the kernel environment.

bvar

christofides_approximation_ty

ChristofidesApproximation : 3/2-approximation for metric TSP.

cost_matrix_ty

CostMatrix : Nat → Nat → Real — cost matrix for assignment.

cst

cut_capacity_ty

CutCapacity : FlowNetwork → (Nat → Bool) → Real — total capacity of a cut.

cut_ty

Cut : FlowNetwork → (Nat → Bool) → Prop — s-t cut (partition of vertices).

dinics_complexity_ty

DinicsComplexity : Dinic's algorithm runs in O(V² E).

facet_defining_ty

FacetDefiningInequality : Polytope → (List Real → Prop) → Prop

flow_network_ty

FlowNetwork : Type — directed graph with capacities.

flow_ty

Flow : FlowNetwork → Type — feasible flow satisfying capacity and conservation.

flow_value_ty

FlowValue : FlowNetwork → Flow → Real — the value of a flow (net flow out of source).

ford_fulkerson_termination_ty

FordFulkersonTermination : Ford-Fulkerson terminates on integer capacities.

gomory_cut_ty

GomoryCut : ILPInstance → ILPInstance — adds a Gomory cutting plane.

graph_ty

Graph : Type — a simple undirected graph (vertices: Nat, edges: pairs).

graphic_matroid_ty

GraphicMatroid : Graph → Matroid — cycle matroid of a graph.

greedy_optimality_ty

GreedyOptimality : Greedy algorithm is optimal for matroid weight maximization.

greedy_set_cover

Greedy set cover: returns selected set indices covering all elements 0..n_elem.

hall_condition_ty

HallCondition : BipartiteGraph → Prop For every subset S of left vertices, |N(S)| ≥ |S|.

hall_theorem_ty

HallTheorem : ∀ G : BipartiteGraph, HallCondition G ↔ PerfectMatching G

held_karp_bound_ty

HeldKarpBound : TSPInstance → Real — Held-Karp lower bound.

held_karp_lower_bound_ty

HeldKarpLowerBound : HeldKarpBound ≤ TSPOptimal.

hungarian

Solve the minimum-weight assignment problem using the Hungarian algorithm. Returns (total cost, assignment vector where assignment[i] = j means row i → col j).

hungarian_algorithm_ty

HungarianAlgorithm : CostMatrix → (Nat → Nat) — solves assignment in O(n³).

hungarian_correctness_ty

HungarianCorrectness : HungarianAlgorithm gives OptimalAssignment.

ilp_instance_ty

ILPInstance : Type — integer linear program: min c·x s.t. Ax ≤ b, x ∈ ℤ^n.

ilp_optimal_ty

ILPOptimal : ILPInstance → List Int → Prop

ilp_solution_ty

ILPSolution : ILPInstance → List Int → Prop

independent_set_ty

IndependentSet : Matroid → List Nat → Prop

int_ty

knapsack_01

Branch-and-bound for 0-1 knapsack (maximize). items: (value, weight), capacity: max weight. Returns (max_value, selected_item_indices).

konig_theorem_ty

KonigTheorem : MaxMatchingSize = MinVertexCoverSize for bipartite graphs.

list_ty

lp_relaxation_lower_bound_ty

LPRelaxationLowerBound : LPRelaxation ≤ ILP optimal.

lp_relaxation_ty

LPRelaxation : ILPInstance → Real — optimal LP relaxation value.

matching_ty

Matching : Graph → Type — a set of non-adjacent edges.

matroid_base_ty

MatroidBase : Matroid → List Nat → Prop — maximal independent set.

matroid_intersection_optimality_ty

MatroidIntersectionOptimality : the max weight common independent set.

matroid_intersection_ty

MatroidIntersection : common independent set in two matroids.

matroid_rank_ty

MatroidRank : Matroid → Nat — rank of a matroid.

matroid_ty

Matroid : Type — a matroid (ground set + independent sets satisfying axioms).

max_flow_min_cut_ty

MaxFlowMinCut : ∀ N, MaxFlow N = MinCut N — the max-flow min-cut theorem.

max_flow_ty

MaxFlow : FlowNetwork → Real — maximum flow value.

max_matching_ty

MaxMatching : Graph → Matching → Prop — a maximum cardinality matching.

min_cut_ty

MinCut : FlowNetwork → Real — minimum cut capacity.

nat_ty

optimal_assignment_ty

OptimalAssignment : CostMatrix → (Nat → Nat) → Prop — assignment minimizing total cost.

option_ty

pair_ty

perfect_matching_ty

PerfectMatching : Graph → Prop — every vertex is matched.

pi

polymatroid_rank_ty

PolymatroidRankFunction : axioms for polymatroid rank.

polytope_ty

Polytope : Type — a convex polytope (intersection of halfspaces).

polytope_vertex_ty

Vertex : Polytope → List Real → Prop — extreme point of polytope.

prop

real_ty

set_cover_approx_ty

SetCoverApproximation : H_n-approximation (log n) for set cover.

strong_duality_ty

StrongDuality : for LP, dual objective = primal when both feasible.

submodular_function_ty

SubmodularFunction : (List Nat → Real) → Prop f is submodular if f(A) + f(B) ≥ f(A∪B) + f(A∩B).

submodular_greedy_approx_ty

SubmodularGreedy_1_2_approx : greedy gives 1/2-approximation for monotone submodular max.

submodular_maximization_ty

SubmodularMaximization : (List Nat → Real) → List Nat — greedy maximization.

supermodular_function_ty

SupermodularFunction : (List Nat → Real) → Prop — supermodular (negation of submodular).

totally_unimodular_ty

TotallyUnimodular : (Nat → Nat → Int) → Prop — every square submatrix has det ∈ {-1,0,1}.

tsp_held_karp

Held-Karp DP lower bound (exact TSP for small n ≤ 20).

tsp_instance_ty

TSPInstance : Type — complete graph with edge weights.

tsp_nearest_neighbor

Nearest-neighbor heuristic for TSP. Returns tour (list of vertex indices).

tsp_optimal_ty

TSPOptimal : TSPInstance → Real — optimal TSP tour length.

tsp_tour_ty

TSPTour : TSPInstance → List Nat → Prop — a Hamiltonian cycle.

tu_integral_polyhedra_ty

TUIntegralPolyhedra : TU matrix → LP has integer optimal vertex.

tutte_condition_ty

TutteCondition : Graph → Prop For every S ⊆ V, the number of odd components of G-S is ≤ |S|.

tutte_theorem_ty

TutteTheorem : ∀ G, PerfectMatching G ↔ TutteCondition G

type0

uniform_matroid_greedy

Greedy maximum weight independent set in uniform matroid U(k, n). Returns indices of k elements with highest weights.

uniform_matroid_ty

UniformMatroid : Nat → Nat → Matroid — U(k,n) uniform matroid.

vertex_cover_approx_ty

VertexCoverApproximation : 2-approx for vertex cover.

weak_duality_ty

WeakDuality : for LP, dual objective ≥ primal objective.