How maxsat-tsp/maxsattrainscheduling works
This Rust project implements train-rescheduling optimization: a user selects solver configurations for fixed-route instances and delay-cost objectives, and the CLI parses the instance, dispatches a solver, and verifies the resulting schedule. Its main product capability is MaxSAT-based Dynamic Discretization Discovery (DDD), alongside SAT and MILP baselines; it also includes a separate conflict-based heuristic GUI. The README documents benchmark and analysis capabilities, but those scripts and data are not runtime components. Some internal wiring is omitted because the sampled source excerpts do not show it.
Main entry points: src/main.rs CLI runner · ddd/mod.rs DDD solver family · milp/mod.rs MILP baselines · src/main.rs GUI entry point
Components 21
Input and CLI
- CLI runner
src/main.rs - Instance parser
src/parser.rs - Problem model
src/problem.rs - Solution verification
src/problem.rs
DDD Solvers
- DDD solver family
src/solvers/ddd/mod.rs - MaxSAT ladder
src/solvers/ddd/maxsat_ladder.rs - Sequential-counter MaxSAT
src/solvers/ddd/maxsat_ladder_sc/solve.rs - Incremental SAT
src/solvers/ddd/incremental_sat.rs - Pure SAT
src/solvers/ddd/puresat.rs - DDD shared logic
src/solvers/ddd/shared/mod.rs - MaxSAT interface
src/maxsatsolver.rs
Solver Baselines
- MILP baselines
src/solvers/milp/mod.rs - Big-M solver
src/solvers/milp/bigm.rs - MIP-DDD solver
src/solvers/milp/mipdddpack.rs - Legacy solvers
src/solvers/legacy/mod.rs - LP exporter
src/bin/export_lp.rs
Heuristic GUI
- Conflict solver
crates/heuristic/src/solver.rs - Rescheduling GUI
crates/heuristic_gui/src/app.rs - GUI entry point
crates/heuristic_gui/src/main.rs
Other components
- Solver user
- Gurobi
Connections 24
- Solver user → CLI runner: selects solver
- CLI runner → Instance parser: loads instance
- Instance parser → Problem model: builds model
- CLI runner → DDD solver family: dispatches DDD
- CLI runner → MILP baselines: dispatches MILP
- CLI runner → Legacy solvers: dispatches legacy
- DDD solver family → MaxSAT ladder: selects variant
- DDD solver family → Sequential-counter MaxSAT: selects variant
- DDD solver family → Incremental SAT: selects variant
- DDD solver family → Pure SAT: selects variant
- MaxSAT ladder → MaxSAT interface: solves MaxSAT
- Sequential-counter MaxSAT → MaxSAT interface: solves MaxSAT
- Incremental SAT → DDD shared logic: uses shared logic
- MILP baselines → Big-M solver: selects variant
- MILP baselines → MIP-DDD solver: selects variant
- Big-M solver → Gurobi: optimizes model
- MIP-DDD solver → Gurobi: optimizes model
- CLI runner → Solution verification: checks solution
- Solver user → GUI entry point: starts GUI
- GUI entry point → Conflict solver: creates solver
- GUI entry point → Rescheduling GUI: launches app
- Rescheduling GUI → Conflict solver: steps and displays
- LP exporter → Instance parser: loads instance
- LP exporter → Gurobi: exports model for