TSP GRASP Demo

EMC-OPT-003 | optimization/tsp_grasp v1.0.0
EDD PROBAR
Loading WASM...

Governing Equations

Tour Length
L(pi) = Sum d(pi_i, pi_i+1)
L = --
1-Tree Lower Bound
LB = MST + min edges
LB = --

Statistics

Cities --
Best Tour --
Lower Bound --
Gap --
Restarts --
2-Opt Improvements --

Controls

Cities 25

Falsification Status

Gap <= 20% --
CV <= 5% --
Status Pending
docs/emc/optimization/tsp_grasp.emc.yaml
Loading EMC configuration...

EMC Identity

ID EMC-OPT-003
Name TSP GRASP with 2-Opt
Version 1.0.0
Status production

Probar Test Suite

0/7 passed
? Tour visits all cities exactly once
? Tour forms closed loop
? Best tour monotonically improves
? 2-opt only improves or maintains
? Tour length >= lower bound
? Same seed produces same result
? All values are finite

Invariant Checker

Valid Permutation
Triangle Inequality
Positive Distances
Finite Values
Above Lower Bound