TSP GRASP Demo

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

Governing Equations

Tour Length
L(π) = Σ d(πᵢ, πᵢ₊₁)
L = --
1-Tree Lower Bound
LB = MST + min edges
LB = --

Statistics

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

Controls

Cities 25
Method

Falsification Status

Gap ≤ 20% --
CV ≤ 5% --
Status Pending
docs/emc/optimization/tsp_grasp.emc.yaml

EMC Identity

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

Verification Tests

TSP-001 Valid Permutation
TSP-002 Above Lower Bound
TSP-003 2-Opt Monotonicity
TSP-004 Deterministic Replay
TSP-005 Greedy vs Random

Falsification Criteria

TSP-FC-001 Invalid Tour
TSP-FC-002 Below Lower Bound
TSP-FC-003 2-Opt Increases
TSP-FC-004 Excessive Gap

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

Assertion Log