Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

alg_solution_ty

AlgSolution : ApproxAlgorithm P → String → Real The solution value produced by the approximation algorithm.

app

app2

app3

approx_algorithm_ty

ApproxAlgorithm : OptimizationProblem → Type An algorithm with a guaranteed approximation ratio.

approx_ratio_ty

ApproxRatio : ApproxAlgorithm P → Real The approximation ratio achieved by the algorithm.

apx_complete_ty

APXComplete : OptimizationProblem → Prop The problem is APX-complete.

apx_hard_ty

APXHard : OptimizationProblem → Prop The problem is APX-hard: no PTAS unless P=NP.

apx_ty

APX : OptimizationProblem → Prop The problem is in APX: has a constant-factor approximation algorithm.

arora_ptas_euclidean_tsp_ty

AroraPTASEuclideanTSP : Prop

arrow

bool_ty

build_approximation_algorithms_env

Populate an Environment with approximation algorithm axioms.

build_approximation_algorithms_ext_env

Register all §9–§12 approximation algorithm axioms into env.

build_env

Alias for build_approximation_algorithms_env.

bvar

christofides_serdyukov

Christofides-Serdyukov algorithm for metric TSP (3/2-approximation). Full implementation with minimum perfect matching on odd-degree vertices.

christofides_serdyukov_ty

ChristofidesSerdyukov : 3/2-approximation for metric TSP The Christofides-Serdyukov algorithm:

chromatic_inapprox_ty

ChromaticInapprox : Graph coloring is hard to approximate within n^(1−ε)

clique_inapprox_ty

CliqueSizeInapprox : MAX-CLIQUE has no n^(1−ε)-approximation unless P=NP

correlation_rounding_ty

CorrelationRounding : LPRelaxation P → ApproxAlgorithm P

cst

dependent_rounding_ty

DependentRounding : LPRelaxation P → ApproxAlgorithm P

eptas_ty

EPTAS : OptimizationProblem → Prop Efficient PTAS: running time is f(1/ε)·poly(n) for some function f.

facility_location_bicriteria_ty

FacilityLocationBicriteria : Real → Real → Prop

fptas_subset_ptas_ty

FPTAS_subset_PTAS : Every FPTAS problem has a PTAS

fptas_ty

FPTAS : OptimizationProblem → Prop The problem has a Fully PTAS: running time is poly(n, 1/ε).

gap_amplification_ty

GapAmplification : Prop

goemans_williamson_max_cut_ty

GoemansWilliamsonMaxCut : 0.878-approximation for MAX-CUT via SDP

goemans_williamson_ratio_ty

GoemansWilliamsonRatio : Real

greedy_algorithm_ty

GreedyAlgorithm : OptimizationProblem → Type A greedy algorithm making locally optimal choices at each step.

greedy_max_coverage

Greedy max-coverage algorithm: select k sets to maximize the number of covered elements. Achieves (1 − 1/e)-approximation.

greedy_set_cover

Greedy set cover algorithm. universe: elements to cover (0..n). sets: each set is a Vec of elements. Returns indices of selected sets (greedy by max coverage).

hypergraph_cut_sdp_ty

HypergraphCutSDP : Real → Prop

inapproximability_reduction_ty

InapproximabilityReduction : Prop

integrality_gap_ty

IntegralityGap : LPRelaxation P → Real The integrality gap: ratio of LP optimum to IP optimum.

is_alpha_approx_ty

IsAlphaApprox : OptimizationProblem → Real → Prop There exists a polynomial-time algorithm with approximation ratio α.

is_set_cover

Check whether a set cover covers the entire universe.

is_vertex_cover

Check whether a vertex cover is valid for the given graph.

iterative_rounding_thm_ty

IterativeRoundingThm : Prop

jain_iterative_rounding_ty

JainIterativeRounding : Prop

k_connectivity_approx_ty

KConnectivityApprox : Nat → Real → Prop

k_means_plus_plus_ty

KMeansPlusPlus : OptimizationProblem → Prop

k_median_approx_ty

KMedianApprox : Real → Prop

k_median_local_search_ty

KMedianLocalSearch : O(1)-approximation for k-median via local search

knapsack_fptas

FPTAS for 0-1 knapsack. Scales item values by (ε·max_value / n) and runs exact DP. Achieves (1 − ε) approximation in O(n^2 / ε) time.

kruskal_mst

Minimum Spanning Tree using Kruskal’s algorithm. Returns (total weight, list of edges in MST).

lasserre_hierarchy_ty

LasserreHierarchy : OptimizationProblem → Nat → Type

list_scheduling_approx_ty

ListSchedulingApprox : Real → Prop

list_ty

load_balancing_online_ty

LoadBalancingOnline : Real → Prop

local_optimum_ty

LocalOptimum : LocalSearchAlgorithm P → String → Prop A solution is locally optimal (no improvement in the neighborhood).

local_search_algorithm_ty

LocalSearchAlgorithm : OptimizationProblem → Type A local search algorithm iteratively improves solutions.

local_search_max_cut

Local search for MAX-CUT: start with random partition, swap vertices to improve cut. Returns (cut value, partition assignment: 0 or 1 for each vertex).

local_search_ratio_ty

LocalSearchRatio : LocalSearchAlgorithm P → Real → Prop Local search achieves the given ratio at any local optimum.

lp_dominates_ty

LPDominates : LPRelaxation P → OptimizationProblem → Prop The LP bound dominates (is at least as tight as) the IP optimum.

lp_hierarchy_ty

LPHierarchy : OptimizationProblem → Nat → Type

lp_relaxation_ty

LPRelaxation : OptimizationProblem → Type The LP relaxation of an integer program.

makespan_ptas_ty

MakespanPTAS : Prop

max_coverage_greedy_ty

MaxCoverageGreedy : (1 − 1/e)-approximation for max coverage by greedy

max_cut_local_search_ty

MaxCutLocalSearch : 2-approximation for MAX-CUT via local search

max_sat_inapprox_ty

MaxSATInapprox : MAX-3SAT has no (7/8 + ε)-approximation unless P=NP

max_snp_hard_apx_hard_ty

MaxSNPHard_implies_APXHard : MAX-SNP hardness implies APX-hardness

max_snp_ty

MaxSNP : OptimizationProblem → Prop The problem is in MAX-SNP (Papadimitriou-Yannakakis class).

metric_tsp_2approx

MST-based 2-approximation for metric TSP. Input: complete graph with metric distances (n x n matrix). Returns a Hamiltonian cycle (vertex ordering) and its total cost.

metric_tsp_ty

MetricTSP : OptimizationProblem — TSP on metric instances (triangle inequality).

mitchell_ptas_euclidean_tsp_ty

BakeryPTAS : Prop

mst_2approx_ty

MST2Approx : MST-based 2-approximation for metric TSP

nat_ty

network_design_lp_ty

NetworkDesignLPRelaxation : Type

online_algorithm_competitive_ty

OnlineAlgorithmCompetitive : OptimizationProblem → Real → Prop

opt_solution_ty

OptSolution : OptimizationProblem → String → Real The optimal solution value for a given instance.

optimization_problem_ty

OptimizationProblem : Type — a minimization or maximization problem.

option_ty

pair_ty

pcp_theorem_ty

PCPTheorem : NP = PCP(log n, 1) Every NP language has a proof system with logarithmic randomness and constant query complexity.

pi

pipage_rounding_ty

PipageRounding : LPRelaxation P → ApproxAlgorithm P

preemptive_schedule_approx_ty

PreemptiveScheduleApprox : Prop

primal_dual_algorithm_ty

PrimalDualAlgorithm : OptimizationProblem → Type An algorithm designed via the primal-dual schema.

primal_dual_guarantee_ty

PrimalDualGuarantee : PrimalDualAlgorithm P → Real → Prop The primal-dual algorithm achieves the given approximation ratio.

primal_dual_weighted_vc

Primal-dual algorithm for weighted vertex cover. Maintains dual variables y_e for each edge; raises y_e until some endpoint becomes “tight” (sum of y_e = w_v), then adds that vertex.

prop

ptas_subset_apx_ty

PTAS_subset_APX : Every PTAS problem is in APX

ptas_ty

PTAS : OptimizationProblem → Prop The problem has a Polynomial-Time Approximation Scheme: for every ε > 0, there is a (1+ε)-approximation running in poly(n).

randomized_rounding_gap_ty

RandomizedRoundingGap : Real → Prop

randomized_rounding_ty

RandomizedRounding : LPRelaxation P → ApproxAlgorithm P Randomized rounding converts LP solutions to integer solutions.

randomized_rounding_vertex_cover

Randomized rounding for weighted vertex cover (LP relaxation). Solves the LP: for each vertex v, x_v ≥ 0; for each edge (u,v), x_u + x_v ≥ 1. The LP optimum is half-integral; round x_v ≥ 1/2 to 1. This gives a 2-approximation in expectation.

real_ty

sdp_integrality_gap_ty

SDPIntegralityGap : SDPRelaxation P → Real

sdp_max_cut_gap_optimal_ty

SDPMaxCutGapOptimal : Prop

sdp_relaxation_ty

SDPRelaxation : OptimizationProblem → Type

set_cover_greedy_ratio_ty

SetCoverGreedyRatio : Greedy set cover achieves H_n ratio (≤ ln n + 1)

set_cover_inapprox_ty

SetCoverInapprox : Set Cover has no (1 − ε)·ln n approximation unless P=NP

set_cover_lp_gap_ty

SetCoverLPGap : The set cover LP has integrality gap Θ(log n)

ski_rental_breakeven_ty

SkiRentalBreakeven : Prop

steiner_forest_approx_ty

SteinerForestApprox : Real → Prop

steiner_tree_approx_ty

SteinerTreeApprox : Real → Prop

steiner_tree_pd_ty

SteinertreePD : The Steiner tree primal-dual gives 2(1 − 1/l) ratio

submodular_greedy_ty

SubmodularGreedy : Greedy gives (1 − 1/e) for submodular maximization

tightness_integrality_gap_ty

TightnessOfIntegralityGap : LPRelaxation P → Real → Prop

tsp_no_approx_ty

TSPNoApprox : Metric-free TSP has no constant approximation unless P=NP

type0

unique_games_conj_ty

UniqueGamesConj : Prop

vertex_cover_2approx

2-approximation for vertex cover via greedy edge cover. At each step pick an uncovered edge (u,v) and add both endpoints to the cover.

vertex_cover_apx_hard_ty

VertexCoverAPXHard : Vertex Cover is APX-hard

vertex_cover_lp_gap_ty

VertexCoverLPGap : The vertex cover LP has integrality gap 2

weighted_vertex_cover_pd_ty

WeightedVertexCoverPD : 2-approximation via primal-dual for weighted VC